Abstract Download gzipped postscript Bibtex entry |
We describe the use of parametric representations of Boolean
predicates to encode data-space constraints and significantly extend
the capacity of formal verification.
The constraints are used to decompose verifications by sets of case
splits and to restrict verifications by validity conditions. Our
technique is applicable to any symbolic simulator. We illustrate our
technique on state-of-the-art Intel designs, without removing
latches or modifying the circuits in any way.
Bibtex Entry
@INPROCEEDINGS{aagaard-dac-99,
AUTHOR = {Aagaard , Mark D. and Jones , Robert B. and Seger , Carl-Johan H. },
TITLE = {Formal Verification Using Parametric Representations of {B}oolean Constraints },
BOOKTITLE = {dac},
YEAR = {1999},
MONTH = {jul},
}
Send questions or comments to
Mark Aagaard
< aagaard@swen.uwaterloo.ca
>