Formal specification in VHDL for hardware verification
Ralf Reetz, Klaus Schneider, Thomas Kröpf · 1998
In this paper, we enrich VHDL with new specification constructs intended for hardware verification. Using our extensions, total correctness properties may now be stated whereas only partial correctness can be expressed using the standard VHDL assert statement. All relevant properties can now be specified in such a way that the designer does not need to use formalisms like temporal logics. As the specifications are independent from a certain formalism, there is no restriction to a certain hardware verification approach. 1 Introduction As VHDL [1] is an important IEEE standard for describing digital circuits, many commercial design tools are based on this hardware description language. Originally created for simulation, this language has recently been used also for formal verification [2] to ensure the correctness of designs. However, VHDL itself is only intended for describing the implementation of a system for synthesis or simulation. For capturing the system specification, only the ...