Verifying transaction ordering properties in unbounded bus networks through combinded algorithmic/deductive methods

Michael Jones, Ganesh Gopalakrishnan

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


We present a verification technique based on network symmetry classes along with a manually derived abstraction that allows us to show, at the bus/bridge level, that all execution traces of all acyclic PCI networks satisfy the transaction ordering property. This now completed case study suggests several avenues for further work in combining model-checking (algorithmic methods) and theorem-proving (deductive methods) in judicious ways to solve infinite-state verification problems at the bus/interconnect level. It is a concrete illustration of partitioning concerns where designers can specify bus protocols in an operational semantics (rule-based) style, invent abstractions, and carry out finite-state model-checking while verification experts can establish formal properties of the abstraction.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems