Remote Fm Formality

CRITICAL: Always Copy from Example Template

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

Step 1: Copy template structure

# 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"

Step 2: Modify only 1 thing in .synopsys_fm.setup

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

Step 3: Run

ssh user@server "cd /project/fm_new && make run"

Project Directory Structure

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

Verified Template Files (from example)

.synopsys_fm.setup — Complete verified template

set 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 template

IMPORTANT: 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