In our last edition we've asked you to submit answers to a Formal Verification FAQ - now the answers keep coming in.
This set is from Ankit Jain an avid contributor to FormalWorld.org
What is Formal Verification?
Ans. Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
In other words, formal verification is a systematic process that uses mathematical reasoning to verify that design intent (specification) is preserved in implementation (RTL)
What is the difference between Formal and simulation based verification?
Ans. In simulation, it is not possible to simulate all possible states in a design. But formal verification explores all possible states in the design. Simulation focuses on scenarios while formal verification focuses on the correctness of the intent of functional behaviour.
In simulation, we must have idea of all the scenarios and vectors and a strong testbench in order to verify the design adequately, while formal verification does not require testbench or stimulus.
We may miss the corner case bugs in simulation while formal verification will catch all the corner case bugs.
Testbench requires time to be created while formal verification starts early in the design cycle.
Simulation must propagate bugs to output pin or we have to write assertions local to the testcase to find the bugs. In formal verification automatically isolate the root cause of the bugs.
Simulation will require mass number of engineers to be employed. On the other hand, we can train engineers to write assertions and teach them the formal concepts. After that verification will become automatic.
What is the difference between Combinational and Sequential Equivalence checking?
Ans. Combinational synthesis changes only the combinational logic and keeps the PO (Primary Output) and NS (Next State) functions (as functions of PI and CS) unchanged, although the network computing these functions can be completely restructured. In this case, equivalence checking consists of just checking the equivalence of the combinational parts of the two circuits.
In contrast, sequential synthesis, additionally uses information about the states unreachable from the initial state to modify the combinational logic further. This can consist of (a) using the unreached states as don’t cares, (b) using the fact that two states are equivalent, (c) using a different encoding for the reachable states, (d) retiming the FFs, or (e) merging two signals in the circuit if in all reachable states the signals have the same values.
How do you do formal verification in physical design (or post layout)?
Ans. The logical functionality of the post-layout netlist (including any layout-driven optimization) is verified against the pre-layout, post-synthesis netlist.
What is global clocking in Formal Verification?
Ans. A clocking block may be declared as the global clocking for all or part of the design hierarchy. The main purpose of global clocking is to specify which clocking event in simulation corresponds to the primary system clock used in formal verification (see F.3.1). Such a specification may be done for a whole design, or separately for different subsystems in a design, when there are multiple clocks and building a single global clocking event is challenging.
What is ‘witness’ in Formal Verification?
Ans. A ‘witness’ is a sequence of input vectors that makes the property true while satisfying all the constraints. ‘Witness’ makes sure that the property is reachable at least once before all the possible state space have been reached by the formal tool. If the property hits first scenario, satisfying the property fully, we can say that a ‘witness’ is found.
‘Witness’ doesn’t depend on the status of the property. Even if the property gets falsified, witness can still be reached or found.
If witness is unreachable then it means that the property is always falsified.
What is ‘counterexample’ in Formal Verification?
Ans. When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexample trace, in order to visually identify the failure that it demonstrates.