Title :
Verification of hardware descriptions at the functional level
Author :
Pawlovsky, Alberto Palacios ; Naito, Sachio
Author_Institution :
Dept. of Electr. & Electron. Eng., Nagaoka Univ. of Technol., Niigata, Japan
Abstract :
A method is presented for the functional verification of designs at the register transfer level. The verification of correctness is taken as a basic specification of the design given in a functional specification language. The verification procedure is based on the identification of observable control signals (OC) and observable actions (OA) in the specification and design descriptions. The OCs and OAs are then taken as a base for the conversion of the descriptions to graph forms. The graphs, reduced by graph grammars, are then used to extract two sets of regular expressions: one representing the sequence of control signals and the other one the sequence of actions taken in response to the first ones. Finally, the verification procedure checks if the sets of the specification are subsets of the design´s sets
Keywords :
formal specification; logic CAD; program verification; functional level; functional specification language; functional verification; graph grammars; hardware descriptions; observable actions; observable control signals; register transfer level; Context modeling; Hardware; Signal design; Specification languages;
Conference_Titel :
TENCON '89. Fourth IEEE Region 10 International Conference
Conference_Location :
Bombay
DOI :
10.1109/TENCON.1989.176902