From e2cbc3a38d2dac0187d539ae59cad9dff54b82d5 Mon Sep 17 00:00:00 2001 From: Emin Date: Wed, 9 Sep 2026 10:42:51 +0800 Subject: [PATCH 1/4] fix(lec): keep public wire names for equiv_make cut-points opt_clean -purge in normalize_design stripped internal public wire names, so equiv_make only created port-level $equiv cells and induction had no internal cut-points: every output stayed unproven (pm32: 65/65). Drop -purge so find_same_wires matches internal nets across gold/gate; pm32 now proves 202/202 equiv cells and the flow continues past LEC. --- chipcompiler/tools/yosys_lec/scripts/run_lec.tcl | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl b/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl index ea9175e9..338cf6b5 100644 --- a/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl +++ b/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl @@ -29,7 +29,9 @@ 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 } proc build_design {stash_name top_design netlist_file} { From ccf5044e1963795209a163a6d12492f59d0f434b Mon Sep 17 00:00:00 2001 From: Emin Date: Wed, 9 Sep 2026 23:36:06 +0800 Subject: [PATCH 2/4] fix(lec): hide FF D-input nets from equiv_make matching Newer yosys synthesis names FF D-input nets after the register (_reg_p_D), so equiv_make's find_same_wires pairs them across gold/gate. They are not equivalent: the golden FF keeps its clock enable while dfflibmap emulates it with a mux in the gate D cone, and such false cut-points stay unproven (pm32 on yosys 0.68: 104 unproven). True D-net matches on plain FFs are likewise unprovable once QN-output cells remove the Q-wire names. Hide D-input nets of all FF/latch cells from matching; FF equivalence is carried by the Q-output wire matches. Verified with the 0.1.0-alpha.12 bundle on pm32: yosys 0.62 and oss-cad-suite 2026-08-27 (0.68+132) both prove 171/171. --- chipcompiler/tools/yosys_lec/scripts/run_lec.tcl | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl b/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl index 338cf6b5..67d87733 100644 --- a/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl +++ b/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl @@ -32,6 +32,12 @@ proc normalize_design {top_design} { # 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} { From a78477a714500a9f56193a7678122a4e6f355a75 Mon Sep 17 00:00:00 2001 From: Emin Date: Wed, 9 Sep 2026 23:36:46 +0800 Subject: [PATCH 3/4] fix(yosys): avoid QN-only DFF cells so LEC keeps FF output names Newer yosys dfflibmap prefers inverted-output (QN) variants on area ties; the functional Q net is then renamed through the output inverter and the mapped netlist loses the FF output wire names that yosys LEC uses as induction cut-points. Exclude QN-only cells from the first dfflibmap pass (discovered generically from dfflibmap -info output); FF types without a Q-output alternative are still mapped by the second pass. Verified with the 0.1.0-alpha.12 bundle on pm32: yosys 0.62 and oss-cad-suite 2026-08-27 (0.68+132) both pass synthesis LEC. --- .../tools/yosys/scripts/yosys_synthesis.tcl | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl b/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl index bd02cdd4..bfc1954a 100644 --- a/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl +++ b/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl @@ -477,7 +477,30 @@ if {[info exists golden_netlist_file] && $golden_netlist_file ne ""} { # 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 From d6f8ca68999af8ddffe1d1d72a30babd3c0b01eb Mon Sep 17 00:00:00 2001 From: Emin Date: Thu, 10 Sep 2026 17:20:47 +0800 Subject: [PATCH 4/4] feat(lec): record FF cut-point contract in synthesis, replay in LEC Name-based cut-point matching depends on yosys' incidental net naming, which changes between versions (0.62 vs 0.68 differed on both FF D-net and Q-net names). Synthesis now records an explicit contract: for every flip-flop (stable instance name from rename -wire), the Q-output net name at golden-write time and at final-netlist time, written to lec_cutpoints.txt next to the golden netlist. Recording runs on a flattened throwaway copy (design -push-copy/-pop) so names match the LEC script's normalized view. run_lec.tcl replays the pairs with equiv_add before opt_clean -purge (which may merge aliased wires). yosys_lec.builder derives the sidecar path from the golden netlist path and selects the golden column per step: postRouteLec's golden side is the mapped netlist, so it reads the gate column. Verified on pm32 and NPC (RISC-V CPU) with yosys 0.62 and oss-cad-suite 2026-08-27 (0.68+132): all four prove fully, and a golden netlist with all 106 internal cut-point names artificially drifted still proves 171/171 via the contract. --- .../tools/yosys/scripts/yosys_synthesis.tcl | 71 +++++++++++++++++++ chipcompiler/tools/yosys_lec/builder.py | 7 ++ .../tools/yosys_lec/scripts/run_lec.tcl | 31 +++++++- test/yosys_lec/test_tools_yosys_lec.py | 43 ++++++++++- 4 files changed, 150 insertions(+), 2 deletions(-) diff --git a/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl b/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl index bfc1954a..043702d6 100644 --- a/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl +++ b/chipcompiler/tools/yosys/scripts/yosys_synthesis.tcl @@ -470,7 +470,62 @@ 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} } @@ -666,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} diff --git a/chipcompiler/tools/yosys_lec/builder.py b/chipcompiler/tools/yosys_lec/builder.py index 1aebc9a3..d69f7244 100644 --- a/chipcompiler/tools/yosys_lec/builder.py +++ b/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)) diff --git a/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl b/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl index 67d87733..572fac2b 100644 --- a/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl +++ b/chipcompiler/tools/yosys_lec/scripts/run_lec.tcl @@ -62,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 ""} { @@ -72,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} { diff --git a/test/yosys_lec/test_tools_yosys_lec.py b/test/yosys_lec/test_tools_yosys_lec.py index 33cf746a..364ea5c3 100644 --- a/test/yosys_lec/test_tools_yosys_lec.py +++ b/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)