###
PROCESS SPACES AND FORMAL VERIFICATION OF ASYNCHRONOUS CIRCUITS

*RADU NEGULESCU*
Ph.D. Thesis

Department of Computer Science

University of Waterloo

Waterloo, Ontario, Canada N2L 3G1

** 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.