From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation

The stack is an ubiquitous component in both software and hardware. It is used as an ADT in data structures, while it serves as a component from floating point units to instruction execution units. In this paper, we explore the specification and verification of a simple bounded stack at differing levels of abstraction. We use HOL theorem proving at higher abstraction levels, while using VOSS symbolic trajectory evaluation at the switch-level. This case study provided a simple context to study various issues involved in combining theorem proving and symbolic simulation. Symbolic trajectory evaluation gives us access to accurate circuit models as well as the advantage of automating most of the proof effort. Theorem-proving gives us the expressive power for specification, than would generally be possible in a model checker approach. Further, we add executability to this combination to evaluate HOL theorem prover specifications. Executing HOL specifications helps detect errors before embarking on tedious proofs.