BENCHMARKS

1. Benchmarks from Germany

FREE SOFTWARE

1. Some relevant software that could be used as part of a verification course. Page with all other software.
2. Page with VIS software for verification.
   VIS (Verification Interacting with Synthesis) is a system for formal verification,
   synthesis, and simulation of finite state systems.
   It has been developed jointly at the University
   of California at Berkeley, the University of Colorado at Boulder, and the University of Texas, Austin.
   
   VIS is able to synthesize finite state systems and/or
   verify properties of such systems, which have been specified
   hierarchically as a collection of interacting finite state machines.
   VIS provides the following features:
   Simulation of logic circuits (proof of concept only).
   Formal "implementation" verification of combinational and sequential circuits (proof of concept only).
   State-of-the-art formal "design" verification using fair CTL model checking and language emptiness.
   Logic synthesis via hierarchy restructuring and a path to and from SIS.
   
   Each of these can be executed interactively from any point in the design hierarchy.
   A Verilog HDL front end, vl2mv, is also provided,
   which compiles a subset of Verilog into an intermediate format BLIF-MV.
3. From Goethe University in Germany: The C@S Verfication System