Formal verification using parametric representations of Boolean constraints
The work
| Authors | Mark D. Aagaard; Robert B. Jones; Carl-Johan H. Serger |
|---|---|
| Editors | |
| Type | misc |
| Year | 1999 |
| Citekey | aagaard1999formal |
Where it appeared
| Published in | Proceedings - ACM IEEE Design Automation Conference |
|---|---|
| Publisher | Association for Computing Machinery |
| Pages | 402--407 |
Identifiers
| DOI | 10.1145/309847.309968 |
|---|---|
| OpenAlex | W1972934510 |
Access
| Landing page | https://doi.org/10.1145/309847.309968 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/309847.309968 |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
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 (R) designs, without removing latches or modifying the circuits in any way.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 02:23 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@misc{aagaard1999formal,
title = {Formal verification using parametric representations of Boolean constraints},
author = {Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Serger},
year = {1999},
journal = {Proceedings - ACM IEEE Design Automation Conference},
publisher = {Association for Computing Machinery},
pages = {402--407},
doi = {10.1145/309847.309968},
}
This record lives at https://refs.drheap.org/aagaard1999formal/ and will keep doing so.