The search functionality is under construction.

The search functionality is under construction.

This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. 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. As an example of high-level designs, we take a simple hardware/software codesign. 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.

- Publication
- IEICE TRANSACTIONS on Information Vol.E85-D No.10 pp.1587-1594

- Publication Date
- 2002/10/01

- Publicized

- Online ISSN

- DOI

- Type of Manuscript
- Special Section PAPER (Special Issue on Test and Verification of VLSI)

- Category
- Verification

The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.

Copy

Kiyoharu HAMAGUCHI, Hidekazu URUSHIHARA, Toshinobu KASHIWABARA, "Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation" in IEICE TRANSACTIONS on Information,
vol. E85-D, no. 10, pp. 1587-1594, October 2002, doi: .

Abstract: This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. 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. As an example of high-level designs, we take a simple hardware/software codesign. 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.

URL: https://global.ieice.org/en_transactions/information/10.1587/e85-d_10_1587/_p

Copy

@ARTICLE{e85-d_10_1587,

author={Kiyoharu HAMAGUCHI, Hidekazu URUSHIHARA, Toshinobu KASHIWABARA, },

journal={IEICE TRANSACTIONS on Information},

title={Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation},

year={2002},

volume={E85-D},

number={10},

pages={1587-1594},

abstract={This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. 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. As an example of high-level designs, we take a simple hardware/software codesign. 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.},

keywords={},

doi={},

ISSN={},

month={October},}

Copy

TY - JOUR

TI - Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation

T2 - IEICE TRANSACTIONS on Information

SP - 1587

EP - 1594

AU - Kiyoharu HAMAGUCHI

AU - Hidekazu URUSHIHARA

AU - Toshinobu KASHIWABARA

PY - 2002

DO -

JO - IEICE TRANSACTIONS on Information

SN -

VL - E85-D

IS - 10

JA - IEICE TRANSACTIONS on Information

Y1 - October 2002

AB - This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. 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. As an example of high-level designs, we take a simple hardware/software codesign. 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.

ER -