Temporal verification of behavioral descriptions in VHDL
Djamel Boussebha, Norbert Giambiasi, Janine Magnier · European Design Automation Conference · 1992
An approach for verifying the temporal scheduling of behavioral models of VHSIC hardware description language (VHDL) is presented. The aim is to verify that the control flow of a behavioral description satisfies its behavioral specifications described in a formalism based on reified temporal logics, and on a notion of physical activity. From this formalism, a verification procedure is established which starts by extracting the temporal subbehaviors from given VHDL descriptions and then gives them to the temporal demonstrator to prove whether they respect the behavioral specifications. >