Add a "mode" option to cfg file #28
Merged
Conversation
Add a "mode" option on .cfg file to define whether you are going for a bmc or an induction proof
|
The formal test-bench used by riscv-formal ( Thus for a complete proof |
|
see #28 (comment) |
checks/genchecks.py
Outdated
| @@ -433,6 +446,7 @@ def check_cons(check, chanidx=None, start=None, trig=None, depth=None, csr_mode= | |||
| check_cons("unique", chanidx=i, start=0, trig=1, depth=2) | |||
| check_cons("causal", chanidx=i, start=0, depth=1) | |||
| check_cons("ill", chanidx=i, depth=0) | |||
| check_cons("const_2_time", chanidx=i, start=0, trig=1, depth=2) | |||
cliffordwolf
Aug 8, 2019
Collaborator
What is const_2_time?
What is const_2_time?
AlAlves
Aug 8, 2019
Author
Contributor
Oops, my bad, I mixed this version with my custom version.
I fixed it.
Oops, my bad, I mixed this version with my custom version.
I fixed it.
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.
Add a "mode" option on .cfg file to define whether you are going for a bmc or an induction proof