my-probes #1

Merged

tampler merged 3 commits from comonoid/yosys-formal:my-probes into main

2026-07-03 00:39:49 +03:00

comonoid commented

2026-07-02 20:00:55 +03:00

Contributor

Problem

make dolec failed for both example designs with:

  ERROR: No SAT model available for async FF cell $procdff$7_gold ($adff).
         Consider running `async2sync` or `clk2fflogic` first.

Even past that error, the check could not have proven anything: the mapped
std cells were read only as Liberty blackboxes, so the SAT engine had no
logic models for them.

Root causes & fixes

Three independent issues in lec/*.ys:

Async-reset FFs. Both designs use always @(posedge clk or posedge reset), producing $adff cells on the gold side, which the SAT engine
cannot model. → added async2sync after equiv_make.
Blackbox std cells. read_liberty -lib ... -setattr blackbox gives
ports only, no functions — even a trivial INVX1 vs ~A check fails.
→ added tech/osu035/osu035_stdcells_sim.v with behavioral models
(functions taken verbatim from the Liberty file) and read it together
with the netlist.
Combinational-only proving. equiv_simple closes combinational
cones only. → added equiv_induct for the sequential equivalences.

Also fixed syn/*.ys: dropped the hardcoded /opt/oss-cad-suite/bin/yosys-abc
path so make dosyn uses the abc bundled with yosys.

Build-flow tidy-up

gen/*.v are now build artifacts: git-ignored, untracked, rebuilt on
demand (gen/.gitkeep + mkdir -p keep the flow working on a fresh clone).
Makefile: .PHONY, pattern rule so dolec re-synthesizes a stale
netlist automatically, make test (runs LEC for all designs), make help.
README: fixed the oss-cad-suite releases link, documented design=
override and the new targets.

Verification

make test: Equivalence successfully proven! for both designs
(counter 4/4, lfsr 31/31 $equiv cells), yosys 0.62.
Mutation-tested — the check is not vacuous: a swapped gate
(NAND→NOR), a swapped cell (XOR→XNOR), and swapped S/R pins on a DFFSR
each make LEC fail as expected; restoring the netlist makes it pass.
The DFFSR model matches the Liberty corner case (clear_preset_var1: L
— both set and reset active → Q=0).
Full flow verified on a fresh git clone (clean → synth → LEC).

Known limitation

osu035_stdcells_sim.v models the 15 cells the current examples map to,
not all 39 in the library. This is documented in the file header along
with how to extend it.

## Problem `make dolec` failed for both example designs with: ERROR: No SAT model available for async FF cell $procdff$7_gold ($adff). Consider running `async2sync` or `clk2fflogic` first. Even past that error, the check could not have proven anything: the mapped std cells were read only as Liberty blackboxes, so the SAT engine had no logic models for them. ## Root causes & fixes Three independent issues in `lec/*.ys`: 1. **Async-reset FFs.** Both designs use `always @(posedge clk or posedge reset)`, producing `$adff` cells on the gold side, which the SAT engine cannot model. → added `async2sync` after `equiv_make`. 2. **Blackbox std cells.** `read_liberty -lib ... -setattr blackbox` gives ports only, no functions — even a trivial `INVX1` vs `~A` check fails. → added `tech/osu035/osu035_stdcells_sim.v` with behavioral models (functions taken verbatim from the Liberty file) and read it together with the netlist. 3. **Combinational-only proving.** `equiv_simple` closes combinational cones only. → added `equiv_induct` for the sequential equivalences. Also fixed `syn/*.ys`: dropped the hardcoded `/opt/oss-cad-suite/bin/yosys-abc` path so `make dosyn` uses the abc bundled with yosys. ## Build-flow tidy-up - `gen/*.v` are now build artifacts: git-ignored, untracked, rebuilt on demand (`gen/.gitkeep` + `mkdir -p` keep the flow working on a fresh clone). - Makefile: `.PHONY`, pattern rule so `dolec` re-synthesizes a stale netlist automatically, `make test` (runs LEC for all designs), `make help`. - README: fixed the oss-cad-suite releases link, documented `design=` override and the new targets. ## Verification - `make test`: **Equivalence successfully proven!** for both designs (counter 4/4, lfsr 31/31 $equiv cells), yosys 0.62. - **Mutation-tested** — the check is not vacuous: a swapped gate (NAND→NOR), a swapped cell (XOR→XNOR), and swapped S/R pins on a DFFSR each make LEC fail as expected; restoring the netlist makes it pass. - The `DFFSR` model matches the Liberty corner case (`clear_preset_var1: L` — both set and reset active → Q=0). - Full flow verified on a fresh `git clone` (clean → synth → LEC). ## Known limitation `osu035_stdcells_sim.v` models the 15 cells the current examples map to, not all 39 in the library. This is documented in the file header along with how to extend it.

❤️ 1

comonoid added 3 commits

2026-07-02 20:00:55 +03:00

fix: make LEC prove equivalence for counter and lfsr 6d911e46e0

The LEC scripts failed in equiv_simple with
"No SAT model available for async FF cell $adff". Three issues:

- Async-reset FFs ($adff) have no SAT model. Add `async2sync` after
  equiv_make to lower them to synchronous form.
- The mapped std cells were read only as Liberty blackboxes, so the SAT
  engine had no logic for them (INVX1, DFFSR, ...) and couldn't prove
  anything. Add behavioral models in tech/osu035/osu035_stdcells_sim.v
  (functions taken from the Liberty file) and read them with the netlist.
- equiv_simple only closes combinational cones; add `equiv_induct` for the
  sequential equivalences.

Also drop the hardcoded /opt/oss-cad-suite abc path in the synthesis
scripts so `make dosyn` uses the abc bundled with yosys.

Both `make dolec design=counter` and `design=lfsr` now report
"Equivalence successfully proven!".

chore: tidy up build flow, gitignore, and docs a0a030cf37

- Makefile: add .PHONY, `all`, `test` (runs LEC for every design), and
  `help`; make `dolec`/`dosyn` rebuild the netlist via a pattern rule so a
  stale gen/<design>_mapped.v is re-synthesized automatically.
- Treat gen/*.v as build artifacts: git-ignore them and drop them from the
  index (they were tracked yet `make clean` deleted them).
- README: fix the oss-cad-suite releases link, document the design=
  override, `make test`/`make help`, and the std-cell sim models.
- Add trailing newlines to the LEC scripts.

fix: keep gen/ dir on fresh clone; note sim-lib scope 1c79651a37

Untracking gen/*.v left the gen/ directory empty, so git would not
recreate it on a fresh clone and `make dosyn` failed with
"Can't open output file gen/..._mapped.v".

- Makefile: `mkdir -p gen` in the synthesis rule so it works even if the
  directory is absent.
- Track gen/.gitkeep so the directory exists right after clone.
- Document that osu035_stdcells_sim.v models only the cells used by the
  current examples, and how to extend it.

comonoid force-pushed my-probes from 1c79651a37 to da6f90d2b2

2026-07-02 23:37:26 +03:00

Compare

comonoid force-pushed my-probes from da6f90d2b2 to 693ef32757

2026-07-02 23:51:42 +03:00

Compare