dbSta: hierarchy conformance and structural suites, with a 1282-netlist corpus - #11138
Open
gadfort wants to merge 21 commits into
Open
dbSta: hierarchy conformance and structural suites, with a 1282-netlist corpus#11138gadfort wants to merge 21 commits into
gadfort wants to merge 21 commits into
Conversation
Equivalence checking needs an oracle. kepler-formal is GPL-3.0 and OpenROAD is
BSD-3-Clause, so it is invoked as a subprocess and never linked: //src/tst:lec
builds the config, runs the binary, and classifies the verdict, linking nothing
of it.
It builds from source as a bazel dev_dependency, so a developer needs no manual
install and the tests cannot silently run against whatever binary happens to be
on $PATH. Two things make that work:
- //bazel:kepler.bzl carries a Starlark transition that strips `-xc++` from
cxxopts for kepler's subtree. OpenROAD sets that flag globally, and it
breaks cmake's compiler probe inside rules_foreign_cc, which kepler's
oneTBB dependency uses. The transition keeps the flag for OpenROAD's own
compilation, which is what it is there for.
- bazel/kepler-patches/ drops a linkopt that naja's python-embed leaks, which
would otherwise export a system library search directory into the link.
At run time lec.cpp resolves the binary from $KEPLER_FORMAL, then the test's
runfiles, then $PATH, so a locally installed binary still wins for anyone who
wants to point at their own build. A test that declares :kepler_formal_bin in
data always has it, so under bazel the tool is never missing and a LEC test can
never quietly degrade into a no-op.
Three details about reading kepler's output, all of which have been wrong at
some point and each of which fails silently rather than loudly:
- The SEC encoding is dual_rail_steady, not binary. Which one is sound
flipped between kepler revisions; the comment in lec.cpp records the
mutation battery that settled it.
- A proved verdict has two spellings. dual_rail_steady prints "No
binary-defined difference was found" where binary prints "No difference
was found", and matching only the first turns every pass into
"inconclusive".
- The verdict text is read BEFORE the exit status, and the exit status only
decides what an absent verdict means. kepler-formal used to exit 0 whether
it proved equivalence or found a difference; it now exits 3 on a
difference. An exit-code-first classifier therefore reports every genuine
inequivalence as a tool error, which is the worst direction to be wrong in:
it makes a real defect indistinguishable from a broken fixture.
The installer gains the host tools kepler's own build reaches outside bazel for
(bison, flex, m4, cmake, pkg-config, python3 headers); without them the failure
surfaces as an unhelpful repository-rule error inside a bazel fetch.
The tests for this land in the next commit, with the fixture they need.
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Contributor
Author
|
@QuantamHD FYI |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Code Review
This pull request integrates the kepler-formal equivalence checker as a Bazel dev dependency and introduces two comprehensive test suites, dbsta_hier_conformance and dbsta_hier_structural, to verify the logical and structural conformance of emitted netlists against input netlists. It also updates the dependency installer script to install the necessary host build tools. The reviewer feedback focuses on improving portability and robustness, specifically by recommending pkgconfig over pkgconf-pkg-config for RedHat-based distributions, replacing locale-dependent character classification functions with locale-independent ASCII checks, and utilizing std::filesystem::path instead of raw string concatenation for file path manipulation.
One netlist loaded through one link mode, owning its own db and sta, with read_verilog -> link_design [-hier] -> write_verilog behind three calls. It is deliberately separate from IntegratedFixture: a consumer that only wants to read, link and write a netlist should not link the optimization tool chain to do it, and the hierarchy conformance suites that follow want nothing else. The link mode is a constructor argument rather than two classes, so a test can run the same netlist both ways and attribute a difference to the mode. Errors surface as exceptions, since link_design reports failure by throwing from utl::Logger::error(), and a netlist that one mode refuses while the other accepts is itself a finding worth catching rather than a crash. TestLoadedDesign covers the fixture. TestLec covers the LEC wrapper from the previous commit and needs this fixture to produce a gate netlist, which is why the two arrive together: a proved pair, a real logic difference (an inverter where the gold has a buffer), and a dropped top-level port. The last two matter most -- both were once reported by kepler-formal with a zero exit code, and the inequivalent one now exits 3, so neither the exit status nor a bare "no difference" line can be trusted on its own. Their netlists live in TestNetlists.h and are written to the test's temp dir rather than checked in as .v files. The security pre-commit hook blocks *.v outside an allowlist of test directories and src/tst/test is not on it, no .v file having ever lived there. Inlining three small netlists costs nothing and buys something: the two defective variants are derived from the good one by a named edit, so the single difference each is testing is visible in the code rather than being a comment on a copy that can drift. The derivation throws if the text it edits is ever renamed, since a silent no-op would leave a "defective" fixture identical to the netlist it came from -- one that still runs and proves nothing. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Two suites over one corpus, both running read_verilog -> link_design [-hier] -> write_verilog and comparing the result against the INPUT netlist. dbsta_hier_conformance proves logical equivalence of each emitted netlist to the input, once per link mode. Deliberately not flat_out == hier_out: the flat dbNet view is built by mode-independent code, so a reader bug upstream of the hierarchy split corrupts both outputs identically and that comparison passes while both are wrong. Running the modes separately also gives attribution -- a hier-vs-flat mismatch says the two disagree but not which is wrong. dbsta_hier_structural diffs the emitted netlist against the input for the ten things a LEC cannot see: module set, top and submodule port order, declared nets, instance bindings, cell census, assigns, name identity, namespace rules, and whether the output can be read back at all. A netlist can be provably equivalent and still have its port list reordered, which silently miswires any parent that instantiates it positionally. Known failures are XFAIL rather than DISABLED_, so a fix turns the suite red with an actionable message instead of quietly leaving the case switched off. The list lives in hier_expected_fail.bzl, grouped by failure mode, and BUILD renders it into the manifest each suite reads. Keeping it in Starlark means Starlark can reject a malformed entry when the package loads: an unknown check or path, a ':' that would truncate the row, or one netlist listed twice under one key. Corpus membership is a directory scan, so adding a case is adding a file. What a folder listing cannot carry -- a case's top module -- lives in BUILD as HIER_TOP_OVERRIDES. This commit carries the fixtures that belong to the suites rather than to any one construct family: inherited/, symlinks to netlists other tests own, so a fixture written for rsz or odb is also held to conformance; structural/, cases only the structural suite can run because a LEC cannot adjudicate them (several are refused by the reader outright); and crash/, five netlists that kill the process and are therefore a data dependency of neither suite. Both suites guard against loading zero cases, because a corpus that silently resolved to nothing would make them vacuously green. That guard earns its keep immediately: the structural suite never had inherited/ in its data, so those 41 cases had never run under it. Adding the dependency turns up 22 rows' worth of structural failures in netlists other tests already own -- port reorders, a uniquification clone, and an added assign -- and the same guard now covers inherited/ so the hole cannot reopen. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
126 netlists written while establishing that the two link modes disagree at all. Each isolates one construct that crosses a hierarchy boundary: bus slices and part-selects handed to a submodule, feedthroughs at depths 1 to 4, aliases where an assign renames a net across a boundary, escaped identifiers, name order interacting with the writer, and instances whose ports are connected positionally. They are the cases that made the campaign worth running: the flat writer drops a submodule's bus-slice feedthrough assign and leaves two top outputs undriven, the hier writer hoists an internal feedthrough into the parent and double-drives a port, and a synthesized hierarchy path collides with a user's escaped name. All three are recorded here as XFAIL with the netlist that reproduces them. Each case carries a `// TARGETS:` header naming the constructs it exercises, which the suite lints: an authored case must declare what it is for, and two cases may share a target set only if their bodies differ. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
272 netlists covering a four-axis cross product exhaustively rather than by inspiration: hierarchy depth 1 to 4, signal shape (scalar, bus MSB-first, bus LSB-first, bus split across boundaries), port wiring (feedthrough, fanout, gated, partial), and identifier form (plain, bracketed, escaped-slash, mixed). A sweep like this is worth its size because the interesting failures live in the interaction, not in any one axis. Depth alone is uninteresting -- but a bracketed identifier on an LSB-first bus split across a depth-4 boundary exercises the path join, the bus regroup and the escape logic at once, and only the cross product reaches it. Generated cases are held to the same rule as authored ones: each declares its TARGETS, and the suite rejects two cases that declare the same targets and have identical bodies, so a generator that emits duplicates fails the build rather than inflating the corpus. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
185 netlists across the two families the campaign keeps finding defects in. bx_naming_* covers what an identifier can legally be and what OpenROAD does with it: escaped identifiers holding a slash, a bracket, a backslash, a dollar, a plus, a keyword, a leading digit or a name that differs from another only by case, in every object kind (module, instance, net, port, bus, bus bit, top) and at depths 1 to 4. Escaping is where the round trip is hardest to get right -- the writer must re-derive an escape the reader threw away -- and these record that it frequently does not: `wire wire;`, `output output;` and `INV_X1 assign (...)` all reach the emitted netlist unescaped. bx_collisions_* sets up the case nobody writes: a user object that ALREADY owns the name OpenROAD is about to synthesize. Flattening joins a hierarchy path with '/' and escapes the result, so instance x containing y becomes `\x/y ` -- which collides with a net literally named `\x/y `. Uniquification names a clone `sub_u1`, which collides with a module the user named `sub_u1`. The writer invents `_NC1` for an unconnected port, which collides with a wire named _NC1. Each of those is a line of the corpus, with the victim declared explicitly, because the collision is invisible without it. The emitted netlist in these cases is not merely ugly: it declares one name twice, which is illegal Verilog that OpenROAD itself silently merges on re-read, so two electrically distinct nets become one. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
201 netlists over the three signal shapes that survive a hierarchy boundary least well. bx_bus_geometry_* varies what a bus can be: descending and ascending ranges on either side of a boundary and mismatched between them, offset ranges ([7:4] into [11:8]), width-1 ranges where ascending and descending are the same thing, negative bounds, part-selects (nested, reversed, straddling a split), and concatenations mixing whole buses, bits and constants. A bus that crosses a boundary is re-derived on the far side from a range and an index, and every one of those variations is a chance to re-derive it differently. bx_constants_* covers tie-offs and literals, which have no driver to trace: a port tied to 1'b0 at depth 3, a literal in a concatenation, an assign whose right side is a constant, a bus tied to a sized or unsized literal in binary, decimal or hex, and a net a user named `1'b0`. Most of these are unprovable by construction -- a cone with no driver is one the oracle refuses -- which is itself worth recording, because it marks where the LEC is blind and the structural checker has to carry the case. bx_dangling_* covers what happens to what nothing reads: unconnected input and output ports, an instance with an empty connection list, dead assigns, undriven nets that leak across a boundary, and the _NC filler wires the writer invents for them. The filler generator consults nothing, so its names are also the subject of the collision cases in the previous commit. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
200 netlists completing the broad construct search. bx_port_rewiring_* is about connections that come back attached to the wrong thing. Positional connections on a hierarchical instance and on a liberty leaf cell, positional lists with a gap or a trailing empty slot, explicit named headers, concatenations and replications on a port connection, whole buses against bit-blasted ones, and submodules that permute their ports internally. Each drives every bit through a different gate, so a wrong binding lands a wrong value on a named output rather than cancelling out -- a permutation is invisible to a LEC if the permuted signals are interchangeable. bx_sequential_* puts flops and clock gates across the boundary: a clock net that crosses hierarchy, an escaped clock name that collides with a flattened path, a flop whose Q feeds back through a parent, and integrated clock gates. The clock-gate cases are XFAIL for a reason that is not OpenROAD's: the oracle cannot model CLKGATE_X1's arity, and they were previously "proved" only because an older build abstracted the latch away, so clock-gate semantics were never actually checked. bx_topology_* varies the shape rather than the signals: diamonds where two paths reconverge, siblings sharing a net, a module instantiated at three different depths, chains four deep, and modules whose instances are declared before the module itself. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
… constructs
87 netlists derived by reading the implementation and asking what each branch
would do wrong, rather than by enumerating Verilog constructs. Coverage is a
poor guide here: dbNetwork's hierarchical traversal is recursive, so a line can
be executed by nearly every case and still be wrong for a shape none of them
has.
The four groups name where they came from:
wb_sta_reader_* OpenSTA's Verilog reader -- attributes before an assign, a
`(* dont_touch = "true" *)` whose value is a string where
an int is parsed, a src line number that overflows, supply
nets, tri0/tri1, an empty specify block, a module that
shadows a liberty cell name.
wb_dbsta_link_* link_design itself -- unresolved modules, uniquified clones
whose names collide with the top or with a liberty cell,
escaped names whose tail looks like a bus, supply nets that
cross a hierarchy boundary.
wb_dbnetwork_* the hierarchical name overlay -- the three functions that
split a flattened path disagree about escapes. getBaseName
tracks backslash parity, stripParentPrefix checks only the
preceding character, and dbNetwork::name(Net) does a plain
find_last_of('/') and then an unanchored erase. Each case
targets one of those disagreements.
wb_writer_* write_verilog -- digit-leading and all-digit names, bus
bit vs escaped scalar lookalikes, _NC drift, an INT_MAX
wire index, port order.
Several of these fail in ways a construct-driven search would not have reached,
which is the argument for writing tests from the code as well as from the
language.
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
76 netlists from a survey of the hierarchy linking path, aimed at the three
families the corpus keeps finding defects in: identifier escaping, name
collisions and port wiring. 16 findings and 60 guards.
The guards matter as much as the findings. 34 port-wiring hazards are sound
today -- bus direction flips composing across three boundaries, a six-level
permutation chain with a different bijection at each level, offset and width-1
ranges, inout splits, twelve-port positional derangements -- and none had a
case. They go red if anyone breaks them.
The findings are five defects, each reached by a construct the corpus lacked:
- The flat bus regroup declares its base name over an existing escaped net
(5 cases). writeWireDcls folds bus bits into one declaration keyed on the
flattened base and skips a net only when findPort(cell, net_name) matches,
but it is handed the bus base `x/b`, not the port's sta name `x\/b`, so
that guard cannot fire. Two cases emit the SAME declaration twice at the
same width -- a reader that merges duplicates accepts it silently while
aliasing two electrically distinct buses.
- The flat hierarchy path join collides with an escaped user name (3), now at
depth 4 and with an implicit-net victim.
- Two synthesized flat names collide with each other (3), including a
three-way merge, so the victim count is not bounded at two.
- An _NC filler wire takes a name the netlist already uses (2). One reaches
_NC10, past the one-digit range. In the other the stolen name is a top
INPUT port and the open formal is an output bus, so the emitted
`wire _NC1;` merely redeclares a port -- legal Verilog, no diagnostic --
and a primary input ends up driven.
- A keyword-named bus is emitted without its escape (3). The known keyword
cases are all scalars, which take staToVerilog2 on the whole name; a bus
takes the parseBusName branch where only the base goes through
staToVerilog, whose escape test is !isAlnumUnderscore.
Two further defects are LEC-blind and recorded structurally: the _NC counter is
a writer member numbered file-globally while the declarations are counted per
module, so a module declares _NC1.._NC2 and references _NC3.._NC4; and a
width-mismatched port connection is not truncated or padded but dropped
entirely, leaving the port bound to invented dangling wires.
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
A per-PR audit of the merged hierarchy fixes in the four classes this corpus scopes -- name collision, modnet reassociation, feedthrough, escaped names -- asking for each whether the fix is even reachable through read_verilog -> link_design -> write_verilog, whether a netlist reproducer ever landed with it, and whether that netlist is in this corpus. The headline is the useful part: none of the ten PRs examined is reachable by this suite, because they fix code the round trip never calls. It is the record of why the corpus was written from the constructs and from the code rather than from the bug history, and it is the first place to look before adding a case for a past fix. Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
gadfort
force-pushed
the
hier-lec-conformance
branch
from
August 13, 2026 19:01
acf238e to
54398a2
Compare
maliberty
reviewed
Aug 14, 2026
maliberty
reviewed
Aug 14, 2026
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
Signed-off-by: Peter Gadfort <gadfort@zeroasic.com>
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
2 participants
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.
Summary
This was generated by asking Claude to build a LEC test loop and then try to find passing and failing netlists that OpenROAD fail to import correctly, by only reading, linking, and writing the netlist back out (this loop performs no work on the netlist and therefore should pass). My hope is that once the LEC tests are in, we can do the same for resizer and and other tools that modify the netlist and ensure we dont corrupt anything. This test suite is a superset of those in The-OpenROAD-Project/OpenSTA#399
Adds an equivalence-checking harness for the hierarchical netlist path and the
corpus it runs on. Every case asks one question:
Two suites answer it two ways.
dbsta_hier_conformanceproves the emittednetlist logically equivalent to the input with a SEC run, once per link mode.
dbsta_hier_structuraldiffs the emitted netlist against the input for the tenthings a LEC cannot see -- module set, top and submodule port order, declared
nets, instance bindings, cell census, assigns, name identity, namespace rules,
and whether the output can be read back at all.
Both compare against the input netlist, never
flat_outagainsthier_out. The flat dbNet view is built by mode-independent code, so a readerbug upstream of the hierarchy split corrupts both outputs identically and a
flat-vs-hier comparison passes while both are wrong. Running the modes
separately also gives attribution: a mismatch between them says the two
disagree, not which one is broken.
What is in the eleven commits
tst: add kepler-formal as a dev dependency and a LEC wrappertst: add LoadedDesign, the read/link/write fixturedbSta: add the hierarchy conformance and structural suitescrash/that kill the process and are a data dependency of neitherdbSta: carry over the PR mining auditThe corpus commits are split by provenance rather than by directory, because
that is what makes a group mean something: the original hier-vs-flat spike
(126), a generated depth x shape x wiring x naming sweep (272), a broad
construct search in three families (586), a whitebox survey written from the
code rather than the language (87), and a survey of the linking path aimed at
escaping, collisions and port wiring (76). Plus 41 symlinks to netlists other
tests already own, so a fixture written for rsz or odb is also held to
conformance.
kepler-formal
GPL-3.0 against OpenROAD's BSD-3-Clause, so it is invoked as a subprocess and
never linked --
//src/tst:lecbuilds the config, runs the binary andclassifies the verdict, linking nothing of it. In-tree precedent for shelling
out:
popeninsrc/rcx/src/parse.cpp,std::systeminsrc/web/src/web_serve.cpp.It builds from source as a bazel
dev_dependency, so nobody has to install itby hand and the tests cannot silently run against whatever binary is on
$PATH.Two accommodations make that work, both narrow:
//bazel:kepler.bzlcarries a Starlark transition that strips-xc++fromcxxopts for kepler's subgraph only. OpenROAD sets that flag globally (a NixOS
accommodation), and
rules_foreign_ccbakes cxxopts intoCMAKE_CXX_FLAGS,which CMake reuses at link time -- so clang tries to parse
.ofiles as C++source when building kepler's oneTBB dependency.
bazel/kepler-patches/drops a linkopt that naja's python-embed leaks, whichwould otherwise export a system library search directory into the link.
etc/DependencyInstaller.shgains the host tools kepler's own build reachesoutside bazel for (bison, flex, m4, cmake, pkg-config, python3 headers).
Without them the failure surfaces as an unhelpful repository-rule error inside
a bazel fetch.
.bazelrcis untouched. The binary comes from runfiles; someone who wantstheir own build passes
--test_env=KEPLER_FORMAL=/path/to/kepler-formalthemselves, which is deliberate -- forwarding it repo-wide would let a stray
value in a developer's shell silently replace the pinned binary.
Known failures are XFAIL, not DISABLED_
A disabled test never runs, so the day the bug is fixed nothing says so and the
case sits switched off. Every known failure is instead an inverted expectation:
if a case starts passing, the suite goes red with a message naming the entry
to delete, so coverage of a bug is never silently lost and a fix is never
silently unnoticed.
The list is
src/dbSta/test/hier_expected_fail.bzl, grouped by failure mode --325 conformance rows in 119 groups, 1148 structural rows in 51 -- and BUILD
renders it into the manifest each suite reads. Keeping it in Starlark rather
than a text file means Starlark rejects a malformed entry when the package
loads: an unknown check or link mode, a
:that would truncate the row, or onenetlist listed twice under a single key. The text format lost all three
silently.
Issue numbers are
TBDpending a single umbrella issue; the aim is to moveevery one of these entries to passing.
Two defects this turned up in its own scaffolding
Both were latent and would have shipped:
used to exit 0 whether it proved equivalence or found a difference, and now
exits 3 on a difference -- so every genuine inequivalence was being reported
as a tool error. That is the worst direction to be wrong in: it makes a real
defect indistinguishable from a broken fixture. The verdict text is now read
first, and the exit status only decides what an absent verdict means.
inherited/in its data. Those 41netlists -- the ones other tests own, which is exactly why they matter -- had
never run under it. Adding the dependency turned up 22 rows of real failures.
The suite had a guard against
structural/silently emptying but none forinherited/; it now has both.Running it
Both suites are should stay inside the default test timeout. The
conformance suite is the expensive one -- roughly 2400 SEC runs -- and it is
the reason kepler is a dev dependency rather than a required one.
Reviewing
Each commit builds and its tests pass on their own, so the history bisects. The
two places worth the most attention are
src/tst/src/lec.cpp, where readingkepler's output wrong is silent rather than loud (three separate ways, all
commented at the point of the decision), and
src/dbSta/test/cpp/TestHierStructural.cpp, where each of the ten checksdefines what "the same netlist" means.
The corpus itself is mechanical: one hazard per netlist, a
// TARGETS:headerdeclaring what it exercises, and a lint that rejects two cases with identical
targets and identical bodies.
What this does not cover
Only
read_verilog -> link_design -> write_verilog. Port punching, bufferinsertion,
write_db/read_db, DEF, SDC and the name-lookup commands are allout of scope here and have known gaps --
odb::replaceBracketsWithUnderscores,for one, cannot be reached from this loop at all. Those need a driver that runs
a transform between link and write, which is deliberately left for later.
Type of Change
Impact
This only adds testing and does not attempt to determine the root cause.
Verification
./etc/Build.sh).