design_db: a verification-gated library of subcircuit implementations#5
Open
plex1 wants to merge 16 commits into
Open
design_db: a verification-gated library of subcircuit implementations#5plex1 wants to merge 16 commits into
plex1 wants to merge 16 commits into
Conversation
…ons (S1 core) New subpackage spire.design_db: for each subcircuit (a slot, keyed by its golden spec) the DB holds correct implementations with metric vectors and provenance. Producers insert through a verification gate; consumers select deterministically (selection decorator + CLI follow). - keys.py: spec_key = sha256(structural AAG + port spec). Keying on to_verilog() text is context-dependent for pre-built instances (signal names are assigned at construction, outside any _push/_pop_shared_state bracket); the numeric AigerExporter section is bit-exact across build contexts. Components are lowered with a fixed top name (to_netlist's default is random). - verify.py: verification seam. Circuit-class detection (reg-kind scan) as a guardrail, the frozen verification.json format, and Tier-0 CEC (yosys -> flattened BLIF x2 -> yosys-abc cec, mirroring rtlscout core/equivalence.py) under a bounded budget. Fail-and-choose: a timeout raises CECTimeout with the options message (--budget | --auto | --stimulus); no auto-fallback. - store.py: v1 layout, atomic writes (tmp+rename), zero-config DB-root resolution (SPIREHDL_DB_PATH -> nearest design_db/ upward -> auto-create ./design_db), manifest with registered_from back-refs, register_slot (idempotent; sequential slots register but stay unverified until a sim tier is frozen). - insert.py: the gate. Accepts a spire Component/Netlist (lowered internally), a Verilog file path, or raw Verilog text. Runs the slot's frozen verification, dedups by AAG structural hash, stamps intrinsic metrics (AIG nodes/depth/latches) plus a heavy-pipeline yosys transistor count (extract_yosys_heavy_metrics_from_verilog), records provenance, admits atomically. - Import stays light: pyosys/aigverse are deferred into the function bodies that need them. - testing/design_db/test_s1_core.py: 11 tests against real yosys + yosys-abc (register, insert + metrics, spire-object insert, atomic reject, dedup, sequential refusal, timeout options, idempotent back-refs, unknown slot, zero-config auto-create, env override). Full suite: 477 passed, 19 skipped, 12 xfailed, 12 xpassed. - docs/README_design_db.md: user-facing docs of the S1 surface (to be extended with the selection decorator, CLI, and sim tiers).
…(S2)
Consumers arrive: deterministic selection over admitted designs, the pure selection decorator,
and the human/agent CLI. The decorator never generates and never spends budget.
- select.py: objectives area|delay|adp|edap as argmin, plus constrained(minimize=, subject_to=),
weighted(weights), lexicographic(objectives) combinators; pin= (exact design_id; missing pin =
broken reproducibility lock, raises); pareto_front(). metric= picks the measurement system
("aig" intrinsic | "transistors" heavy-pipeline | a technology once PPA-scored); metric=None
resolves deterministically technology -> transistors -> aig. Resolved
(selected_id, objective, metric) recorded in the manifest (record=True).
- decorator.py: @from_design_db(objective=, metric=, pin=, fill=, db=) - trace (same arg
classification as @abc_optimized) -> register slot -> select -> splice via the stored
design.aag + _instantiate_from_cache. Miss => the original logic (one-line note; builds never
fail); fill= fires once on miss, then re-select. Registration captures the function's current
source as the slot starting point: starting_point.py (runnable wrapper when self-contained,
tagged fidelity: self-contained|fragment) + source_ref={file,qualname,line} in spec.json.
- cli.py + __main__.py + [project.scripts] spire: `spire db init | ls | show <name|key|prefix>
[--pareto] | insert <v> --slot ...`. show/ls are read-only and never create a DB (regression
test); insert exits 2 with REJECTED(...) on verification failure and keeps stdout JSON-clean
(tool noise redirected).
- insert.py: gate hardening - candidate ports must match the slot spec (clear "port mismatch"
error instead of an abc mystery); design.aag stored per design (precomputed splice input, so
elaboration-time splicing needs no yosys).
- store.py: update_manifest_selection().
- docs/README_design_db.md: extended for the S2 surface (decorator quick start, selection,
CLI, layout incl. design.aag/starting_point.py/source_ref).
- testing/design_db: 25 tests green (S1 11 + S2 14) against real yosys/yosys-abc; full spire
suite unaffected.
…rmanent slot names, and split `verify` and `set-verification` (configure) / `verify` (advisory) / `insert`
…ce of truth; index.json = self-healing cache; fcntl-locked manifest) â�� concurrent inserts can never lose designs
…r recorded); readers never create; identifier docs clarified
…mporary selection overrides
select_design -> pick_design and the manifest selection record is REMOVED: it could only ever
say what the LAST compile chose (not the best eval; last-writer-wins on shared DBs), and it made
a read look stateful. Picking is now a pure query (record= gone, update_manifest_selection
deleted; the manifest is name bindings only; `spire db ls` drops its selected column). The audit
trail moves to the artifact: $SPIREHDL_DB_SELECTION_LOG makes the decorator append one JSON line
{spec_key, name, design_id, objective, metric} per splice to a caller-owned file — selections
are a property of the compiled artifact, not the library.
Temporary selection overrides force picks without touching source (what-if compiles,
composition sweeps): $SPIREHDL_DB_PINS (JSON {slot: design_id}, crosses process boundaries) or
selection_overrides({...}) (scoped context manager, nestable). Keys are spec_keys or manifest
names; values follow pin= rules (unknown => error); an explicit source-level pin= always wins.
Readers never create: pick_design/pareto_front open the store without auto-creation and
read_index never materializes a slot on a read — a query cannot create a DB.
Docs: identifier clarifications (slot identity = spec_key, names are permanent aliases,
design_id format <source>:<hash10>, design_ref prefix resolution, pin exactness rationale),
selection-overrides + selection-log sections, loop-over-a-slot snippet. Tests: overrides (both
doors, nesting, name keys, precedence, errors, AAG-level decorator-splice proof, cross-process
env), pure-query guarantees, selection log, readers-never-create. design_db 62 passed; full
spire suite 539 passed / 19 skipped.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YD3ZSuktGBUWBgzUv8VEUn
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.
What this adds
spire.design_db— a content-addressed store of correct implementations of a subcircuit.Each slot is keyed by its golden specification; implementations enter only through a
verification gate and are selected deterministically at build time. Generation and selection
are fully decoupled: filling a slot once lets every later build pick from it. Generation itself
lives outside spire (RTLScout calls in through the public
insert/annotateAPI; spire neverimports rtlscout).
New folder
src/spire/design_db/plus aspireconsole script ([project.scripts]) — purelyadditive, no existing spire module is touched (19 files, +3485 lines, 0 deletions).
The pieces
design_db/v1/<spec_key>/(spec, golden, verification,starting point, admitted designs). Zero-config root resolution: explicit
--db→$SPIREHDL_DB_PATH→ nearestdesign_db/upward from cwd → auto-create.metric-stamp (
aig+transistors) → atomic admit (dir rename). A failing candidateleaves no trace; a structural duplicate returns
deduped=True. Spire designs are first-classinserts: the
.pysource is stored alongside, Verilog stays the interchange form.harness (corners + seeded random, golden-simulated outputs, frozen
tb.sv+ vectors).Tier 2: authored stimulus (a Python
generate(ports, n_vectors, seed)generator; outputsalways golden-simulated).
set-verification(configure + one-shot freeze) is split fromverify(advisory check) andinsert(the gate); frozen verifications are immutable.objective = area|delay|adp|edapor combinators (constrained,weighted,lexicographic),pareto_front, andpin=as a reproducibility lock. Metric systems areself-describing (each design's
metrics.jsonmaps objective axes per measurement system);annotateattaches externally measured systems — e.g. real asap7 PPA — enablingmetric="asap7"selection. The resolved(selected_id, objective, metric)is recorded in themanifest for auditability.
@from_design_dbdecorator — trace → auto-register the slot (golden + spec + defaultverification + captured starting point) → select → splice. Miss ⇒ the original logic
(AAG-identical to the undecorated function, test-asserted), never an error, never spends
budget. Opt-in
fill=hook: called once on a miss asfill(spec_key, db_root=…, objective=…, metric=…), with a re-select in the same compile.Slot names are permanent (function qualname by default; renames raise).
(
index.jsonis only a self-healing cache) and manifest writes are fcntl-locked, soconcurrent inserts — same slot or different slots, threads or processes — can never lose
designs. Parallel fills of one DB are supported.
spire db init|ls|show|insert|seed|verify|set-verification|annotate(alsopython -m spire.design_db).Trust model, in one line
Producers propose; the gate disposes — nothing enters without passing the slot's frozen
verification, metrics are tooling-stamped, and technology PPA enters only through
annotate.Testing
51 tests in
testing/design_db/, all passing; full spire suite green:starting-point capture
annotate/ self-describing metric systems (incl. sibling-consistency guard)three concurrent subprocess inserts into one slot all landing
Downstream, RTLScout's full suite runs against this branch as a submodule (99 passed), including
a composed test where a decorator miss fires a real RTLScout campaign and the same compile
splices the result.
Docs
docs/README_design_db.md— concepts, decorator + filling quick starts, thefill=contract,selection & metric systems, verification tiers, CLI table, layout on disk.