Verification of hardware descriptions at the functional level

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