I am very new to Verification and this might be a very trivial question
I have read that Assertion based Formal Verification does not require a test bench or test cases. But consider this example:
State S35 can be active for <= 5 cycles
assert property (@(posedge clk ) $rose(S35) |=> S35[1:4] ##1 !S35 );
Even in the above example, the design under test must be sensitized so that it can reach S35 and test cases have to be applied to the DUT that can either pass or fail the assertion.
My question is, where is the difference between this method and a simulation based method?Even in Simulation based method, the DUT will be sensitized in order to check whether S35 is active for more than 5 cycles?
I went through the material on formal verification at Verification Academy. In addition to this can anyone suggest a good source of reference?
On your question, formal verification would work. Below is what I wrote in my SystemVerilog Assertions Handbook:
7.1.3 Who should use formal verification
Formal verification is best performed by the RTL design engineer with assertions, assumptions, and
restrictions (see 4.5.1) written by both the RTL designer and the verification engineer. The verification
engineer specifies the requirements, whereas the design engineer understands the design details and can
identify the needed corrections in the event of errors identified by the formal verification tool and the
counterexamples (i.e., scenario cases that can cause the failure).
7.1.4 More about model checking
In model checking, properties (written in a property language, like SVA) are used to capture the design
intent. A formal verifier reads in an RTL design and builds a state transition graph for the system in a
manner similar to an FSM. A first and foremost requirement for Model Checking is that designs need to be
synthesizable and cycle-based. A natural limitation of such an approach would be that designs that contain
elements such as phase-locked loops (PLLs), behavioral memories, etc. cannot be converted into logic
equations, thus they can’t be proven using the formal engines. Typically, a model checker treats non-
synthesizable blocks as black-boxes, making the outputs of those blocks free ranging variables (meaning
that they can have any random value), unless built-in models are available for those black boxes
The Verifier then reads in the properties and directives. Typically these properties represent the design
specification as temporal sequences (such as request to grant protocols, illegal transitions), and they specify
whether these properties hold forever or during a finite time. A Model Checker then checks whether the
design implementation obeys these properties by searching the entire state space of the design, and
produces counterexamples if the design fails to obey the properties.
By definition, FV is a complete proof, and hence is the ultimate verification methodology – if applicable.
However, FV suffers heavily from the state space explosion problem for larger designs because it needs to
search a very large number of states. An acceptable methodology is to limit the analysis to blocks of
manageable size by partitions (i.e., smaller blocks) or by imposing constraints via the restrict operator to
limit the scenarios for convergence on a proof (see 4.5.1.3). The assume construct should also be used to
specify legal input states; this would avoid a failure due to some sequence of inputs that would not happen
in the real world.