Conversation
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.
Open
5 tasks
Newer yosys synthesis names FF D-input nets after the register (<name>_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.
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.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What Changed
Scope
Select the areas touched by this PR:
uv.lock, or release artifacts.Runtime And Packaging Impact
ecc-toolsorecc-dreamplacedependency changedNotes:
Validation
List the commands you ran. Mark checks that are not applicable as N/A.
uv run pytest test/uv run ruff check chipcompiler testuv run ruff format --check chipcompiler testecc --help,ecc --version,ecc version --jsonnix run .#cli -- --helpecc runSkipped checks and reason:
Checklist