Process spaces and formal verification of asynchronous circuits

Abstract

This thesis proposes process spaces, a simple and unified treatment for concurrency issues such as parallel composition, refinement, deadlock, livelock, and starvation. Processes are modeled as contracts over which executions may occur. The main innovation is that executions are abstract: this leads to a very general model. For trace-based executions, process spaces relate closely to trace theory and CSP, except that we do not attach alphabets or connectivity restrictions to processes.

We revise several algebraic properties of process compositions and comparisons that are commonly known from concurrency theory. A novel transform reveals symmetries among usual process operations.

For finite-trace processes, we have a tool that uses a public-domain BDD library. This tool fully supports modular and hierarchical verification, and draws on the flexibility of the underlying formalism to address several niche applications. One application is to detect switch-level faults in asynchronous MOS circuits. Another is to verify sufficiency of relative delay constraints by handling them as metric-free processes, without requiring post-layout numerical information on delays.

By comparing processes for liveness and progress, we obtain a classification of concurrency faults. We also determine links among implicit liveness, progress, and safety properties, so one can specify just the simpler safety properties, and then assume typical liveness and progress properties. We briefly discuss some promising applications that involve analog trajectories and true concurrency.

To handle relabelings, hidings, and derivatives, we construct them as process maps arising from relations on execution sets. We obtain several algebraic properties, including criteria for performing verifications on images of processes by over-approximation, under-approximation, and independence with respect to such maps.