Skip to content

ci: add yosys synth_xilinx check to the emit bit-exact gate - #1871

Merged
gHashTag merged 2 commits into
masterfrom
feat/emit-synth-gate
Aug 7, 2026
Merged

ci: add yosys synth_xilinx check to the emit bit-exact gate#1871
gHashTag merged 2 commits into
masterfrom
feat/emit-synth-gate

Conversation

@gHashTag

@gHashTag gHashTag commented Aug 7, 2026

Copy link
Copy Markdown
Owner

The gate proved semantic equivalence (iverilog bit-exact) but not that the emitted RTL synthesizes — a change can stay bit-exact in sim yet break synthesizability and only fail when a bitstream is attempted on silicon.

verify_emit_bitexact.py now runs yosys synth_xilinx -nocarry -flatten on the microsequencer for one single-output (2,2,1) and one multi-output (2,4,2) topology, asserting no yosys error AND a non-zero FF+LUT mapping (a design DCE'd to nothing would 'pass' an empty-module sim but map to 0 cells). Measured: (2,2,1) → 3273 FF + 7752 LUT, (2,4,2) → 6453 FF + 10161 LUT. Synth phase runs only if yosys is present; the workflow now installs it alongside iverilog. Every PR touching the generator now proves both spec→RTL bit-exactness AND synthesizability. Refs #1764

The gate proved semantic equivalence (iverilog bit-exact) but not that the emitted
RTL synthesizes -- a change can stay bit-exact in sim yet break synthesizability and
only fail when a bitstream is attempted on silicon. verify_emit_bitexact.py now runs
yosys synth_xilinx -nocarry -flatten on the microsequencer for one single-output
(2,2,1) and one multi-output (2,4,2) topology, asserting no yosys error and a
non-zero FF+LUT mapping (a design DCE'd to nothing would pass an empty-module sim
but map to 0 cells). Measured: (2,2,1) -> 3273 FF + 7752 LUT, (2,4,2) -> 6453 FF +
10161 LUT. Synth phase runs only if yosys is on PATH; the workflow now installs it
alongside iverilog. Every PR touching the generator now proves both spec->RTL
bit-exactness AND synthesizability to real Xilinx cells.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-07 13:23:57 UTC

Summary

Status Count
Total Open PRs 12
PRs with Failing Checks 0
PRs with All Checks Green 12
READY 5
FAILING 0
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=4c1aaad5309a != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

CI's apt yosys reported FF=0 LUT=0 while the local oss-cad-suite yosys passed:
the stat total is printed as 'N cells' (not 'Number of cells:'), and some yosys
builds log stat to stderr rather than stdout. Parse the total from both formats
and from stdout+stderr combined; assert on the version-stable total cell count
(>=200) rather than per-primitive FF/LUT names (which are informational). The
failure branch now dumps the real stat tail for diagnosis.

Refs #1764

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

@github-actions

github-actions Bot commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-07 13:36:02 UTC

Summary

Status Count
Total Open PRs 12
PRs with Failing Checks 0
PRs with All Checks Green 12
READY 5
FAILING 0
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=4c1aaad5309a != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag
gHashTag merged commit c2c6047 into master Aug 7, 2026
18 checks passed
@gHashTag
gHashTag deleted the feat/emit-synth-gate branch August 7, 2026 13:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant