The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
Cet article traite de la vérification formelle des conceptions de haut niveau, en particulier de la comparaison symbolique des descriptions au niveau du transfert de registre et des descriptions comportementales. Nous utilisons des machines à états étendues par une logique du premier ordre sans quantificateur avec égalité, comme modèles de ces descriptions. Nous ne pouvons pas adopter la notion classique d’équivalence pour les machines à états, car les signaux dans les sorties correspondantes de ces deux descriptions ne changent pas de la même manière. Cet article définit une nouvelle notion de cohérence basée sur les transitions de signaux des sorties correspondantes, et propose un algorithme pour vérifier la cohérence de ces descriptions, jusqu'à un nombre limité d'étapes à partir des états initiaux. Comme exemple de conceptions de haut niveau, nous prenons une simple conception matérielle/logicielle. Le programme AC pour le traitement du signal numérique appelé filtre PARCOR a été comparé à sa conception correspondante donnée sous forme de description au niveau du transfert de registre, qui est composée d'une architecture VLIW et d'un code d'assemblage. Puisque cet exemple se termine sur environ 4500 31 étapes, l’exploration symbolique d’un nombre fini d’étapes est suffisante pour vérifier les descriptions. Notre vérificateur de prototype a réussi la vérification de cet exemple en XNUMX minutes.
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.
Copier
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
Copier
@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},}
Copier
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 -