Prove all things; hold fast that which is good.
—New Testament, I Thessalonians
All technology should be assumed guilty until proven innocent.
No amount of experimentation can ever prove me right; a single experiment can prove me wrong.
A common mistake that people make when trying to design something completely foolproof is to underestimate the ingenuity of complete fools.
—Douglas Adams, Mostly Harmless
When writing a specification of a circuit, we are usually trying to accomplish certain goals. For example, we may want to be sure that the protocol never leads to a deadlock or that whenever there is a request, it is followed by an acknowledgment possibly in a bounded amount of time. In order to validate that a specification will lead to a circuit that achieves these goals, simulation can be used, but this cannot guarantee complete coverage. This chapter, therefore, describes methods to verify that specifications meet their goals under all permissible delay behaviors.
After designing a circuit using one of the methods described in the previous chapters, we check the circuit by simulating a number of important cases until we are confident that it is correct. Unfortunately, anything short of exhaustive simulation will not guarantee the correctness of our design. This is especially problematic in asynchronous design, where a hazard may manifest as a failure only under a very particular set of delays. Therefore, it is necessary to use ...