VERDECT
From: jebergen@uwaterloo.ca
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.
-
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.
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.
It's available by ftp from
here
(maveric0.uwaterloo.ca:/pub/software/verdect2.3_sparc.tar.gz)
Contact: Jo Ebergen, Computer Science Department, University of Waterloo,
Waterloo, Ontario, N2L 3G1 (jebergen@uwaterloo.edu)