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/pub/users/stevens/. 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'.