Conversation
Use exact PDR obligations for concrete and strict rail equality, report outputs affected by uninitialized sequential logic, and add regression coverage.
bump naja
python publishing flow
Removed KF's SEC equivalence problem export instructions and added section for custom Python primitives.
Expose selected instance inputs as compared outputs and outputs as shared inputs in CLI, YAML, and Python LEC/SEC flows, including compact extraction. Add interface/connectivity validation and regression coverage while keeping normal equivalence statuses. Known limitation: a nested cut that empties its parent wrapper can cause SEC to treat that wrapper as opaque; this remains unresolved.
Add tests for invalid paths, pins, signatures, ownership transfer, CLI configuration validation, aliases, and compact-mode error recovery. Preserve all existing test and production lines.
Enable relation learning and internal X equality by default through CLI, YAML, and Python options. Prove candidates from initialization and joint induction before publishing state equalities. Preserve the existing output property and bypass learning entirely when disabled. Add dedicated soundness and option coverage. Keep existing test assertions unchanged, disabling learning only in tests of the previous no-mining path.
Constrain exact interpolation, reachable-state enumeration, and invariant validation with relations accepted by the existing learning switches. Preserve the original queries when learning is disabled and keep the output property unchanged. Document the switch gating beside the stored invariant and add six regression tests without changing existing assertions. Validation: 421 SEC tests, 363 CLI/boundary tests, and Python/native suites passed.
Exclude ki-dual-rail / cts_aes_asap7_base and pdr-dual-rail / nangate45_swerv until their excessive runtime is resolved. Preserve all 148 other combinations.
…ions The internal relation learner applied its hypotheses as SAT assumptions, which prevents the solver from using the hypothesised register equalities during preprocessing: with the two designs' transition logic written over different input literals, congruence closure cannot merge structurally identical gates, and a trivially inductive query becomes a search problem that exhausts the learner's work budget. On the issue #250 designs every candidate relation therefore went uncertified (64 candidates, 0 proved on acc8; 85 candidates, 0 proved on tinyalu) and the learner had no effect on the proof. Apply the equality hypotheses by aliasing each candidate's right-hand register to its left-hand literal in the current frame, and add the remaining (definedness) hypotheses as unit clauses. Refinement re-encodes in a fresh solver instead of retracting assumptions. The certified set is unchanged in meaning; only the encoding of the same induction query differs. Dual-rail PDR self-compare, previously partial, now proves every output: acc8 7/8 -> 8/8 (~25 s -> <1 s); tinyalu 8/17 -> 17/17 (~121 s -> <1 s); accumulator banks of every size in the issue's table prove in <1 s. Add CLI regression tests for both issue #250 designs, gated on full coverage as the report recommends. Fixes #250. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017goaCDRnHusDV3VvPSQ4fV
The summary ran as a workflow_run follow-up, which GitHub always executes on the default branch. It did fire for pull requests, but each table landed in a detached run labelled main that the pull request never links to, so in practice only main had a usable summary. Make the summary the last job of regress-sec instead. It now belongs to the run it reports on, so every pull request shows it in its checks, on its own run summary page, and as an artifact of its own run. Remove the workflow_run workflow, which would otherwise produce a duplicate. Also save the rows as JSON next to the table and compare each run with the newest main run that has them: a "Changes vs main" section lists only the rows whose SEC result, output coverage, or CI status differ, and every row gains the main runtime and relative change. SEC-step fallback timings are shown but not compared, and a missing or malformed baseline is reported and ignored rather than trusted. Without a baseline the table is unchanged.
…earning The learner's size gate summed each register's cone separately, so shared logic was counted once per register and real designs never reached the solver. - Split the candidates into partitions instead of giving up (Mishchenko et al., ICCAD 2008, section 3.3). - Replay each counterexample on the original transitions next to random states, so one counterexample refines all candidates (Mony et al., DAC 2005, section 3.2). - When a partition is undecided, ask each pair separately and drop only the undecided ones instead of discarding everything (Mony et al., sections 2 and 4.1). tinyrocket self-SEC (PDR, dual-rail) goes from 8/132 outputs to 132/132, so the CLI test now expects a full proof. docs/sec-internal-relations.md describes the flow and its limits.
Every partition created a solver variable for every symbol in both frames, used or not. On nangate45_black_parrot_sec_final that is 5.3M variables and about 2 GiB per partition, and the learner peaked at 16.3 GiB. The partition encoders now create a variable when the encoded logic first mentions a symbol, and apply the hypothesis merge through the encoder's symbol map. Dual-rail validity clauses are added only for the rails a partition uses. The clauses for the pairs being proved are unchanged. black_parrot round 0: about 5.8 GiB to 2.5 GiB per partition, peak 16.3 GiB to 13.2 GiB, 347 s to 284 s. The peak is still dominated by transition logic that stays cached, so this design can still exceed a 13 GiB runner.
The partitioned learner runs on any design, and on nangate45_black_parrot_sec_final (666,543 candidate pairs) it needs over 13 GiB and tens of minutes, so its CI rows ran out of memory or crawled. The logic behind the candidates is now counted once per shared node, and above about 8 million nodes the learner is skipped, which leaves the output proof as it is without learning. Counting stops at the limit, so a large design is not built in memory just to be measured. The previous gate summed every register's cone separately and therefore skipped every real design. Locally, k-induction dual-rail on black_parrot: over 1,500 s and 13.2 GiB before, 304 s and 6.4 GiB now (208 s and 6.3 GiB with learning disabled). tinyrocket (0.9 million nodes) still learns and proves 132/132 outputs.
The summary job listed the jobs of every attempt of its run. After a few re-runs that listing spans several pages, and GitHub's API answers some of those pages with a persistent 502, so every re-run of the summary failed (main run #335, four attempts). Listing the current attempt returns every job of the run in a listing that paginates cleanly. Jobs carried over from earlier attempts keep their own run_attempt, which summarize_sec_regress.py already uses to pick the latest attempt of each job and its result artifact.
Listing only the current attempt would look up every job under that attempt number, but after a re-run of failed jobs the unchanged jobs ran, and stored their results, under an earlier attempt. The step now lists attempts 1 through the current one. A job appears from the attempt it ran in onward, so its first appearance gives that attempt, and the summary keeps each job's latest attempt and reads the matching result artifact. Jobs re-run in different attempts are therefore each taken from their own last run.
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
3 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.
No description provided.