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

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.

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

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