Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs


To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


This paper deals with verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. As models of those descriptions, we use state machines extended by quantifier-free first-order logic with equality. Since the signals in the corresponding outputs of such descriptions rarely change simultaneously, we cannot adopt the classical notion of equivalence for state machines. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algorithm for checking consistency of those descriptions, up to a limited number of steps from initial states. A simple hardware/software codesign is taken as an example of high-level designs. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite number of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems