Model Checking for a Functional Hardware Description Language
J. Nathan Foster · 2002
We present a verification tool for the functional hardware description language SAFL. Model checking [JGP99] is a popular verification technique. Given a model of a finite state transition system, and a temporal logic specification, a model checker determines if the model satisfies the specification. Advantages of model checking over other verification techniques are that it is fully automatic, and can produce counter examples for false specifications. We have developed a model checker which uses the SAFL language as the modelling language. SAFL [MS00] is a functional hardware description language. As a result of this project, the same SAFL description can be used to describe a circuit and as a model for model checking. No separate model of the system is needed. It is hoped that this will make verification a regular part of the development process for SAFL programs. Just as a static type checker enforces safety properties for a programming language, we would like to see our model checker used to verify user-defined temporal