Using partial-order semantics to avoid the state explosion problem in asynchronous systems

Abstract

We avoid state explosion in model checking of delay-insensitive VLSI systems by not using states. Systems are networks of communicating finite-state nonsequential processes with well-behaved nondeterministic choice. A specification strategy based on partial orders allows precise description of the branching and recurrence structure of processes. Process behaviors are modelled by pomsets, but (discrete) sets of pomsets with implicit branching structure are replaced by pomtrees, which have finite presentations by (automaton-like) behavior machines. The latter distinguish both concurrency and branching points, and define a finite recurrence structure. Safety and liveness checking are integrated. In contrast to state methods, our methods do not require enumeration or recording of states. We avoid separate consideration of execution sequences that do not differ in their partial order, and ensure termination by recording only a small number of system loop cutpoints -- in the form of system behavior states. In spite of the name, behavior states are not states.