High-level hardware verification using process algebras
Shahid Ikram · 1996
The complexity involved in designing digital systems is controlled using abstraction to hide design details. Every level of abstraction is characterized by the primitive components of that level, by the value set they manipulate and share, and by the ways to combine them to build structures. The objectives of this work are to design a rigorous formalism to model digital systems at various levels of abstraction, to verify correctness relations between the descriptions at these levels, and to model behavior under composition. We are especially interested in behavior of the register-transfer and the instruction-set level. The key idea is to find a small set of basic rules that capture the essential properties of synchronous systems at the intended levels of design. These rules are then used to develop a comprehensive theory, which includes proving a large set of theorems that characterize the behavior of complex systems and can be used in modeling and verification. To this end, we are proposing an extended automaton model for synchronous digital systems through a new process algebra called IspCal or instruction set process calculus. An operational semantics and a trace semantics are defined for the IspCal operators. Based upon these two semantics, two alternative notions of equivalence are devised for the IspCal terms. It is shown why one of the equivalence offers a better model then the other. The syntax, the trace semantics, the operational semantics, and the equivalence relations are embedded in the Cambridge HOL theorem prover. A set of theorems is derived from this embedding showing that the proposed semantics behave in accordance with the general understanding of digital systems. Furthermore, it is shown that the proposed equivalence relations are congruent over the IspCal operators. This gives IspCal a much desired property of substitutivity, which is vitally important for hierarchical design and verification. Finally, a set of theorems is derived that allows expansion of structural descriptions of agents in IspCal into behavioral descriptions and therefore provides efficient means to verify implementations against the specifications.