Verification of Register Transfer Level (RTL) Designs

Alberto Palacios PAWLOVSKY; Sachio NAITO

Verification of Register Transfer Level (RTL) Designs

Alberto Palacios PAWLOVSKY, Sachio NAITO

Full Text Views

0

Cite this

Summary :

This paper describes a new method for verifying designs at the RTL with respect to their specifications at the functional level. The base of the verification method shown here is the translation of the specification and design representations to graph models, where the descriptions common to both representations have a symbolic representation. These symbol labeled graphs are then simplified and, by solving the all node-pair path expression problem for them, a pair of regular expressions is obtained for every two nodes in the graphs. The first regular expression in each pair represents the flow of control and the second one the flow of data between the corresponding nodes. The process of verification is carried out by checking whether or not every pair of regular expressions of the specification has a corresponding pair in the design.

Publication: IEICE TRANSACTIONS on Information Vol.E75-D No.6 pp.785-791

Publication Date: 1992/11/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Issue on Pacific Rim International Symposium on Fault Tolerant Systems)

Category

Cite this

Copy

Alberto Palacios PAWLOVSKY, Sachio NAITO, "Verification of Register Transfer Level (RTL) Designs" in IEICE TRANSACTIONS on Information, vol. E75-D, no. 6, pp. 785-791, November 1992, doi: .
Abstract: This paper describes a new method for verifying designs at the RTL with respect to their specifications at the functional level. The base of the verification method shown here is the translation of the specification and design representations to graph models, where the descriptions common to both representations have a symbolic representation. These symbol labeled graphs are then simplified and, by solving the all node-pair path expression problem for them, a pair of regular expressions is obtained for every two nodes in the graphs. The first regular expression in each pair represents the flow of control and the second one the flow of data between the corresponding nodes. The process of verification is carried out by checking whether or not every pair of regular expressions of the specification has a corresponding pair in the design.
URL: https://global.ieice.org/en_transactions/information/10.1587/e75-d_6_785/_p

Copy

@ARTICLE{e75-d_6_785,
author={Alberto Palacios PAWLOVSKY, Sachio NAITO, },
journal={IEICE TRANSACTIONS on Information},
title={Verification of Register Transfer Level (RTL) Designs},
year={1992},
volume={E75-D},
number={6},
pages={785-791},
abstract={This paper describes a new method for verifying designs at the RTL with respect to their specifications at the functional level. The base of the verification method shown here is the translation of the specification and design representations to graph models, where the descriptions common to both representations have a symbolic representation. These symbol labeled graphs are then simplified and, by solving the all node-pair path expression problem for them, a pair of regular expressions is obtained for every two nodes in the graphs. The first regular expression in each pair represents the flow of control and the second one the flow of data between the corresponding nodes. The process of verification is carried out by checking whether or not every pair of regular expressions of the specification has a corresponding pair in the design.},
keywords={},
doi={},
ISSN={},
month={November},}

Copy

TY - JOUR
TI - Verification of Register Transfer Level (RTL) Designs
T2 - IEICE TRANSACTIONS on Information
SP - 785
EP - 791
AU - Alberto Palacios PAWLOVSKY
AU - Sachio NAITO
PY - 1992
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E75-D
IS - 6
JA - IEICE TRANSACTIONS on Information
Y1 - November 1992
AB - This paper describes a new method for verifying designs at the RTL with respect to their specifications at the functional level. The base of the verification method shown here is the translation of the specification and design representations to graph models, where the descriptions common to both representations have a symbolic representation. These symbol labeled graphs are then simplified and, by solving the all node-pair path expression problem for them, a pair of regular expressions is obtained for every two nodes in the graphs. The first regular expression in each pair represents the flow of control and the second one the flow of data between the corresponding nodes. The process of verification is carried out by checking whether or not every pair of regular expressions of the specification has a corresponding pair in the design.
ER -