Logic Equivalence Check

Formal Verification :

It's also called as "Logic Equivalence Check". It checks the functionality equivalence of the implementation design with reference design (golden design). It checks and verifies multiple rules which are configured for equivalence check and errors out if any mismatches are found between the designs. It ignores timing information.

Formal verification is done before and after of,

• Logical Synthesis
• Physical Synthesis
• Place and Route

It can be performed after every stage of PnR.

Logical Synthesis :

Reference : RTL file

Implemented : Synthesized netlist / Gate level netlist

Physical Synthesis :

Reference : RTL file

Implemented : Synthesized and modified netlist

Place and Route :

Reference : Synthesized netlist

Implemented : Netlist extracted from optimized routed design

Steps involved :

• Read
• Match
• Verify
• Debug

Read :

Reads and breaks both the designs into Logic cones and Compare points.

(*For low power designs, the UPF's of reference and implementation design are to be loaded)

Logic cones : Block of combo logic that drives a compare point. Logic cones are bordered by registers, ports and black boxes. The output of logic cone is considered as a compare point.

Compare points :

• Primary outputs (Output ports)
• Register input pin
• Black box input pin

Inputs of logic cones :

• Primary inputs (Input ports)
• Register output pin
• Black box output pin

Eg : The combo connected in between two registers is considered as a logic cone, where both the registers here act as compare points.

 

Match :

Aligns the corresponding compare points between the two designs.

Eg : maps the registers with the same name in both the designs.

Cones won't match if the identical compare point in reference design doesn't exist in the implemented design.

(*Note : Tool won't match the objects of incompatible types. Eg : It won't match an input port to a flip flop)

Verify :

Checks the functionality between each compare point pair.

Cones are said to be perfect (passed) if the functionality between the two compare points is same for both the designs.

Debug / Diagnose :

Analyze the reports, GUI and debug the compare points.

The basic flow that includes above mentioned steps :

Read .svf file

⇓

Read reference design and libraries

⇓

Link design

⇓

Load UPF

⇓

Read implemented design and libraries

⇓

Link design

⇓

Load UPF

⇓

Match

⇓

Verify

⇓

Debug (If verify fails)

 

.svf (Standard Variation Format) file is generated automatically by the tool at the time of optimization and it contains the modifications done while optimizing. So, it is mandatory to load when performing formal verification.

 

.svf file contains,

• object name changes
• register optimizations
• duplicate and merged registers
• datapath transformations
• retiming
• register phase inversion
• clock gating information
• boundary scanning
• internal scanning (conversion of FF into SEFF)
• black boxes

Difference between Formal verification and Traditional simulation :