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

synthesize the design with dc_shell

 $rake asic:fpu 

launch formality, and hope for the best

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.

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...