Fundamental Hardware Design in PVS

Abstract

The development of Programmable Logic Devices (PLDs) has introduced programming as a primary tool in the development of digital circuits. This work attempts to create a generic verification environment in which designs can be specified and verified using the Prototype Verification System (PVS). This is accomplished by providing library support for general hardware constructs. The environment is intended for use with any PLD and any PLD programming language. The goal of the environment is to allow the easy translation of digital designs to PVS and provide sufficient support to make verification possible without a great deal of effort.