Automatic Verification of Safety and Liveness for Pipelined Machines Using WEB Refinement

---

Panagiotis Manolios and Sudarshan K. Srinivasan. ACM Transactions on Design Automation of Electronic Systems (TODAES), © ACM

Abstract

We show how to automatically verify that complex pipelined machine models satisfy the same safety and liveness properties as their instruction-set architecture (ISA) models by using well-founded equivalence bisimulation (WEB) refinement. We show how to reduce WEB-refinement proof obligations to formulas expressible in the decidable logic of counter arithmetic with lambda expressions and uninterpreted functions (CLU). This allows us to automate the verification of the pipelined machine models by using the UCLID decision procedure to transform CLU formulas to Boolean satisfiability problems. To relate pipelined machine states to ISA states, we use the commitment and flushing refinement maps. We evaluate our work using 17 pipelined machine models that contain various features, including deep pipelines, precise exceptions, branch prediction, interrupts, and instruction queues. Our experimental results show that the overhead of proving liveness, obtained by comparing the cost of proving both safety and liveness with the cost of only proving safety, is about 17%, but depends on the refinement map used; for example, the liveness overhead is 23% when flushing is used and is negligible when commitment is used.

PDF (344K) © ACM