Ken Stevens

Associate Professor
University of Utah
Electrical and Computer Engineering
Salt Lake City UT

ANALYZE

A tool to aid in the analysis and verification of asynchronous circuits

Current design practices heavily depend on automated tool support for the time consuming tasks of circuit and system analysis and synthesis. Asynchronous design requires the same, if not greater, tool sophistication to achieve commercial quality circuits. Fortunately, the hierarchical and modular nature of asynchronous design lends itself particularly well to synthesis and verification formalism and algorithms. This is a tool which helps to fill the tool need in the domain of formal asynchronous circuit and system verification.

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.

What Analyze Does

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.

Links for downloading the source and examples

Common Lisp source for Analyze a verification tool for asynchronous circuits and systems based on bisimulation. This tool supports all the asynchronous hazard models, including Burst-Mode.
Documentation for Analyze.
Short demo presentation of Analyze.
Analyze examples from the Post Office chip and other sources.
Library of gate descriptions in CCS that Analyze can use.

REFERENCES

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 Hewlett-Packard Company.