✨ Support sequential networks in write_aiger - #699
Open
marcelwa wants to merge 1 commit into
Open
Conversation
`write_aiger` hardcoded a latch count of 0 and asserted that the network was combinational, so `sequential<aig_network>` could be passed in but silently lost its registers: they degraded into extra PI/PO pairs. Emit registers as AIGER latches when the network type provides `num_registers`, `foreach_ri`, and `foreach_ro`. The combinational path is unchanged and still produces byte-identical output. Reset values are always written explicitly. An omitted reset field means 0 in the AIGER format, so omitting it would silently turn an uninitialized register into a zero-initialized one; an undefined reset is instead encoded by repeating the latch's own current-state literal, as the format prescribes. Latch names are emitted as `l<n>` symbol table entries, mirroring `on_latch_name`. Because the binary format encodes CIs implicitly, PIs must be variables 1..I and register outputs I+1..I+L. That invariant is now checked by a debug assertion rather than being silently assumed. Also add the missing `<cassert>` include; the header used `assert` but only compiled because its includers happened to provide it. Verified against both readers: the output round-trips through `aiger_reader` preserving register count, reset values, and names, and ABC reads it back with the expected `Init0`/`Init1`/`InitDC` counts. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #699 +/- ##
=======================================
Coverage 84.06% 84.07%
=======================================
Files 190 190
Lines 29468 29500 +32
=======================================
+ Hits 24773 24802 +29
- Misses 4695 4698 +3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
This was referenced Jul 28, 2026
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.
Description
write_aigerhardcoded a latch count of0and asserted the network was combinational,so a
sequential<aig_network>could be passed in but silently lost its registers — theydegrade into extra PI/PO pairs, and the assertion is a no-op in release builds.
This adds real latch support, gated on
num_registers/foreach_ri/foreach_roviaif constexpr. The combinational path is untouched and still produces byte-identicaloutput — the two pre-existing byte-exact tests pass unchanged.
Reset values
Reset values are now always written explicitly, which matters more than it first looks:
0in the AIGER format, so omitting it for anuninitialized register would silently convert it into a zero-initialized one.
repeating the latch's own current-state literal.
Verified in both directions — ABC reports the expected
Init0 = 1. Init1 = 1. InitDC = 1.for a network carrying one register of each kind, and the output round-trips through
aiger_readerpreserving register count, reset values, and names.CI ordering
The binary format encodes CIs implicitly, requiring variables
1..Ito be the primaryinputs and
I+1..I+Lthe register outputs. That invariant was previously assumedsilently; it is now documented and checked by a debug assertion.
Drive-by
Added the missing
<cassert>include. The header usesassertbut only ever compiledbecause its includers happened to provide it — a TU that includes
write_aiger.hppfirst currently fails to build.
Testing
Five new test cases in
test/io/write_aiger.cpp(26 assertions total), passing in bothdebug and
NDEBUGbuilds:0and1aiger_readerround trip preserving PI/PO/register counts and reset valuesl<n>and surviving a round tripContext: this came out of building a Python-side ABC bridge in
aigverse, where sequential designs could not be
handed to ABC at all because there was no way to write them. Offering it upstream since
it seems generally useful.
🤖 Generated with Claude Code
https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz