Although asynchronous systems can be based on formal handshake semantics, "equality" between behavioral descriptions and implementations has been difficult to formally define. Milner's work on CCS -- "Calculus of Communicating Systems" -- has helped me formalize and understand equalities. Bisimulation, and a property I define as "conformance" can be combined to formally prove satisfaction between arbitrary hierarchies of asynchronous components and systems and their specifications.
This tool uses CCS as an input language to analyze asynchronous circuits and verify they satisfy the specification. ANALYZE is in its infancy, and is very incomplete at this stage. The tool is coded using efficient model checking techniques, but does not used advanced data representations such as BDDs. Bisimulation and Trace equivalences are the foundational equivalences between specification and implementation. Temporal model checking, which can be used to validate the initial specification or an implementation, must be done using other tools such as the Concurrency Workbench (CWB) or the Concurrency Factory.
ANALYZE will take a CCS description and do a number of checks and expansions which are not possible using standard CCS syntax and expansion laws. This allows circuits to be analyzed in 1: speed-independent (arbitrary delay of devices), 2: delay-insensitive (arbitrary delay of devices and interconnections), and 3: burst (speed-independent with stability) modes. ANALYZE performs static checks of the implementation to ensure correct interconnection, and some specification and application requirements. Analyze will also generate CWB compatible output of minimized agents in standard normal form.
When both a specification and implementation are supplied, the implementation will be verified for satisfaction (called conformance) to the specification. Verification uses both bisimulation and trace formalisms.
Milner, Robin. "Communication and Concurrency", Prentice Hall International (UK) Ltd, 1989.
Stevens, Kenneth S. "Practical Verification and Synthesis of Low Latency Asynchronous Systems", PhD Thesis, University of Calgary, Calgary, Alberta, September 1994.
Stevens, Kenneth S. "Automatic synthesis of Fast, Compact Self-Timed State Machines", University of Calgary Research Report No. 92/495/33, December 1992.
A. L. Davis, W. S. Coates, and K. S. Stevens. "Automatic Synthesis of Fast Compact Asynchronous Control Circuits", IFIP Working Conference on Asynchronous Design Methodologies, March 1993.
Unger, Steven H. "Asynchronous Sequential Switching Circuits", 1983 Reprint by Robert E. Krieger Publishing Company, Inc., Krieger Drive, Malabar, Florida 32950 (originally published by Wiley, 1969)
Liu, Ying. "Reasoning About Asynchronous Designs In CCS", Master's Thesis, University of Calgary, Dept. of Computer & Electrical Engineering, October 1992.
Analyze was developed at the University of Calgary, under a grant from