Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs
In this work we compared different IC3-based model checking techniques for verifying Verilog RTL designs.
We analyzed a total of 535 safety checking problems (Verilog RTL with SVA), and evaluated 6 different techniques: 4 of them operating at the bit level, and 2 at the word level.
The study helped us identify several advantages of word-level model checking over bit-level techniques, and opportunities for improving scalability in model checking.
- Complete details can be found in our DATE 2019 paper [Link]
- Experiment data and numerous plots can be found in the Github repository [Link]
- I presented a poster on this work at the DATE 2019 conference in Florence, Italy [Link]
- I will be presenting a paper on the techniques underlying AVR at the NASA Formal Methods Symposium 2019 in Houston, TX [preprint]
