Formal specification in VHDL for hardware verification

Abstract

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.