ci: add yosys synth_xilinx check to the emit bit-exact gate - #1871
Merged
Conversation
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>
Contributor
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>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-07 13:36:02 UTC
Summary
Seal Status
|
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
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.
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.pynow runsyosys synth_xilinx -nocarry -flattenon 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