The development of theorem-based design methods is considered. Theorem-based design uses formal logic to create provably correct implementations. Past work has focused on using formal logic and post-hoc proof for design verification. Here, the focus is on hardware synthesis functions, called hardware metafunctions, which synthesize hardware in a provably correct manner. Designs produced using the metafunctions are correct-by-construction and are formally related to their specifications by simple substitution or rewriting of terms within the correctness theorem for each metafunction. Typically, the metafunctions are parametric and, once proven correct, validate an entire class of designs. Theorem-based design is practical when the metafunctions and their proofs of correctness are machine-executable. This is accomplished using appropriate declarative languages with a strong formal basis and by developing the proofs of correctness using automatic theorem provers. The functional language SCHEME is used along with the Higher Order Logic (HOL) proof checker. An introduction to the use of higher-order logic as a design along with the verification of an adder array metafunction for an array multiplier is presented.>

The development of high speed, large capacity hardware systems for logic simulation makes Boolean comparison of logic networks feasible for designs of practical importance. Boolean comparison provides a complete check of functional equivalence of two logic networks and is a valuable tool in design verification. This paper describes virtual logic that controls the Boolean comparison process and provides large reductions in the required number of test cases for many practical design problems. The virtual logic is simulated by the logic simulation system at the same time as the two models are simulated for test cases. The virtual logic has the task of generating new test cases such that the entire input space is covered but minimizing the number of test vectors required. Multivalued logic simulation and other techniques are used to achieve the reductions. Since the entire Boolean comparison task is completed without assistance of a general purpose host system the usual communication overhead is avoided.

This correspondence presents a method for proof of correctness of register transfer level (RTL) parallel control sequences that describe hardware behavior. An RTL language endowed with parallel constructs is presented and its semantics is defined. The semantics includes temporal behavior. An assertion-based proof method is presented for verification of parallel control sequences described in this language. An example is given and comparisons are drawn between proofs of parallel register transfer level sequences and parallel programs. The temporal semantics associated with the language permits the construction and proof of parallel sequences that are not possible with parallel programs. Accessing shared resources outside critical regions is possible and is illustrated.

This paper extends Floyd's inductive assertion method to formal verification of register transfer level (RTL) hardware descriptions. An RTL description with imbedded assertions about machine state will be the input to the verifier. The formal semantics of an RTL language for synchronous designs are defined, to make mechanical generation of verification conditions (VC's) possible. These VC's are to be fed to a theorem prover. Proof of all the VC's constitutes complete verification. The semantic rules define how time advances, in addition to how machine variables change. These rules make possible verification of real-time performance as well as logical correctness. Such real-time performance verification is important for some hardware designs. The paper also emphasizes the differences between software and hardware verification. An example is given to illustrate the formal verification method.

A descriptive notation is proposed for microprogramming which uses conventional sequential machine notation for the microprogram, and a register transfer language to define microoperations. The combination allows the definition of useful formal transformations which preserve system behavior. The transformations correspond to paralleling and disassembling microoperations in time and altering the control unit appropriately to preserve the original behavior.

Languages for describing digital systems have two messages to convey. They must provide enough information about the behavior of the system to permit simulation, and enough information about the structure of the system to indicate how it might be built. This double requirement distinguishes system description languages from conventional programming languages and necessitates special methods for documenting the meaning of the language. Such languages have a single form, or syntax, but two meanings, or semantics. Documentation of the language requires the definition of two distinct meanings.