A Small Formality Tutorial

• What is Formality?

The Formality User Guide should be your 1st reference.

"Formality is an application that uses formal techniques to prove or disprove the functional equivalence of two designs or two technology libraries. For example, you can use Formality to compare a gate-level netlist to its register transfer level (RTL) source or to a modified version of that gate-level netlist. After the comparison, Formality reports whether the two designs or technology libraries are functionally equivalent. The Formality tool can significantly reduce

your design cycle by providing an alternative to simulation for regression testing.

The techniques Formality uses are static and do not require simulation vectors. Consequently, for design verification you only need to provide a functionally correct, or “golden,” design (called the reference design) and a modified version of the design (called the implementation design). By comparing the implementation design against the reference design, you can determine whether they are functionally equivalent to each other. Technology library verification is similar except that each cell in the implementation library is compared against each cell in the reference library one cell at a time."

• How to run the 1st tutorial example?

The following steps for command line. However, fm_shell -gui may be better for your experiment. Assume you are installing Formality (fm) in /tools/synopsys/fm/C-200906_sp1 and Design Compiler (DC or syn) in /tools/synopsys/syn/C-200906-SP1, then

1. install Formality and Design Compiler

2. set designware directoty to DC

set hdlin_dwroot /tools/synopsys/syn/C-200906-SP1

3. read_verilog -container r -libname WORK -vcs "+libext+.v" -01 { /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/RTL/gray2bin.v /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/RTL/gray_counter.v /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/RTL/rs_flop.v /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/RTL/fifo.v /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/RTL/pop_ctrl.v /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/RTL/push_ctrl.v }

4. set_top r:/WORK/fifo

5. read_verilog -container i -libname WORK -01 { /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/GATE/fifo.vg }

6. read_db { /tools/synopsys/fm/C-200906_sp1/doc/fm/tutorial/LIB/lsi_10k.db }

7. set_top i:/WORK/fifo

8. match

9. verify

10. diagnose

11. remove_container r

12. remove_container i

13. remove_library -all

• Useful commands

1. set default parameters

set verification_blackbox_match_mode identity

set verification_set_undriven_signals PI

set verification_passing_mode consistency

2. avoid errors and warnings

set hdlin_error_on_mismatch_message false

set hdlin_unresolved_modules black_box

set hdlin_ignore_full_case false

set hdlin_ignore_parallel_case false

3. see memory and cpu

memory

cputime

The OPENCAD Formality UI document is also a good reference to see examples.