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, version 2.3, comes with the following files.
Currently we only have an executable for a sparc machine.
If you need an executable for another machine or the source code (in C),
please let us know.
manual, a brief manual on VERDECT in plain ascii.
about.ps, a brief paper in postscript on VERDECT,
which appeared in IEEE newsletter of TCCA.
verdect, the executable for a sparc machine.
examples, a directory containing several subdirectories with
basic examples, examples relating to micropipelines,
examples relating to the counterflow processor,
and examples illustrating what VERDECT cannot do.
libraries, a directory containing two small libraries of
frequently used basic elements.
It's available by ftp from
Contact: Jo Ebergen, Computer Science Department, University of Waterloo,
Waterloo, Ontario, N2L 3G1 (email@example.com)