MASC/Formality

Formality Flow By Tom Golubev

Formality is a formal verification tool that allow quick verification of RTL vs netlist.

Rake now has the formality verify option

To Get started

Launch formality, and hope for the best.

Note: the ddc and SVF files generated from dc_shell need to be in the asic directory. See below for how to synthesize

 $rake verify:fpu   (You may need to add full=1 if the target is not in the .xml file.)

[Optional]

 synthesize the design with dc_shell
   $rake asic:fpu

GUI

To use the gui, launch with console support

 $rake verify:fpu console=1 v=1

use the start_gui command

 $fm_shell (setup)> start_gui

Now the gui shows up.

Some important features of the gui:

 Allow you to match unmatched ports manually.
 Help debug/analyze failing points using the cone schematic.
 Lower the learning curve.

COMMANDS

Launch verification with the console.

 $rake verify:fpu console=1 v=1

Note that the v=1 option has to be used, since we wouldn't want to send something to the grid that goes to the console.

Now the ./fm_fpu.sh file is created, launch it.

 $./fm_fpu.sh

report_black_boxes: reports the black boxes used in the design. black boxing failing sub-blocks is a strategy to pinpoint failure.

MATCHING

Sometimes Formality cannot match the input / output ports of the top-level when they are in System Verilog.

Use the gui for matching if possible. When a whole bus is to be matched, it is usually helpfull to use a bash one-liner to solve the problem.

 for i in `seq 5 36`; do echo set_user_match {r:/WORK/rachael_core/ibus_request[$i]} {i:/WORK/rachael_core/ibus_request\[data_wr][$(($i - 5))]} \ -noninverted -type port; done

Once you have all the rules correct, copy all commands from the console, and paste them into .xml file for the project. Rake will insert these into the Formality template and you will not have to do this again.

sample .xml entry. Note that xml is not indentation / tab sensitive. So it need not be indented.

 <verify base="rachael_core">
   <match>
     set_user_match {r:/WORK/rachael_core/ibus_request[1]} {i:/WORK/rachael_core/ibus_request\[we][0]} -noninverted -type port
     set_user_match {r:/WORK/rachael_core/ibus_request[2]} {i:/WORK/rachael_core/ibus_request\[we][1]} -noninverted -type port
     set_user_match {r:/WORK/rachael_core/ibus_request[3]} {i:/WORK/rachael_core/ibus_request\[we][2]} -noninverted -type port
     set_user_match {r:/WORK/rachael_core/ibus_request[4]} {i:/WORK/rachael_core/ibus_request\[we][3]} -noninverted -type port
   </match>
 </verify>

STRATEGIES

resynthesize without SYN_ASIC or STM90 defines.

 use sed to remove the -define from the .tcl file.

 For rachael_core this would be:
   dc_rachael_core.tcl

   sed -e s/"-define SYN_ASIC=1,USE_STM90=1"//g dc_rachael_core.tcl -i

 Replace the .tcl file with your design.

 rerun synthesis
   $./dc_rachael_core.sh

 Rerun verification.

Try hierarchical verification

 This will treat every sub-module as an independent unit.
 
 fm_shell (match)> write_hi -replace -match net -save_directory /mada/users/agolubev/scoore/projects/tapeout/rachael_rnode/ -save_file_limit 10 -save_time_limit 0 rachael_core_hier.tcl

 then source the file. NOTE: The GUI is very slow when many lines are to be printed, quit the gui, do an operation, then relaunch gui is need-be.
 fm_shell (match)> source rachael_core_hier.tcl

This will launch verification on many sub-modules, and you can continue debugging from there.

DEBUGGING

Many problem arise from undriven ports, using `ifdef SYN_ASIC in RTL...