1.1.1. The Art of Equivalence Checking

Ever wonder why RTL to netlist verification is needed?
why is the process of Equivalence Checking (EC) so hard?

Read on.... :)

Logic Synthesis as a process is prone to Bugs. There are too many transformations happening in logic synthesis which can alter the netlist in a wrong manner and make it infer functionality other than what was intended in the original RTL. These bugs are not intentional but happen by accident during synthesis tool development. They can happen mostly during the elaboration stage as new verilog/VHDL constructs start showing up from time to time in new language standards. It takes time to build a robust Langauge analysis/elaboration engine as a front end to synthesis engine.

Now, How do we make sure we did not goof up our synthesis?

Simulation is not a robust proof of correctness as it was never intended to be exhaustive. However we can run the same functional vectors and check our netlist to see if we are lucky to catch a problem in gates. This is never a full proof verfication strategy.

Equivalence checking comes to the rescue. :). And it is fool proof. EC mathematically proves that the RTL and Netlist are equivalent and does not need functional vectors.

Most EC vendors give manuals along with the tools which explain how to configure these tools for various scenarios like

1. retiming
2. clock gating in Netlist
3. scan inserted netlist
4. Cut point insertion
5. Hierarchical verification/debug
6. Constant propagtion

to name a few. There might be more and the list is not comprehensive by any means. :)

The tools (Verplex/Fromality) also have a nice Debussy like interface to debug and pinpoint the cause of mismatch. These tools also write out failing vectors which can be used by a simulator for further debug.

EC does have it's set of difficulties when performing the following operations..

1. ACMP (Automatic compare point matching)
Before the proof starts, correspondence has to be established between the golden (RTL) and revised (Netlist) circuits. There are various techniques like name based matching, structural matching, prover based matching and ATPG to accomplish this.

2. verifying difficult SAT instances

3. Verifying data path components like Multipliers/dividers.

Operations are easier at word level (Binary Moment diagrams) than bit level for arithmetic circuits. However, the problem is in obtaining word level diagrams from bit level representation. Bit level operations on arithmetic circuits are very inefficient and memory/runtime intensive. ILP (Integer linear proramming) approaches are very popular but they fare poorly on control logic and work well on data path.

This is a very hot and active area of research in Formal community. :)

4. Difficulty in reaching counter examples as the generated counter example might not be reachable in normal circuit operation.

5. Equivalent cut point insertion

Formal tools internally find cut point equivalences to break a big problem into smaller sub problems to solve it more efficiently (using BDD + SAT). If cut point equivalnces are not correctly determined (most tools use ATPG for finding these equivalences), the formal tool may show false Negatives to the end user and create unnecessary panic!.

6. Identifying boundary nets for data path components (as they need to goto a different solver)

Most of these problems stem from the structural dis-similarities which exist between RTL and netlist as they come from 2 different (synthesis and Verification) engines.