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 on Ken's WWW site http://kdstevens.com/~stevens/analyze-page.html.