Asynchronous Circuit Verication Using Trace Theory and CCS

We investigate asynchronous circuit verication using Dill's trace theory [1] as well as Milner's CCS (as mechanized by the Concur-rency Workbench). Trace theory is a formalism specically designed for asynchronous circuit specication and verication. CCS is a gen-eral purpose calculus of communicating systems that is being recently applied for hardware specication and verication [2]. Although both formalisms are similar in many respects, we nd that there are many interesting dierences between them when applied to asynchronous cir-cuit specication and verication. The purpose of this paper is to point out these dierences, many of which are precautions for avoiding writ-ing incorrect specications. A long-term objective of this work is to nd a way to take advantage of the strengths of both the Trace The-ory verier and the Concurrency Workbench in verifying asynchronous circuits.