Inconclusive Assertion in Synopsys VC Formal

2 Questions -

1. In Assertion Based Formal Verification, if I get an Inconclusive Assertion, then what are the various approaches to handle that assertion or to converge it?
2. Is it a right approach to develop a reference rtl and write assertions to compare reference rtl output with DUT output on each active clock edge? Will it increase the valid State Spaces and hence complexity, run time also?

Also it would be helpful, if anyone can provide some good reference material for assertion based formal verification, as I am not able to find much articles/papers on this topic.

I have got the answer of my own question, so I am here posting it.

Inconclusive Assertions are natural part of Formal Verification. So Verification Sign off is still possible, if you have got the "Required Proof Bound Depth". (It is similar to coverage in Simulation based Verification, where you can still sign off the verification, if you have got the required coverage numbers). To get the "Required Proof Bound Depth", one must contact the design team.

Bounded Proof Depth > Required Proof Depth => Equivalent to Full Proof

Bounded Proof can be due to multiple reasons.

• State Space of the Design and/or Assertion
• Complexity of the Design and/or Assertion
• Tool Options (Effort Level Run Time Memory Constraint Algorithm)

So your approach should be to get "Required Proof Bound".

Now to get Required Proof Bound, various options are there.

• Tool/Resource Options (Effort Level, Run Time, Memory Constraint)
• State Space & Complexity Options
  • Modify/Add Constraints
  • Blackboxing
  • Cut-points
  • Modify Assertions
  • Alter Parameter values for Parameterized Designs
  • Simulation Based Reset State
  • Guided Proofs
  • Abstractions

Still, there is no assurance to get required proof bound, through this approach. So typically, Formal Verification standalone is not used, but it is used, rather as a supplement to the Simulation Based Verification

Yes, comparing reference model and DUT output, can increase the complexity, so reference model should be used minimally, if required.