Repository navigation
Conversation
A combinational LEC that finds a difference exited 0, the same as one that proves the designs equivalent; SEC already reports its verdict in the exit status (0 proved, 3 counterexample). A script or build rule that runs kepler-formal could not tell a broken design from a good one without parsing the log, and one that trusted the exit status passed a deliberately broken netlist. A difference now exits kLecDifferenceExitCode, defined as SEC's counterexample code, from all three LEC paths (whole design, scopes, compact snapshots); equivalent stays 0. This changes a contract the tests pinned in seven places (the structured in-process run, MiterTests' differing pairs, the tinyrocket examples, the Python primitives test); they now expect 3, and LecResultExitCodesAreStable fixes the value. The README gains an LEC result-code table beside the SEC one. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
KeplerFormalCliTests.cpp is built by CMake only, so the tests the first commit changed there do not run under bazel test. MiterTests does: LecExitStatusTellsADifferenceFromEquivalence runs the binary on an equivalent pair (exit 0) and a differing one (exit 3). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This branch has not been deployed
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
1 participant
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.
A combinational LEC that finds a difference exits 0, the same as one that proves the designs equivalent. SEC already reports its verdict in the exit status (0 proved, 3 counterexample). A build rule that runs kepler-formal has to parse the log to tell a broken design from a good one. In bazel-orfs, a rule that trusted the exit status passed a deliberately broken netlist.
This changes a contract the tests pin, so it's up for discussion. Seven places expected exit 0 for a differing pair: the structured in-process run,
MiterTests' differing pairs, the tinyrocket examples (tinyrocketagainsttinyrocket_edited), and the Python primitives test. If exit 0 on a difference is intended, this PR is the place to say so and I'll close it.kLecDifferenceExitCode, defined askSecCounterexampleExitCode(3). This holds on all three LEC paths: whole design, scopes and compact snapshots. Equivalent stays 0.LecResultExitCodesAreStablepins the value.Tested:
bazel test //....MiterTestsandBazelPythonPrimitivesTestpass with the updated expectations, and so doesMiterTests' newKeplerCliSubprocessTests.LecExitStatusTellsADifferenceFromEquivalence, which runs the binary on an equivalent and a differing pair.Correction: an earlier version of this description implied that the
KeplerFormalCliTests.cppchanges ran underbazel test. That file is built by CMake only, so those edits keep the CMake suite consistent but were not run. The Bazel-run test above is the one that covers this change.🤖 Generated with Claude Code