An automatically verified generalized multifunction arithmetic pipeline
Matthias Mutz · 1994
The verification of sequential circuits with complex datapaths and non-trivial timing behavior is a difficult task. A multifunctional pipline is described as an example of such a circuit automatically verified by a verification procedure. The paper aims at presenting a possible target for hardware verification methods both for hardware designers interested in applying such methods and researchers developing such methods. 1. INTRODUCTION There is much doubt by designers concerning the practicability of current verification systems in hardware design. There are only a few examples of circuits verified on the basis of formal methods, which in principle also (but possibly not in practice) could be validated by simulation. Of course, there are some examples, e.g. [Joy 88]. Indeed, verification methods and simulation often significantly differ, especially when a partial specification is verified or when a correctness proof is established within a formal framework. Verification means to compa...