LEC.pptx lectrure on lec formal tool for vlsi

formal verification

1. Agenda 1 Introduction LEC 2 Levels of LEC 3 Advantages of LEC 4 LEC flow using Cadence conformal LEC 5 Some issues in LEC

2. Introduction to Logic Equivalence Checking Generally design development undergoes numerous design iteration process These process has a potential to introduce the logical bugs in design Equivalence checking is formal verification technique used to check functional equivalence between two different versions of same design Some formal verification techniques used are: ROBDD SAT Does not guarantee that the initial design met the design specification Ignores timing information Only Boolean equivalence Reference/Golden and Implemented /Revised versions can be: RTL vs RTL RTL vs Netlist Netlist vs Netlist

3. RTL vs RTL module rtl_eq_eheck ( a,b,c,f ); input a,b,c ; output f; reg f; always @(a or b or c) begin f = ((a && b) || c); end endmodule module rtl_eq_eheck ( a,b,c,f ); input a,b,c ; output f; reg f; reg w1, w2; always @(a or b or c) begin w1 = (a && b); w2 = c; f = (w1 || w2); end endmodule Golden Revised Different design Implementation like ASIC design FPGA design

4. RTL vs Netlist module rtl_eq_eheck ( a,b,c,f ); input a,b,c ; output f; reg f; always @(a or b or c) begin f = ((a && b) || c); end endmodule a b c f Golden Revised This level of EC used post synthesis RTL to mapped netlist RTL to PnR netlist RTL to SPICE netlist

5. Netlist vs Netlist a b c f a b c f Golden Revised This level of EC used between mapped netlist to optimized netlist optimized netlist to scan stitched netlist scan stitched netlist to EDI netlist

6. Are the two circuits equivalent?

7. Non equivalent circuits

8. Advantages of LEC LEC use the formal verification technique, Formal Verification : A systematic method that uses mathematical proof to check the design’s properties Advantages of formal verification Enable "White box" verification No test vectors required Exhaustive verification Find bugs earlier Speed

9. LEC flow using Cadence Tool – Conformal LEC

10. Conformal LEC flow

11. LEC compare options A typical session compare(flat compare) Top down approach Hierarchical compare Bottom up approach

12. Starting and Exiting LEC Starting LEC GUI mode: UNIX%lec Non-GUI mode: UNIX% lec -nogui Switch GUI & non-GUI modes (anytime during LEC session ) LEC> set gui[on | off] Batch mode: UNIX % lec –dofile <batch_file> -nogui LEC> dofile <batch_file> Exiting LEC LEC>exit -force LEC automatically closes all windows upon exit

13. A typical flat compare Setup mode Saving LEC transcript to a log file Specifying black boxes Reading libraries and designs Specifying design constraints Specifying modeling directives Switching to LEC mode LEC mode Mapping process Resolving unmapped key points Compare process Debugging non-equivalent key points Report run statistics

14. Setup mode Black boxes Formal tool cannot deal with some blocks This logic is ignored by the tool Usually a Verilog module instance Examples Analog circuits “Hard IP ” Large embedded memories (register files, caches, etc.) and multipliers What is verified then? Drivers of black-box input pins Receivers of black-box input pins Internals of black box are ignored – be careful ! Commands used: add notranslate module m1 m2 mem * –both report black box

15. Setup mode – 1/4 Saving transcript set log file logfile_NAME –replace Reading libraries and design Library Verilog (standard simulation libraries) Liberty read library <filename …> [- verilog | -liberty] [-replace | -append] [-both | -golden | -revised] Design (Synthesizable RTL, gate, transistor) Verilog VHDL SPICE read design <filename …> [-file < verilog_command_file >] [- verilog | -verilog2k] [-golden | -revised]

16. Setup mode – 2/4 Design constraints What are design constraints? User’s inputs to control part of a design’s logic Purpose of constraints To disable test logic (for example; scan and JTAG) To specify one-hot or one-cold conditions To specify relationships between pins To constrain undrivensignals Example of constraints Pin constraint add pin constraint 0|1 signal_name [–revised | -golden] Instance constraint add instance constraint 0|1 inst1 [–revised | -golden] Pin equivalence add pin equivalence CLK –invert CLK_n -revised Tied signal add tied signal 0 GND -net -revised Undrivensignal set undriven signal 0 -revised

17. Setup mode – 2/4 Modeling directives In SETUP mode, user can specify directives to influence the way LEC models the design Modeling directives are needed to handle modeling styles specific to vendors libraries or synthesis tools Modeling options: Latch folding (set flatten model –latch_fold) Gated-clock (set flatten model –gated_clock) Sequential redundancy (set flatten model –seq_redundant) Sequential constant (set flatten model –seq_constant) Latch transparent (set flatten model –latch_transparent) Sequential merge (clock and data logic cones ) (set flatten model –seq_merge) Grounded clock (set flatten model –nodff_to_dlat_zero) DFF direct feedback (set flatten model –nodff_to_dlat_feedback)

18. Setup mode – 4/4 Switching to LEC mode Set system mode lec Flatten golden and revised designs Perform circuit modeling Map key points (automatic by default) LEC generates modeling messages after youchange mode to LEC You can turn off automatic mapping to read file containing mapped key points

19. LEC mode – 1/6 Mapping process Understanding mapping process What are key points? Key points: Primary Inputs, Primary Outputs, DFFs, cut gates, z-gates, blackbox. Logic cone: Design consists of combinational logic cones bounded by key points What is key point mapping? Pairing corresponding key points between golden and revised Why is key point mapping necessary? To match corresponding logic cones

20. LEC mode – 2/6 How is key point mapping done? Name based: mapping based on path name, net name, instance name etc. Function based: Mapping based on function and structure of logic cone. Command used: set mapping method –name only set mapping method – noname Mapping takes too long By default mapping in name based followed by function based mapping Function based mapping takes long time Incomplete mapping Unmapped points must be resolved Resolve mapping issues Use the following command add renaming rule r1 –revised

21. LEC mode – 3/6 Categories of unmapped points Extra: key points that only exits in one design that doesn’t affect the functionality. Unreachable: key point are not observable Not mapped: key point have no correspondence in other side. can be resolved by renaming rule Command: report unmapped points

22. LEC mode – 4/6 Compare process Understanding compare process How is state element handled? No connection between input and output. Both are verified separately What are the compare points? Sink points: primary output, DFF, Black box, cut gates What is being compared? Two designs are equivalent when all corresponding cones are equivalent Debugging non-equivalent key points Commands: add compare points –all compare

23. LEC mode – 5/6 report compare data –class […] Categories of compare report Equivalent Inverted Equivalent Non equivalent Abort Not compared

24. LEC mode – 6 /6 Debugging non-equivalent key points Diagnose smaller cone first Using the Mapping Manager to sort key points by supporting size Concentrate on one logic cone at a time Debugging tools Diagnosis Manager Schematic Viewer Source Code Manager Gate Manager

25. Some issues in LEC Formal tools are great at proving that one logic cone is equivalent to another Problem: matching up the cones in one input file with the cones in the other input file. If you can't figure out which cones are supposed to be equivalent, then the tool can't help you Normally done by matching up the signal names Done automatically Some tools alter signal names. Change the borders of cones No direct equivalence between cones in one file and the other Causes formal tool to do tedious process of matching up cones based on the topology of the network Very time-consuming