Abstract :
As long as simulation is relied upon, the hardware will only be as good as the test data; therefore most widely used computers contain bugs. Verification is the only known technique for theoretically complete debugging, but it remains impractical despite researchers´ efforts. This article explores a methodology in between functional simulation and formal verification. The correctness of hardware is specified as in formal verification. Input and output assertions are given in predicate calculus. Then, instead of showing that output assertions will be satisfied by the functional specification of hardware for all inputs that satisfy input assertions, it is shown that this relation holds for selected inputs. The triple, input assertion, hardware specification, and output assertion are run against test data. The advantage of this method over functional simulation is that the output data are automatically checked for correctness. The advantage over formal verification is that processes can be executed without being penalized by the incompleteness and inefficiency of theorem provers. Concurrent Prolog provides a readable, efficient compromise between functional simulation and formal verification of VLSI chip design. It is well suited for simulation of component systems and may become the language of choice for this application.
