State Reachability Benchmarks
Notes to the following benchmarks:
- All the following properties are state reachability properties
- BMC is able to solve all, but may require significant effort
- Simulation-based methods, using ACO, was able to reach many of these in shorter computational costs (but vector lengths may be higher)
- Detailed results can be referred to in the following papers:
-
"Utilizing GPGPUs for design validation with a modified ant colony optimization,"
Min Li, Kelson Gent and
Michael S. Hsiao,
in Proceedings of the IEEE High Level Design Validation and Test Workshop, November 2011.
-
"An ant colony optimization technique for abstraction-guided state justification,"
Min Li and
Michael S. Hsiao,
in Proceedings of the IEEE International Test Conference,
November 2009.