ASYNCHRONOUS TOOLS
                                       
          Budi Rahardjo 
          Electrical and Computer Engineering
          University of Manitoba
          15 Gillson Street
          Winnipeg, Manitoba
          Canada - R3T 5V6
          
   
     _________________________________________________________________
   
   $Id: asynctools.html,v 1.5 1995/11/11 22:05:07 rahard Exp rahard $
     _________________________________________________________________
   
   
   
   This is a summary of publicly available asynchronous tools. Most of
   the tools are available over the Internet, while others are available
   by sending a request to the author(s) or contact person(s). I
   understand that there are other tools out there, unfortunatly they are
   not available for public use.
   
   The information was collected from many people (see the
   acknowledgement), with their original comments. I have added
   additional information. This file is available through WWW at
   http://www.ee.umanitoba.ca/~rahard/asynctools.html. An text version is
   available as ftp://ftp.ee.umanitoba.ca/pub/asynchronous/asynctools or
   available through WWW at
   http://www.cs.man.ac.uk/amulet/async/async_tools.html.
   
   I will maintain this information. Corrections and comments, are
   welcomed. I should mention that I did not have a chance to test
   individual tools.
     _________________________________________________________________
   
Table of contents

     * Acknowledgements
     * SIS
     * FORCAGE
     * MEAT
     * SMV, CSML, and MCB
     * VERDECT
     * SYN
     * ASSASSIN
     * Synchronized Transitions
     * 3D
     * Analyze
     * VERSIFY
     * PETRIFY
     * Other tools
       
   
     _________________________________________________________________
   
SIS

   Contributor: Luciano Lavagno 
   
   SIS, the UCB sequential synthesis system, that offers asynchronous
   synthesis as well as synchronous sequential and combinational
   multi-level logic synthesis capabilities. Its asynchronous package was
   developed by myself, Cho Moon and Paul Stephan, so we can also provide
   assistance in bug fixing and so on. It is written in C, and has been
   ported to most workstations (DEC, SUN, IBM) without problems. It is
   available with source code.
   
   The specification formalism, Chu's Signal Transition Graph, is similar
   to timing diagrams: the user defines which transitions cause which
   transitions. E.g. a rising transition on the set input of a set-reset
   flip-flop causes a rising transition on the Q output, this causes a
   falling transition on the QBAR output, and so on. More formally, the
   STG is an interpreted Petri net. An FSM-style input will also be
   provided for users who prefer it (even though it allows less
   optimizations, and hence it is discouraged).
   
   It uses two different delay models for synthesis, one where the logic
   is assumed to be implemented as two-level logic gates with no bounds
   on the amount of delays of each gate, and one where each gate and wire
   has a bounded delay (given by the implementation library description).
   
   
   The system can perform the following operations:
    1. check of some properties (e.g. liveness) of the specification.
    2. state assignment (if required).
    3. synthesis of an initial implementation as a logic network.
    4. constrained optimization of this logic network (avoiding to
       introduce hazards).
    5. technology mapping onto a specific standard cell-like library,
       inserting delay buffers whenever necessary to produce a
       hazard-free logic.
       
   
   
   There is a set of papers and a sort of user's manual that leads you
   through a set of examples of how to use the system.
   
   SIS is available through anonymous FTP at
   ftp://ic.eecs.berkeley.edu/pub/Sis Contact person:
    Luciano Lavagno.
   Note that there are two "versions" of SIS. Contact for the "supported"
   one is:  (for "registration" purposes, so that
   you can be notified when there is an upgrade.)
     _________________________________________________________________
   
FORCAGE

   Contributors:
   
          Luciano Lavagno 
          Michael Kishinevsky 
          
   
   
   FORCAGE is a speed-independent circuit analysis and synthesis package
   developed by M. Kishinevsky, A. Kondratyev, A. Taubin, V. Varshavsky
   et al. at St. Petersburg, Russia, The University of Aizu, Japan and
   Technical University of Denmark.
   It runs on IBM PCs and clones and includes:
   
    TRANAL
    
   analyzes a circuit for speed-independence (semi-modularity) by all
   states traversal.
   
    TRASPEC
    
   analyzes a circuit for speed-independence (distributivity - the most
   common case of semi-modularity) and constructs a Change Diagram
   describing behavior of the circuit. Contrary to TRANAL this system
   implements a polynomial algorithm of a circuit analysis that does not
   restore all states of the circuit.
   
    TRASYN
    
   verifies implementability of a Change Diagram specification and
   synthesizes a speed-independent circuit implementing the
   specification.
   
   A theory underlying the FORCAGE is given in the book:
   Michael Kishinevsky, Alex Kondratyev, Alexander Taubin and Victor
   Varshavsky. "Concurrent Hardware. The Theory and Practice of
   Self-Timed Design" , John Wiley and Sons, Dec. 1993, ISBN 0471 93536
   0.
   
   Sections 1.2 and 2.1
          a theory for the TRANAL system
          
   Chapters 1 (Section 1.3), 2, 3 and 6 (sections 6.1 - 6.3)
          a theory for the TRASYN system
          
   Chapter 4
          a theory for the TRASPEC system. (for the TRASPEC theory see
          also the paper of the same authors: "Analysis and
          Identification of Speed-independent Circuits on an Event
          Model", Formal Methods in System Design, vol.4, No.1, 1994.)
          
   FORCAGE (for MS-DOS machines) is available through anonymous FTP
    1. ftp://ftp.ee.umanitoba.ca/pub/asynchronous/forcage.zip

(these are no longer available)
    1. ftp://ftp.id.dtu.dk/pub/forcage/forcage3.zip
    2. ftp://ftp.id.dtu.dk/pub/forcage/forcage3.arj
    3. ftp://ftp.id.dtu.dk/pub/forcage/forcage3.zip
    4. ftp://ftp.id.dtu.dk/pub/forcage/forcage3.arj
       
   Contact person: Michael Kishinevsky 
   
   A program for performance analysis of speed-independent circuits
   compatible with FORCAGE is available as
   ftp://ftp.id.dtu.dk/pub/timesim/timesim.tar.Z and
   ftp.id.dtu.dk:/pub/timesim/timesim.tar.Z. Given a (cyclic) Signal
   Graph as input, it computes the cycle time and critical cycles. It
   runs under Unix. (Implemented by Christian Nielsen, Technical
   University of Denmark)
   
  View from outside:
  
   From: Luciano Lavagno 
   
   The specification [in Forcage] is pretty much the same as STG's,
   except that it does not handle data-dependent computation. I.e. in
   every "state" of the system only a well defined set of transitions can
   occur, and in order to model, e.g., read and write cycles of a bus you
   need to use some "tricks". This apparently is not a great limitation,
   because the authors have been able to use it to design realistic
   circuits. The delay model is unbounded gate delays with realistic
   gates (various types: either NAND/NOR or complex CMOS AND-OR-INVERT
   gates can be used).
   
   It does:
     * checks of liveness and so on of the specification.
     * synthesis in a technology chosen among one of the available ones
       (I am aware on NAND/NOR and AND-OR-INVERT).
     * verification of the speed-independence of the implementation (or
       of hand-designed circuits).
       
   
     _________________________________________________________________
   
MEAT

   Contributor: Ken Stevens 
   
   MEAT -- The Most Excellent Asynchronous Tool, dudes!. It is available
   through anonymous ftp
     * ftp://ftp.cpsc.ucalgary.ca/pub/users/stevens
       
   
   
   Taken from the documentation (meat.doc) :
   
  HISTORY
  
   
   
   This is part of a tool set that was developed here at HP Labs to help
   with the development of a large 300,000 transistor asynchronous
   communication chip called the Post Office. During the design of the
   Post Office, we noticed that an inordinately large amount of time was
   spent in the process of turning state machine specifications into
   implementations. Most of this was done in a very "Unger-esque" style,
   and we figured could be quite easily implemented in Software. Grinding
   all the minimizations through by had was also very error prone.
   
   Al took the challenge and made Ken a bet that within 3 weeks given a
   sum of products input he could output correct asynchronous covering
   using a Quine-McCluskey like algorithm. Well, he got it working, but
   tuning the performance to make it efficient took several months!
   
   Bill hacked up some code that takes a state machine specification and
   generates the maximal compatibles. The user then selects the
   compatibles and his code will do the state assignment and output the
   unreduced logic equations. This is an Unger like reduction and uses
   the Tracey algorithm, and is a front end to the asynchronous logic
   minimizer.
   
   Ken hacked up a back-end to the Logic Minimization that does CMOS
   transistor minimization, and generates a schematic for the circuit.
   This was interfaced to the design tool we've been using called
   Electric(tm), and so it hasn't been included. If you are interested,
   we can send you the code that does the transistor minimization.
   
   Steve Nowick also interfaced Bill's interface to the Asynchronous
   Verification tool that is being designed at Stanford under the
   direction of David Dill. (This is not included, either). ...
     _________________________________________________________________
   
SMV, CSML, and MCB

   Contributor: David Long  (editor
   note: the address is invalid.)
   
   SMV -- a symbolic model checker for CTL [latest revision 2.4.2]. It is
   available as ftp://emc.cs.cmu.edu/pub/tape
   
   A BDD-based symbolic model checking program (SMV) that can handle
   asynchronous systems is available for FTP from tempura.logi.cs.cmu.edu
   It is not specifically geared to asynchronous circuits, but you may
   find it useful.
   
   CSML is a high level level language for describing finite state
   machines. There is a compiler which produces a finite state machine as
   output. There is also a CTL model checker called MCB which accepts the
   state machine file as input. MCB is an enhanced version of the EMC
   model checker.
   
   A BDD library with extensions for sequential verification is
   available. The libraries main features include:
     * Stuff for sequential verification, such as routines for relational
       product and frontier set simplification
     * Pointer flags for output negation, input negation, and "else
       negation"
     * Unified result cache for all operations. All operations, including
       things like multi-variable quantification and simultaneous
       substitution, cache across calls
     * Routines for node profiles (histograms of the number of nodes at
       each level) and function profiles (histograms of the number of
       functions obtainable by restricting variables above each level)
       for analyzing BDD sizes.
     * Routines for dumping BDDs to files and loading them again
     * Garbage collection via either reference counting or "keep only
       these"
     * Settable node limit. Operations abort and clean up their
       intermediates if they cannot finish without the total number of
       nodes exceeding the limit.
     * Very small and fast. Should be fairly portable across 32-bit
       machines running UNIX. If you're not running UNIX, you'll have to
       modify the memory management routines (the package implements a
       buddy scheme and calls sbrk directly).
       
   Papers on various related topics.
    1. ftp://emc.cs.cmu.edu/pub/bdd/futurebus.ps is a paper describing
       the formal verification of the Futurebus+ cache coherence
       protocol.
    2. K.L. McMillan and J. Schwalbe, "Formal Verification of the Encore
       Gigamax Cache Consistency Protocols," International Symposiym on
       Shared Memory Multiprocessors, 1991. It is available as
       ftp://emc.cs.cmu.edu/pub/tape/ISSMM.ps
    3. ftp://emc.cs.cmu.edu/pub/tape/SMC.ps is the paper "Symbolic Model
       Checking: 10^20 States and Beyond".
       
   
     _________________________________________________________________
   
VERDECT

   Contributors:
     * Ken Stevens 
     * Jo Ebergen 
       
   VERDECT can be used for the verification of speed-independent or
   delay-insensitive circuits, in particular control circuits. VERDECT
   has a simple user interface, can verify safety and various progress
   conditions, and allows a modular verification.
   
   VERDECT is able to verify specifications and implementations written
   in "commands", a CSP-like notation. It's available from:
   href=ftp://maveric0.uwaterloo.ca/pub/software/verdect2.3_sparc.tar.gz
   Contact person:
   
          Jo Ebergen
          Computer Science Department
          University of Waterloo
          Waterloo, Ontario, N2L 3G1
          jebergen@maytag.waterloo.edu
          
   
     _________________________________________________________________
   
SYN

   Contributor: Peter Beerel 
   
   SYN 2.01, Synthesis of speed-independent circuits
   
  SPECIFICATION:
  
   State Graph specification description which satisfies complete state
   coding (CSC) and is distributive with input choice.
   
  IMPLEMENTATION:
    1. Net list description of speed-independent circuit.
    2. Specification and implementation files compatible with AVER, a
       speed-independent circuit verifier written by Dave Dill
       (dill@hohum.stanford.edu).
       
  DELAY MODEL:
  
   Unbounded gate delay model
   
  BASIC GATES USED:
  
   ANDs, ORs, C_Elements with unlimited fanin and possible attached input
   inverters.
   
  CONNECTION WITH OTHER TOOLS:
  
   I have modified a version of SIS to generate the low-level state graph
   from an STG. I have also written a converter from extended burst-mode
   FSMs (kyy@paperchase.stanford.edu, nowick@cs.stanford.edu) to state
   graphs with semi-automated state variable insertion. Both are
   available upon request.
   
  EXTENSIONS:
  
   SYN 3.0 soon to be available (hopefully): Synthesis with basic gates
   with limited fanin.
   
  AVAILABILITY:
  
   SYN 2.01 can be obtained through anonymous FTP
   ftp://snooze.stanford.edu/pub/tools/SYN/. Associated papers (TAU '92
   and ICCAD '92) are also FTPable. Contact person:
   
          Peter Beerel
          pabeerel@viterbi.stanford.edu
          AEL 007
          Stanford University
          Stanford, CA 94305
          (415)-723-9510
          
   
     _________________________________________________________________
   
ASSASSIN

   Availability: ftp://imec.be/pub/vsdm/SW-distrib/assassin/
   Contributor: Chantal Ykman 
   
   ASSASSIN is the IMEC compiler for synthesis and analysis of
   asynchronous control circuits. It is an evolving system being
   developed by Peter Vanbekbergen, Chantal Ykman, and Bill Lin. The
   software is written in "C" and should be portable to most workstation
   platforms.
   
   The specification formalism used is a general "Timed" Signal
   Transition Graph (STG) Model. This model extends Chu's Signal
   Transition Graph model in a number of important ways. These extensions
   were required to specify and synthesize a wide class of industrial
   applications. For example, new types of events and Boolean guards have
   been introduced to permit the specification of mixed mode
   asynchronous/synchronous behavior. In addition, general Petri nets
   with complex conditional behaviors are permitted in our model, which
   is necessary to capture arbitration protocols. Also, timing semantics
   have been defined to model environmental requirements and assumptions.
   Other models, such as timing diagrams, may be translated to the timed
   STG model.
   
   For the timed STG model, a number of algorithms have been developed to
   synthesize realistic design problems automatically. Some work at the
   STG level while others work on a state graph (SG) model. At the STG
   level, methods have been developed that can be used to synthesize and
   optimize circuits directly from the STG without first generating a
   state graph, where state explosion may occur. These methods enables
   synthesis of highly concurrent specifications, coming up with
   solutions where concurrency can be reduced in place of introducing
   unnecessary state signals, as well as taking into account complex
   timing constraints. At the state graph level, methods have been
   developed for exploring a large solution space where concurrency can
   be reduced and where new state signal transitions may be added in a
   concurrent way. These methods have the important advantage that they
   can be applied to a very large class of extended STG's, even non-STG
   formalisms as long as an initial state graph consistent with
   interleaved semantics can be derived. Contact persons:
   
          Bill Lin ,
          Chantal Ykman 
          
   
     _________________________________________________________________
   
Synchronized Transitions

   Contributor: Budi Rahardjo 
   
   Synchronized transition (ST) is a methodology advocated by J.
   Staunstrup. (See J. Staunstrup, A Formal Approach to Hardware Design,
   Kluwer Academic Publishers, 1994. ISBN:0-7923-9427-5.) There is a set
   of tools to translate the description to a C program or to a
   description that can be fed to LP, the Larch Prover. ST tools are
   available through anonymous FTP at
   ftp://ftp.std.com/Kluwer/software/synchronized_transitions
   
   Contact person: 
     _________________________________________________________________
   
3D

   Contributor: Kenneth Yun 
   
   3D v3.02, Mixed Asynchronous / Synchronous Synthesis Tool
   
  SPECIFICATION:
  
   Extended-burst-mode Specification (cf: ICCAD'93 "Unifying
   Synchronous/Asynchronous State Machine Synthesis" by Yun and Dill and
   ICCAD'94 "Performance-driven Synthesis of Asynchronous Controllers" by
   Yun, Lin, Dill, and Devadas)
   
   Range of specifiable behavior:
    1. Restricted multiple-input change (input burst) with don't-care
       inputs allowed
    2. Input choices based on sampling possibly glitchy signals
       
  IMPLEMENTATION:
  
   Target implementation is a combinational circuit with both primary
   outputs and state variables fed back.
    1. Two-level PLA description of outputs and state variables
    2. Verilog netlist using a customizable CMOS standard cell/gate array
       technology mapper
       
   Note:
    1. The 3D tools makes use of Steve Nowick's exact logic minimizer
       (nowick@cs.columbia.edu) to generate minimized logic equations. An
       alternative combinational logic minimizer based on BDD
       descriptions is under construction. (ICCAD'94).
    2. An algebraic technology mapper (included in the distribution)
       generates a Verilog netlist from each two-level logic equation.
       The CMOS library that comes with the mapper is easily
       customizable.
       
  DELAY MODEL:
  
   Bounded wire delay model
   
  CONNECTION WITH OTHER TOOLS:
  
   The 3D tool has been incorporated as a part of a larger asynchronous
   synthesis system called STETSON available from HP Labs.
   
  AVAILABILITY:
  
   3D v3.02 can be obtained through anonymous FTP from
   snooze.stanford.edu. Associated papers (ICCAD'94, ICCAD'93, EDAC'93,
   ICCAD'92, ICCD'92) are also available at the same site. Contact
   person:
   
          Kenneth Y. Yun
          kyy@paradise.ucsd.edu
          Department of Electrical and Computer Engineering
          University of California, San Diego
          9500 Gilman Drive
          La Jolla, CA 92093-0407
          (619) 534-6365
          
   
     _________________________________________________________________
   
Analyze

   Contributor: Ken Stevens 
   
   I have been developing a new tool called `Analyze'. Analyze uses
   formal methods for circuit synthesis and verification. Although it is
   still in its infancy, it has many delay models you can use to verify
   circuits -- my burst-mode model, the delay-insensitive model, DI plus
   isochronous forks, and the speed-independent. It also can use several
   different equality formalisms, including trace semantics and
   bisimulation. The design of CCS lends itself well to specifications
   and tool-directed top-down synthesis.
   
   The tool is currently available for FTP in the `pub' directory of
   `phred.cpsc.ucalgary.ca'. The source is in the file `analyze.tar.Z',
   and an examples file with examples to help get you started are in
   `analyze-examples.tar'.
   ftp://phred.cpsc.ucalgary.ca/pub/users/stevens/
     _________________________________________________________________
   
VERSIFY

   Contributor: Oriol Roig 
   Availability: http://www.ac.upc.es/vlsi (binaries for SunOS and HP-UX
   only)
   
   A CAD tool for the verification of speed-independent circuits. The
   circuit is verified against a Signal Transition Graph specification.
     _________________________________________________________________
   
PETRIFY

   Contributor: Alex Yakovlev 
   Availability: ftp://ftp.ac.upc.es/pub/archives/cad/petrify
   
   The is a Software Tool called "PETRIFY" (main developer and contact
   person is J. Cortadella, jordic@ac.upc.es) whose main functionality is
   synthesis of Petri nets from state graphs (defined as FSM nets) and
   Petri net transformations.
   
   In the ftp site you will find:
     * UPC-DAC-95-09.ps.gz (the technical report)
     * petrify-1.0.tar.gz (the software)
       
   
     _________________________________________________________________
   
Other tools

    1. Contributor: Luciano Lavagno 
       
       There are also other people who arew working on developing such
       systems. You may want to contact them as well (I have no precise
       information on availability/capabilities of their tools):
          + Tam-Anh Chu tchu%cirrusl@oliveb.atc.olivetti.com
   
       
    2. Contributor: Ruchir Puri 
       
       If You are utilizing FSM specifications, (like Ken) then you might
       like to look at my paper on:
       
       An Efficient Algo. for finding Minimal Closed Covers in FSMs.
       Which will appear in the April issue of IEEE Transactions on CAD.
       
       Right now I am working on the Modular Synthesis and am
       incoroporating the Top Down and Bottom up Async Synthesis from
       STGs. I have bits of code running but will still take some time
       before the system is ready.
    3. Contributor: polly@howdy.stanford.edu
       
       A set of tools called STETSON will be available.
       
   
     _________________________________________________________________
   
Acknowledgements

   Thank you goes to the following people (in random order) for providing
   the information :
     *  Luciano Lavagno
     *  Michael Kishinevsky
     *  Sean Morley
     *  Ken Stevens
     *  Steve Nowick
     *  David Long
     *  Ruchir Puri
     *  Peter Beerel
     *  Jo Ebergen
     *  Chantal Ykman
     *  Polly Siegel
     *  Al Davis
     *  Kenneth Yun
     *  Nigel Paver
     *  Jo Depreitere
     *  Jim Garside
     *  Oriol Roig
       
   (Did I forget your name ?)
   
   Special thanks to Nigel Paver for creating the original HTML version
   of this list.
     _________________________________________________________________
   
   Budi Rahardjo rahard@ee.umanitoba.ca 
-- 
Budi Rahardjo
                 
Electrical and Computer Engineering - University of Manitoba - Canada