Formal Verification of Digital Circuits Using Symbolic Ternary System Models
The work
| Authors | Randal E. Bryant; Carl-Johan Seger |
|---|---|
| Editors | E. M. Clarke; R. P. Kurshan |
| Type | incollection |
| Year | 1991 |
| Also known as | bryant1991formalb |
| Citekey | bryant1990ternary |
Where it appeared
| Published in | Computer-Aided Verification '90 |
|---|---|
| Publisher | American Mathematical Society |
| Pages | 121--146 |
Identifiers
| DOI | 10.1007/bfb0023717 |
|---|
Access
| Landing page | https://www.cs.cmu.edu/~bryant/pubdir/cav90.pdf |
|---|
Related
| Distinct from | bryant1991memory |
|---|---|
| Distinct from | chakraborty2015wordlevel |
| Distinct from | claessen2009faithful |
| Distinct from | khasidashvili2009assumeguarantee |
| Distinct from | seger1995formal |
From bibtex.
Abstract
Ternary system modeling involves extending the traditional set of binary values {0,1} with a third value X indicating an unknown or indeterminate condition. By making this extension, we can model a wider range of circuit phenomena. We can also efficiently verify sequential circuits in which the effect of a given operation depends on only a subset of the total system state. This paper presents a formal methodology for verifying synchronous digital circuits using a ternary system model. The desired behavior of the circuit is expressed as assertions in a notation using a combination of Boolean expressions and temporal logic operators. An assertion is verified by translating it into a sequence of patterns and checks for a ternary symbolic simulator. This methodology has been used to verify a number of full scale circuit designs.
A copy is held
pdf, 171.6 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 21:23 UTC |
| Approved by | a person 2026-09-23 14:09 UTC |
Filed under
Cite it as
@incollection{bryant1990ternary,
title = {Formal Verification of Digital Circuits Using Symbolic Ternary System Models},
author = {Randal E. Bryant and Carl-Johan Seger},
editor = {E. M. Clarke and R. P. Kurshan},
year = {1991},
booktitle = {Computer-Aided Verification '90},
publisher = {American Mathematical Society},
pages = {121--146},
doi = {10.1007/bfb0023717},
}
This record lives at https://refs.drheap.org/bryant1990ternary/ and will keep
doing so. It used to be called bryant1991formalb, and those addresses still resolve to this one.