Embedding hardware description languages in proof systems
Goossens, KGW Kees · 1992
Hardware description languages have been used in industry since the 1960s to document and simulate hardware designs. Simulation is a very useful tool to find design faults without the need to manufacture the design. A well known drawback of simulation, however, is that the number of inputs combinations (or test vectors) increases exponentially. For modern designs, it would take years to fully simulate a design. In practice a limited number of test vectors are used to probe the circuit, possibly failing to uncover faults. A response to this situation has resulted in formal verification of hardware designs. This entails using a mathematical proof system to describe the design, followed by proving correctness with respect to its specification. Most proposed methodologies are not automated, and need considerable expertise to be used. Although formal verification methods remove the exponential explosion occurring for simulation, verification takes considerable time. A severe drawback is that many notations are employed, depending on the tools which are used. Industrial hardware description languages have not yet been used, alienating the hardware verification field from the industrial designers. This work aims to address this problem. To be able to use a hardware description language in conjunction with a proof system it must have a firm mathematical basis. This work has