Logical verification

During the development of a SoC there can be many stages of the design process that modify the representation of the gate-level netlists. These could be to ensure timing closure, to change the power use or many other design tasks. It is always important to re-verify that the current gate-level netlists still hold equivalence to the 'golden'  higher level (RTL) model description. This Logical verification stage may be executed many times and use a range of verification tasks to confirm the logical representation of the system. Verification can be by formal methods (mathematically correct) , generated tests and manually created tests. 

Logic Equivalence Checking

Logical Equivalence is a formal verification method that uses formal mathematical proofs to determine two representations of design perform the same logical functionality. The two representations are usually the Register Transfer Level (RTL) model description and the sythensized gate-level netlists. It is an important verification step to ensure the synthesis process did not introduce any functional discrepancies and that the transistors that will be fabricated in silicon perform the same logic functions and the RTL model. 

LEC breaks down the RTL design into logic cones and does the same with the Gate-level netlist. The tools then, by using a number of different means, try to find points of comparison and via formal methods, is able to prove that the logical function between two points is equivalent. There will usually be some tuning of scripts to make it compatible with the current technology and ignoring things such as clock gating cells and DFT logic which may have been inserted during the synthesis stage to ensure that the designs are equivalent. Once this has been proved mathematically, you can have confidence (as long as the flow is set up correctly) that the logic is verified. 

Here are some high level descriptions of some of the tools, please look on vendor documentation for more specific detail.

Cadence

The Cadence Conformal Equivalence Checking tools provide formal equivalence checking of designs from RTL down to place and route of gates. Any tool is only as good as the range of proof checkers that it contains. In the EC-XL configuration Cadence provides formal equivalence checking for digital logic, including complex arithmetic logic and datapaths, while the EC-GXL configuration is designed for custom circuits, including memories.

 

 

Synopsys

The Synopsys Formality Equivalence Checking tool uses Guidance to help the tool make sense of the process design changes made by various tools within the design flow. Formality obtains this Guidance information from files that are generated from the other tools. 

Synopsys ESP

Combines formal methods with event-driven simulation for verification of custom designs such as embedded memories, custom macros, standard cells and I/O cell libraries. It verifies the functional equivalence of the SPICE-level netlist against a behavioral or RTL representation of the design.

Please note this is not a form of overall system validation against requirements. If the functionality of the RTL is wrong, the functionality of the gate-level netlist is wrong too.

Gate level verification

Gate level verification can be used to ensure the Synthesis translation was correct and the design has not been altered or affected. It can also test low level entities such as power structures that are not represented in RTL descriptions and added during synthesis. Gate level verification use simulations operating on gate level netlists. Verification at this level is not usually exhaustive due to the time required to run such a gate level simulation. Test vectors can be prioritised, for example specific timing concerns not covered by Static Timing Analysis.