4.8. Formal Verification¶
Hammer supports post-synthesis and post-P&R formal verification. It provides a simple API to provide a set of reference and implementation inputs (e.g. Verilog netlists) to perform formal verification checks such as logical equivalence checking (LEC).
This action requires a tool plugin to implement HammerFormalTool
.
4.8.1. Formal Verification Setup Keys¶
Namespace:
vlsi.core
formal_tool_path
- Set to the directory containing the tool plugin directory for the formal tool, typically
/path/to/tool_plugin/formal
. This will be the parent directory of the directory containing__init__.py
anddefaults.yml
.
- Set to the directory containing the tool plugin directory for the formal tool, typically
formal_tool
- Actual name of the formal verification tool that is setup in the directory
formal_tool_path
, e.g.conformal
- Actual name of the formal verification tool that is setup in the directory
4.8.2. Formal Verification Input Keys¶
Namespace:
formal.inputs
check
(str)- Name of the formal verification check that is to be performed. Support varies based on the specific tool plugin. Potential check types/algorithms could be “lec”, “power”, “constraint”, “cdc”, “property”, “eco”, and more. At the moment, only “lec” is supported.
input_files
([])- A list of file paths to implementation source files (verilog, vhdl, spice, liberty, etc.) to be passed to the formal verification tool. For a LEC tool, this would be the sources for the “revised” design. The paths may be relative to the directory in which
hammer-vlsi
is called.
- A list of file paths to implementation source files (verilog, vhdl, spice, liberty, etc.) to be passed to the formal verification tool. For a LEC tool, this would be the sources for the “revised” design. The paths may be relative to the directory in which
reference_files
([])- A list of file paths to reference source files (verilog, vhdl, spice, liberty, etc.) to be passed to the formal verification tool. For a LEC tool, this would be the sources for the “golden” design. The paths may be relative to the directory in which
hammer-vlsi
is called.
- A list of file paths to reference source files (verilog, vhdl, spice, liberty, etc.) to be passed to the formal verification tool. For a LEC tool, this would be the sources for the “golden” design. The paths may be relative to the directory in which
top_module
(str)- Name of the top level module of the design to be verified.
4.8.3. Formal Verification Inputs¶
Running the syn-to-formal
action after running synthesis will automatically generate the Hammer IR required to pipe the synthesis outputs to the Hammer formal verification tool, and should be included in the Hammer call, as demonstrated in the “Post-Synthesis Formal Verification” command below. The same goes for post-place-and-route formal verification.
At this time, only netlists are passed to the formal verification tool. Additional files (SDCs, CPFs, etc.) are needed for more advanced formal verification checks but are not yet currently supported. Similarly, formal verification on the behavioral RTL is also not yet supported.
4.8.4. Formal Verification Outputs¶
The formal verification tool produces reports in OBJ_DIR/formal-rundir/
. Outputs from formal verification flows such as engineering change order (ECO) patches are not yet supported.
4.8.5. Formal Verification Commands¶
Synthesis to Formal Verification
hammer-vlsi -e env.yml -p config.yml -p OBJ_DIR/syn-rundir/syn-output.json -o OBJ_DIR/syn-to-formal_input.json --obj_dir OBJ_DIR syn-to-formal
Post-Synthesis Formal Verification
hammer-vlsi -e env.yml -p config.yml -p OBJ_DIR/syn-to-formal_input.json --obj_dir OBJ_DIR formal
P&R to Formal Verification
hammer-vlsi -e env.yml -p config.yml -p OBJ_DIR/par-rundir/par-output.json -o OBJ_DIR/par-to-formal_input.json --obj_dir OBJ_DIR par-to-formal
Post-P&R Formal Verification
hammer-vlsi -e env.yml -p config.yml -p OBJ_DIR/par-to-formal_input.json --obj_dir OBJ_DIR formal