Global SEC check

docs/user/FlowVariables.md

@@ -275,7 +275,7 @@ configuration file.
 | <a name="SC_LEF"></a>SC_LEF| Path to technology standard cell LEF file.| |
 | <a name="SDC_FILE"></a>SDC_FILE| The path to design constraint (SDC) file.| |
 | <a name="SEAL_GDS"></a>SEAL_GDS| Seal macro to place around the design.| |
-| <a name="SEC_CHECK"></a>SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. If this fails, report an issue to OpenROAD.| 0|
+| <a name="SEC_CHECK"></a>SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hard macros, the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM macros, are checked as black boxes (proof boundaries): they are the same cells in both netlists and their abstracts carry no logic. If this fails, report an issue to OpenROAD.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)|
 | <a name="SETUP_MOVE_SEQUENCE"></a>SETUP_MOVE_SEQUENCE| Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.| |
 | <a name="SETUP_SLACK_MARGIN"></a>SETUP_SLACK_MARGIN| Specifies a time margin for the slack when fixing setup violations. This option allows you to overfix or underfix(negative value, terminate retiming before 0 or positive slack). See HOLD_SLACK_MARGIN for more details.| 0|
 | <a name="SKIP_ANTENNA_REPAIR"></a>SKIP_ANTENNA_REPAIR| Skips antenna repair entirely.| 0|

flow/designs/asap7/chi_async_bridge/config.mk

@@ -37,3 +37,7 @@ export VERILOG_TOP_PARAMS     = REQ_W 32 RSP_W 16 DAT_W 64 SNP_W 24 DEPTH 4
 else ifeq ($(FLOW_VARIANT),medium)
 export VERILOG_TOP_PARAMS     = DEPTH 4
 endif
+
+# Temporary disabling: the asynchronous clock-domain crossings are outside
+# the sequential check.
+export SEC_CHECK = 0

flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk

@@ -55,3 +55,7 @@ export PDN_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/pdn.tcl
 
 export BLOCKS = I2cDeviceCtrl
 
+
+# Temporary disabling: the bidirectional IO pads are outside the sequential
+# check.
+export SEC_CHECK = 0

flow/designs/nangate45/mempool_group/config.mk

@@ -78,3 +78,7 @@ export CORE_AREA   = 10 12 1090 1090
 export RTLMP_MIN_CHANNEL_SIZE = 20 20
 
 export SYNTH_HDL_FRONTEND = slang
+
+# Temporary disabling: the hierarchical netlist leaves memory write-mask pins
+# undriven, which the sequential check cannot verify.
+export SEC_CHECK = 0

flow/designs/sky130hd/chameleon/config.mk

@@ -50,3 +50,7 @@ export FP_PDN_RAIL_OFFSET = 0
 export TNS_END_PERCENT    = 100
 
 export RTLMP_MIN_CHANNEL_SIZE = 70 70
+
+# Temporary disabling: the hard macros carry no logic in their Liberty, which
+# leaves no output for the sequential check to verify.
+export SEC_CHECK = 0

flow/designs/sky130hd/microwatt/config.mk

@@ -51,5 +51,7 @@ endif
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-# Temporary disabling
+# Temporary disabling: the hierarchical netlist is rejected by the
+# equivalence checker (duplicate wire declaration).
 export LEC_CHECK = 0
+export SEC_CHECK = 0

flow/platforms/ihp-sg13g2/config.mk

@@ -168,7 +168,7 @@ export KLAYOUT_DRC_FILE ?= $(PLATFORM_DIR)/drc/sg13g2_minimal.lydrc
 export CDL_FILE ?= $(PLATFORM_DIR)/cdl/sg13g2_stdcell.cdl
 #export KLAYOUT_LVS_FILE = $(PLATFORM_DIR)/lvs/$(PLATFORM).lylvs
 
-export REMOVE_CELLS_FOR_LEC ?= "bondpad_70* sg13g2*"
+export REMOVE_CELLS_FOR_LEC ?= "bondpad_70*"
 
 # ---------------------------------------------------------
 #  Final

flow/scripts/formal_check.tcl

@@ -67,6 +67,86 @@ proc write_lec_script { step file1 file2 } {
   close $outfile
 }
 
+# Hardened sub-blocks (BLOCKS) enter the parent netlist as timing-only
+# abstracts with no logic model, so a formal check would treat every output
+# cone that reaches one as opaque. Return the instance paths of all block
+# instances in the loaded design; both netlists come from the same run, so the
+# same path exists in both and each instance can be paired with itself.
+# Escapes every unescaped `/` in an instance name as `\/`, the OpenSTA SDC
+# convention kepler-formal reads: `/` separates hierarchy levels and `\/` is a
+# literal slash inside one name. Existing escapes are kept as they are.
+proc formal_escape_slashes { name } {
+  set escaped ""
+  set length [string length $name]
+  for { set i 0 } { $i < $length } { incr i } {
+    set ch [string index $name $i]
+    if { $ch eq "\\" } {
+      incr i
+      append escaped "\\" [string index $name $i]
+    } elseif { $ch eq "/" } {
+      append escaped "\\/"
+    } else {
+      append escaped $ch
+    }
+  }
+  return $escaped
+}
+
+# Mirrors dbNetwork::stripParentPrefix: in a hierarchical database write_verilog
+# names a leaf by what follows the last unescaped `/` of its database name.
+proc formal_strip_parent_prefix { name } {
+  set pos [string last "/" $name]
+  while { $pos >= 0 } {
+    if { $pos == 0 || [string index $name [expr { $pos - 1 }]] ne "\\" } {
+      return [string range $name [expr { $pos + 1 }] end]
+    }
+    set pos [string last "/" $name [expr { $pos - 2 }]]
+  }
+  return $name
+}
+
+# Boundary path of a block instance exactly as write_verilog names it: in a flat
+# database the whole instance name is one leaf (`\u0/r0 ` in Verilog, so the
+# path is `u0\/r0`); in a hierarchical database the leaf keeps its module
+# instance path and loses the parent prefix. Paths are never reinterpreted.
+proc formal_boundary_path { inst } {
+  set name [$inst getName]
+  set prefix ""
+  if { [[ord::get_db] hasHierarchy] } {
+    set mod_inst [[$inst getModule] getModInst]
+    if { $mod_inst != "NULL" } {
+      set prefix "[$mod_inst getHierarchicalName]/"
+    }
+    set name [formal_strip_parent_prefix $name]
+  }
+  return "$prefix[formal_escape_slashes $name]"
+}
+
+# Hard macros are proof boundaries: the instances of the masters listed in
+# BLOCKS, and every instance of a BLOCK-class master (SRAM macros, hardened
+# sub-blocks). A macro is the same cell in both netlists, so only its
+# connections need checking; expanding its contents into state would only make
+# the proof slower.
+proc formal_block_instance_paths { } {
+  set paths {}
+  set blocks {}
+  if { [env_var_exists_and_non_empty BLOCKS] } {
+    set blocks $::env(BLOCKS)
+  }
+  set block [ord::get_db_block]
+  foreach inst [$block getInsts] {
+    set master [$inst getMaster]
+    if { [$master isBlock] || [lsearch -exact $blocks [$master getName]] >= 0 } {
+      lappend paths [formal_boundary_path $inst]
+    }
+  }
+  return [lsort $paths]
+}
+
+proc formal_yaml_quote { text } {
+  return "\"[string map {\\ \\\\ \" \\\"} $text]\""
+}
+
 proc write_sec_script { step file1 file2 } {
   set outfile [open "$::env(OBJECTS_DIR)/${step}_sec_test.yml" w]
   puts $outfile "format: verilog"
@@ -79,6 +159,17 @@ proc write_sec_script { step file1 file2 } {
   foreach libFile $::env(LIB_FILES) {
     puts $outfile " - $libFile"
   }
+  # Each macro instance becomes a proof boundary: its input pins are compared
+  # across the two netlists and its output pins are shared free inputs, so the
+  # macro is checked as a black box instead of hiding the cones behind it.
+  set boundaries [formal_block_instance_paths]
+  if { [llength $boundaries] > 0 } {
+    puts $outfile "set_as_boundary:"
+    foreach path $boundaries {
+      set quoted [formal_yaml_quote $path]
+      puts $outfile "  - \[$quoted, $quoted\]"
+    }
+  }
   puts $outfile "log_file: $::env(LOG_DIR)/${step}_sec_check.log"
   close $outfile
 }

flow/scripts/variables.yaml

@@ -1677,9 +1677,12 @@ LEC_CHECK:
 SEC_CHECK:
   description: >
     Perform a sequential equivalence check between the initial synthesis
-    netlist and final netlist with the Kepler Formal PDR engine. If this
-    fails, report an issue to OpenROAD.
-  default: 0
+    netlist and final netlist with the Kepler Formal PDR engine. Hard macros,
+    the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM
+    macros, are checked as black boxes (proof boundaries): they are the same
+    cells in both netlists and their abstracts carry no logic. If this fails,
+    report an issue to OpenROAD.
+  default: $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)
   stages:
     - synth
     - final