Use when running Synopsys Formality (FM) formal verification on a remote Linux server. First copy from example template, then modify per design. Covers project setup, SVF integration, execution, and result analysis.
Run formal equivalence verification (FEV) using Synopsys Formality on a remote Linux server. Verifies that DC synthesis output (gate-level netlist) is functionally equivalent to the original RTL, using SVF guidance from Design Compiler. Always copy from the verified example template first.
dc/svf/*.svf)dc/gate/*_netlist.v)fm_shell)The example template at ~/agent_digits/example/fm/ is a verified, working reference. Always copy from it to avoid syntax errors (especially set_top format).
# On remote server — copy entire fm directory structure
ssh user@server "cd /project && cp -r ~/agent_digits/example/fm/ ./fm_new && cd fm_new && rm -rf rpt/* log/* fss/* FM_INFO* formality_svf/* formality*.log fm_shell_command.log"
.synopsys_fm.setupssh user@server "sed -i 's/shift_reg_16bit/YOUR_MODULE_NAME/g' /project/fm_new/.synopsys_fm.setup"
Only change TOP_DESIGN_NAME. Library paths and set_top syntax are pre-configured.
ssh user@server "cd /project/fm_new && make run"
fm/
├── .synopsys_fm.setup # FM environment config (library, paths, variables)
├── Makefile # Run/clean commands
├── scr/
│ └── fm.tcl # Main FM verification script
├── rpt/ # Reports output
├── log/ # Log files
├── fss/ # Failed session (for debugging)
└── formality_svf/ # SVF produced by FM
.synopsys_fm.setup — Complete verified templateset synopsys_auto_setup true
set verification_clock_gate_hold_mode COLLAPSE_ALL_CG_CELLS
set verification_clock_gate_edge_analysis true
set verification_set_undriven_signals 0
set verification_failing_point_limit 0
set hdlin_dwroot /opt/synopsys/syn/V-2023.12
#**************************************** Library setup ***************************************************
set search_path [list "$TSMC_HOME/digital/Front_End/timing_power_noise/CCS/tcbn65lp_200a/" \
]
set lib_files [list tcbn65lptc_ccs.db \
tcbn65lptc1d21d2_ccs.db \
]
#**************************************** Library setup ***************************************************
#**************************************** Set Alias *******************************************************
# *** CHANGE THIS per design ***
set TOP_DESIGN_NAME "YOUR_MODULE_NAME"
set SVF "../dc/svf/${TOP_DESIGN_NAME}.svf"
set RTL_PATH "../dc/rtl"
set GATE_NETLIST "../dc/gate/${TOP_DESIGN_NAME}_netlist.v"
set search_path [concat ${RTL_PATH}\
${search_path}]
set RPT_UNMATCHED "./rpt/${TOP_DESIGN_NAME}_unmatched_points.rpt"
set RPT_MATCHED "./rpt/${TOP_DESIGN_NAME}_matched_points.rpt"
set RPT_FAILING "./rpt/${TOP_DESIGN_NAME}_verify_failing.rpt"
set RPT_PASSING "./rpt/${TOP_DESIGN_NAME}_verify_passing.rpt"
set SESSION "./fss/verify_failed.fss"
#**************************************** Set Alias *******************************************************
scr/fm.tcl — Complete verified templateIMPORTANT: This script uses the exact set_top syntax that works with Formality V-2023.12. Do NOT modify set_top format.
sh date
set_svf ${SVF}
foreach lib_file ${lib_files} {
set fm_shell_status [read_db -technology_library ${lib_file}]
if { $fm_shell_status == 0 } {
exit
}
}
set hostFiles [split [eval \ls -1 \
${RTL_PATH}/*.v \
]]
foreach filename ${hostFiles} {
set fm_shell_status [read_verilog -container r -libname WORK ${filename}]
if { $fm_shell_status == 0 } {
exit
}
}
set_top r:/WORK/${TOP_DESIGN_NAME}
read_verilog -container i -libname WORK ${GATE_NETLIST}
set_top i:/WORK/${TOP_DESIGN_NAME}
match
report_unmatched_points > $RPT_UNMATCHED
report_matched_points > $RPT_MATCHED
if {[verify]!=1} {
analyze_points -all > "./log/analyze_points.log"
report_failing > $RPT_FAILING
report_passing > $RPT_PASSING
save_session -replace $SESSION
}
sh date
exit
Makefile — Verified template