Efficient Verification of VLSI Circuits Based on Syntax and Denotational Semantics
The work
| Authors | Filip Van Aelten |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1989 |
| Citekey | vanaelten1989efficient |
Where it appeared
| Publisher | MIT Research Laboratory of Electronics |
|---|---|
| Number in series | RLE Technical Report No. 546 |
| School | MIT Research Laboratory of Electronics |
Related
| Distinct from | vanaelten1989efficientimec |
|---|
From bibtex.
Abstract
A fully automatic circuit verification system takes in a circuit description and a specification of its behavior, and checks whether the circuit behaves as specified. Existing verification systems follow one of two approaches: a deductive approach, based on a formal logic, or a rewrite rule approach, which starts from knowledge about how transistors work, and goes straight but slowly from premises to conclusions. I present a new, more efficient approach, which incorporates large scale knowledge about VLSI circuits in a coherent fashion. The approach is based on the denotational method for defining the semantics of a programming language. A circuit is parsed according to a circuit grammar, and the resulting parse tree is mapped into a behavioral description which is matched with the user supplied specification. The new strategy is implemented in the program Semanticist.
A copy is held
pdf, 6.7 MB. 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-10-05 22:03 UTC |
| Approved by | a person 2026-10-22 23:06 UTC |
Cite it as
@techreport{vanaelten1989efficient,
title = {Efficient Verification of VLSI Circuits Based on Syntax and Denotational Semantics},
author = {Filip Van Aelten},
year = {1989},
publisher = {MIT Research Laboratory of Electronics},
school = {MIT Research Laboratory of Electronics},
}
This record lives at https://refs.drheap.org/vanaelten1989efficient/ and will keep doing so.