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.
