FORCAGE
FORCAGE , the speedindependent 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 PC's and clones and includes:
TRANAL
analyzes a circuit for speedindependence (semimodularity)
by all states traversal.
TRASPEC
analyzes a circuit for speedindependence (distributivity 
the most common case of semimodularity) 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 speedindependent
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 SelfTimed 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 and
Chapter 4  a theory for the TRASPEC system.
(for the TRASPEC theory see also the paper of the same authors:
"Analysis and Identification of Speedindependent Circuits on
an Event Model", Formal Methods in System Design, vol.4,
No.1, 1994.)
FORCAGE (for MSDOS machines) is available through anonymous FTP
in .zip format or
in .arj format
(ftp.id.dtu.dk:/pub/forcage/forcage3.zip, /pub/forcage/forcage3.arj) and also
from here.
Contact: Michael Kishinevsky:
kishinev@uaizu.ac.jp
A program for PERFORMANCE ANALYSIS of speedindependent circuits
compatible with FORCAGE is available from
here
(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
(lavagno@polito.it)
The specification [in Forcage] is pretty much the same as STG's, except
that it does not handle datadependent 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 ANDORINVERT 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 ANDORINVERT).
 verification of the speedindependence of the implementation (or of
handdesigned circuits).
