IEICE TRANSACTIONS on Information
Verifying Signal-Transition Consistency of High-Level Designs Based on Symbolic Simulation
Summary :
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
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
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.
Cite this
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 -
English
