Design Automation Conference (1988)
Anaheim, CA, USA
June 12, 1988 to June 15, 1988
Madre , Bull Res. Center, Louveciennes, France
Billon , Bull Res. Center, Louveciennes, France
A novel method is presented for verifying functionality in the design of VLSI circuits. The method fits naturally in a methodology based on a hardware description language (HDL). Two programs describe the system under design: (1) its specification and (2) the extracted behavior from its layout. Verifying the design comes down to proving that these programs are correct and equivalent with regard to the HDL semantics. The authors define a process named formal analysis that permits to prove these properties without setting values to the programs inputs. Formal analysis is based on a canonical form of Boolean logic that is named typed Shannon's canonical form. They implemented this method in PRIAM, an efficient circuit prover now used by industrial CPU designers.
VLSI circuit design, circuit correctness, functionality, hardware description language, HDL, specification, formal analysis, canonical form, Boolean logic, typed Shannon's canonical form, PRIAM, circuit prover
Madre and Billon, "Proving circuit correctness using formal comparison between expected and extracted behaviour," Design Automation Conference(DAC), Anaheim, CA, USA, 1988, pp. 205-210.