[CI] Invariant Verification Test Cases#699
Conversation
Jiahui17
left a comment
Jiahui17
left a comment
There was a problem hiding this comment.
If we add a new CLI command, make sure to document it in docs/
There was a problem hiding this comment.
- Wrap this test in
#ifdef DYNAMATIC_ENABLE_LEQ... - Add
--enable-leq-binariesindynamatic/.github/workflows/ci.yml
Line 83 in 8074f73
- Change this to invariant fixture
There was a problem hiding this comment.
You mentioned that we can add more test cases for the verify-invariants fixture as it should be fast. The current test cases are taking around 5 seconds each (on the eda machine). Is this a reasonable time for a larger set of tests?
Jiahui17
changed the title
| parser.add_argument("json_file", help="Path to the JSON file to update.") | ||
| parser.add_argument( | ||
| "nuxmv_file", help="Path to the file generated by nuXmv.") | ||
| parser.add_argument("-d", "--detect-unproven", dest="detect_unproven", |
There was a problem hiding this comment.
--abort-on-unknown is more precise?
| clEnumValN(HDL::SMV, "smv", "SMV")), | ||
| cl::cat(mainCategory)); | ||
|
|
||
| static cl::opt<bool> verifyInvariants( |
There was a problem hiding this comment.
This flag does not specify that the invariants need to be annotated (they are always annotated if they are in the JSON), but rather tells the exporter to generate them in a different way (in order to check the correctness of the invariants):
Usually they are generated as
INVAR !(fork0.outs0 & fork0.outs1)
but in the case the verify-invariants flag is set, they are generated as
INVARSPEC NAME p10 := !(fork0.outs0 & fork0.outs1)
There was a problem hiding this comment.
should the script be a separate file to not grow this one too much?
There was a problem hiding this comment.
In an earlier version I had two different files, but then we decided that, due to a lot of code duplication, it would be better to merge them into a single file.
2 participants
Adding tests to verify the automatically annotated invariants in rigidification to