The Role of a Symbolic Programming Language in Hardware Verification: The Case of Maple
Farhad Mavaddat · Birkhäuser Boston eBooks · 1993
There is some reluctance towards the use of formal verification methods by the design community. One factor contributing to this lack of enthusiasm is the degree of user sophistication required in representing a design and reasoning about it in most systems, especially those involving theorem provers. To overcome this, we present the use of symbolic programming languages to prove several classes of hardware designs correct. We start by defining a functional model for the specification of synchronous hardware. Next, we discuss the programming techniques for implementing the model in the symbolic programming language Maple. Given a Maple model (a program) of a design, we execute the program to derive its symbolic behaviour. The Maple system is also used to compare the derived and the reference behaviours. We end by presenting several Maple-based verification examples. Our contribution to hardware verification is the development of a modeling method within a symbolic programming paradigm, and the ensuing facility for reasoning about certain designs. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.