fix(lec): keep public wire names for equiv_make cut-points

chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl

@@ -470,14 +470,92 @@ select -write ${timing_cell_stat_rpt} t:*DFF*
 tee -q -o ${timing_cell_count_rpt} select -count t:*DFF*
 tee -q -a ${timing_cell_count_rpt} select -count */t:*_DLATCH*_ */t:*_SR*_
 
+# Record FF instance -> Q net name on a flattened throwaway copy of the
+# current design. Structural FF detection (D + clock + Q ports), so it does
+# not depend on cell type naming. Returns a flat list: {cell qnet ...}.
+proc lec_record_ff_qnets {} {
+    design -push-copy
+    flatten
+    splitnets -ports -format _
+    set dump [tee -q -s result.string dump]
+    design -pop
+    set records [list]
+    set cur_name ""
+    set cur_qnet ""
+    set cur_has_d 0
+    set cur_has_clk 0
+    set cur_has_qn 0
+    foreach line [split $dump \n] {
+        if {[regexp {^[[:space:]]*cell (\S+) (\S+)[[:space:]]*$} $line -> ctype cname]} {
+            set cur_name $cname
+            set cur_qnet ""
+            set cur_has_d 0
+            set cur_has_clk 0
+            set cur_has_qn 0
+            continue
+        }
+        if {$cur_name eq ""} {
+            continue
+        }
+        if {[regexp {^[[:space:]]*connect \\(\S+) +\\?(\S+?)[[:space:]]*$} $line -> port net]} {
+            switch -- $port {
+                Q        { set cur_qnet $net }
+                QN       { set cur_has_qn 1 }
+                D        { set cur_has_d 1 }
+                C - CK - CLK { set cur_has_clk 1 }
+            }
+            continue
+        }
+        if {[regexp {^[[:space:]]*end[[:space:]]*$} $line]} {
+            if {$cur_qnet ne "" && $cur_has_d && $cur_has_clk && !$cur_has_qn} {
+                lappend records $cur_name $cur_qnet
+            }
+            set cur_name ""
+        }
+    }
+    return $records
+}
+
 if {[info exists golden_netlist_file] && $golden_netlist_file ne ""} {
+    # LEC cut-point contract: name-based matching in yosys LEC depends on
+    # incidental net names that change between yosys versions. Record an
+    # explicit contract instead: for every flip-flop (stable instance name
+    # from the rename above), the Q-output net name now (golden side) and at
+    # final-netlist time (gate side). yosys_lec replays the pairs with
+    # equiv_add. Recording runs on a flattened throwaway copy so the names
+    # match what the LEC script sees after its own flatten.
+    set lec_cutpoints_file [file join [file dirname $golden_netlist_file] lec_cutpoints.txt]
+    set lec_golden_records [lec_record_ff_qnets]
     yosys write_verilog -noattr -noexpr -nohex -nodec ${golden_netlist_file}
 }
 
 # technology mapping for clockgate
 clockgate {*}$tech_cells_args {*}$exclude_cells
 
+# Avoid QN-only (inverted-output) DFF cells: their functional Q net is renamed
+# through the output inverter, so the mapped netlist loses the FF output wire
+# names that yosys LEC uses as induction cut-points. dfflibmap -info reports
+# only one candidate per FF type, so iterate: exclude each inv pick until every
+# type maps to a non-inv cell or only inv variants remain. FF types without a
+# Q-output alternative are still mapped by the second pass below.
+set no_inv_cells [list]
+while {1} {
+    set dffmap_info [tee -q -s result.string dfflibmap -info {*}$tech_cells_args {*}$exclude_cells {*}$no_inv_cells]
+    set added 0
+    foreach line [split $dffmap_info \n] {
+        if {[regexp {^\s*cell (\S+) \(inv,} $line -> inv_cell]
+            && [lsearch -exact $no_inv_cells $inv_cell] < 0} {
+            lappend no_inv_cells -dont_use $inv_cell
+            set added 1
+        }
+    }
+    if {!$added} {
+        break
+    }
+}
+
 # technology mapping for flip-flops
+dfflibmap {*}$tech_cells_args {*}$exclude_cells {*}$no_inv_cells
 dfflibmap {*}$tech_cells_args {*}$exclude_cells
 
 # Follow mapped DFF cell names, not library filenames. For designs without
@@ -643,4 +721,20 @@ tee -q -o "${synth_stat_json}" stat -json -top $top_design {*}$liberty_args
 tee -q -o "${synth_check_rpt}" check -mapped
 
 # write synthesized design
+if {[info exists lec_cutpoints_file]} {
+    # Complete the LEC cut-point contract with the gate-side Q nets and write
+    # it next to the golden netlist for the yosys_lec step.
+    array set lec_gate_qnets {}
+    foreach {cname qnet} [lec_record_ff_qnets] {
+        set lec_gate_qnets($cname) $qnet
+    }
+    set lec_cutpoints_fh [open $lec_cutpoints_file w]
+    puts $lec_cutpoints_fh "# ff_cell golden_q_net gate_q_net"
+    foreach {cname qnet} $lec_golden_records {
+        set gate_qnet [expr {[info exists lec_gate_qnets($cname)] ? $lec_gate_qnets($cname) : "-"}]
+        puts $lec_cutpoints_fh "$cname $qnet $gate_qnet"
+    }
+    close $lec_cutpoints_fh
+    log "LEC cut-point contract written to $lec_cutpoints_file"
+}
 write_verilog -attr2comment -noexpr -nohex -nodec -defparam ${final_netlist_file}

chipcompiler/tools/yosys_lec/builder.py

@@ -126,6 +126,13 @@ def build_step_config(workspace: Workspace, step: YosysLecStep) -> None:
     config.set("top_design", tcl.word(workspace.design.top_module))
     config.set_path("golden_file", _path_text(step.input.golden_verilog))
     config.set_path("gate_file", _path_text(step.input.gate_verilog))
+    golden = step.input.golden_verilog
+    cutpoints = Path(golden).parent / "lec_cutpoints.txt" if golden else None
+    config.set_path("cutpoints_file", _path_text(cutpoints))
+    # postRouteLec's golden side is the mapped synthesis netlist, whose FF
+    # Q-net names live in the gate column of the cut-point contract.
+    golden_column = "gate" if step.name == "postRouteLec" else "golden"
+    config.set("cutpoints_golden_column", tcl.word(golden_column))
     config.set_path("report_dir", _path_text(step.report.dir))
     config.set_path("result_json", _path_text(step.output.json))
     config.set_path("status_file", _path_text(step.report.status))

chipcompiler/tools/yosys_lec/scripts/run_lec.tcl

@@ -29,7 +29,15 @@ proc normalize_design {top_design} {
     yosys async2sync
     yosys flatten
     yosys splitnets -ports -format _
-    yosys opt_clean -purge
+    # Keep public wire names: equiv_make uses them to create internal $equiv
+    # cut-points; -purge would strip them and leave induction without invariants.
+    yosys opt_clean
+    # Never name-match FF D-input nets: with the clock enable emulated by a
+    # mux in the gate-side D cone, same-named D nets are not equivalent, and
+    # such false cut-points are unprovable. FF equivalence is carried by the
+    # Q-output wire matches instead.
+    yosys rename -hide t:*DFF* %x:+\[D\] t:*DFF* %d
+    yosys rename -hide t:*DLATCH* %x:+\[D\] t:*DLATCH* %d
 }
 
 proc build_design {stash_name top_design netlist_file} {
@@ -54,7 +62,7 @@ proc write_failure_artifacts {reason} {
 }
 
 proc run_equivalence {} {
-    global top_design blacklist_file use_undef equiv_status_file
+    global top_design blacklist_file use_undef equiv_status_file cutpoints_file cutpoints_golden_column
     yosys design -copy-from gold -as gold $top_design
     yosys design -copy-from gate -as gate $top_design
     if {$blacklist_file ne ""} {
@@ -64,6 +72,35 @@ proc run_equivalence {} {
         yosys equiv_make gold gate equiv
     }
     yosys hierarchy -top equiv
+
+    # Replay the synthesis-recorded FF cut-points: an explicit contract that
+    # does not depend on yosys' incidental net naming. Must run before
+    # opt_clean -purge, which may merge aliased wires and rename them.
+    if {[info exists cutpoints_file] && $cutpoints_file ne "" && [file exists $cutpoints_file]} {
+        yosys cd equiv
+        # post-route LEC's golden side is the mapped synthesis netlist, which
+        # carries gate-column names.
+        set gcol [expr {[info exists cutpoints_golden_column] && $cutpoints_golden_column eq "gate" ? 2 : 1}]
+        set n_applied 0
+        set n_skipped 0
+        set cutpoints_fh [open $cutpoints_file r]
+        foreach line [split [read $cutpoints_fh] \n] {
+            set line [string trim $line]
+            if {$line eq "" || [string index $line 0] eq "#"} continue
+            set cols [split $line " "]
+            set gnet [lindex $cols $gcol]
+            set tnet [lindex $cols 2]
+            if {$gnet eq "-" || $tnet eq "-"} {
+                incr n_skipped
+                continue
+            }
+            yosys equiv_add -try "\\${gnet}_gold" "\\${tnet}_gate"
+            incr n_applied
+        }
+        close $cutpoints_fh
+        yosys log "LEC: replayed $n_applied synthesis cut-points ($n_skipped skipped)"
+    }
+
     yosys opt_clean -purge
 
     if {$use_undef} {

test/yosys_lec/test_tools_yosys_lec.py

@@ -53,7 +53,48 @@ def _write_gcd_netlist_pair(gate: Path) -> None:
     gate.with_name("gcd_Synthesis_golden.v").write_text(gcd_text)
 
 
-def test_yosys_build_step_exposes_rtl_derived_golden_path(tmp_path):
+def test_lec_config_wires_cutpoints_contract_for_synthesis_lec(tmp_path):
+    from chipcompiler.tools.yosys_lec import builder
+
+    workspace = _workspace(tmp_path)
+    gate = tmp_path / "Synthesis_yosys" / "output" / "gcd_Synthesis.v"
+    _write_gcd_netlist_pair(gate)
+
+    step = builder.build_step(
+        workspace=workspace,
+        step_name=StepEnum.LEC.value,
+        input_def=None,
+        input_verilog=gate,
+    )
+    builder.build_step_space(step)
+    builder.build_step_config(workspace=workspace, step=step)
+
+    config = step.data.config.read_text()
+    assert f"set cutpoints_file {gate.parent / 'lec_cutpoints.txt'}" in config
+    assert "set cutpoints_golden_column golden" in config
+
+
+def test_lec_config_selects_gate_column_for_post_route_lec(tmp_path):
+    from chipcompiler.tools.yosys_lec import builder
+
+    workspace = _workspace(tmp_path)
+    gate = tmp_path / "route_ecc" / "output" / "gcd_Routing.v"
+    gate.parent.mkdir(parents=True)
+    gate.write_text(GCD_RTL.read_text())
+
+    step = builder.build_step(
+        workspace=workspace,
+        step_name=StepEnum.POST_ROUTE_LEC.value,
+        input_def=None,
+        input_verilog=gate,
+        input_db=tmp_path / "Synthesis_yosys" / "output" / "gcd_Synthesis.v",
+    )
+    builder.build_step_space(step)
+    builder.build_step_config(workspace=workspace, step=step)
+
+    config = step.data.config.read_text()
+    assert "set cutpoints_golden_column gate" in config
+
     from chipcompiler.tools.yosys import builder
 
     workspace = _workspace(tmp_path)