diff options
| author | Emil J <emil.tywoniak@gmail.com> | 2022-10-19 12:20:12 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-19 12:20:12 +0200 |
| commit | 8859d801c83b6d67279bb907837bb7b08d2f338e (patch) | |
| tree | 06602fe3b308c3b36a9d19efdd08399f477ebab1 /misc | |
| parent | f4ede15d6857c02576a32f94043af866fde607aa (diff) | |
| download | yosys-8859d801c83b6d67279bb907837bb7b08d2f338e.tar.gz yosys-8859d801c83b6d67279bb907837bb7b08d2f338e.tar.bz2 yosys-8859d801c83b6d67279bb907837bb7b08d2f338e.zip | |
Temporal induction counterexample loop detection (#3504)
I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
Diffstat (limited to 'misc')
0 files changed, 0 insertions, 0 deletions