General Safety Properties
Notes to the following benchmarks:
- All the properties in this suite are AG type.
- We use the symbol "V" to represent disjunction of elements in the property.
- A flip-flop id, say G20, in the .bench file is prefixed with an "FF" in the property and written as FF20.
- Currently, we have used random logic simulation to obtain one initial state for the design, which
is used in the base case run. More than one initial state can also be employed by the user.
- The circuits starting with "b" have a reset signal among one of its inputs.
- Some of the original ISCAS circuits are not initializable. All the circuits given in this suite
are modified to be "sequence initializable".
- Most of the benchmarks could not be solved with BMC+induction, but require property-strengthening to solve.
- Detailed results on these benchmarks can be found in the following papers:
-
"Explicit safety property strengthening in SAT-based induction,"
(pdf)
Vishnu Vimjam and
Michael S. Hsiao,
in Proceedings of the IEEE International Conf. VLSI Design,
January 2007, pp. 63-68.
-
"Fast illegal state identification for improving SAT-based induction,"
(pdf)
Vishnu Vimjam and
Michael S. Hsiao,
in Proceedings of the IEEE Design Automation Conf., July 2006, pp. 241-246.