Home | Publications | CV | Software | Links

Synchronization Verification Tool (S-VeT)

 

Release

    January 11, 2007      S-VeT version 0.1 is available for download


Download

    Version Binary Manual
    0.1 S-VeT_bin.tar.gzManual-0.1


Acknowledgement

    This work is supported by Semiconductor Technology Academic Research Center (STARC) and Japan Society for the Promotion of Science (JSPS)


Introduction

    S-VeT is a tool that used to verify synchronization in SpecC descriptions. Implementation of S-VeT is similar to other well-known C verifiers like SLAM, BLAST, and MAGIC. However, in order to cope with non-deterministic behavior of statement execution in SpecC, execution of every statement is described with equality/inequality formulae and solved by using commercial ILP solver.


Installation

    S-VeT has been successfully installed on Fedora Core 3, 4 and GCC 3.0-3.4. In order to run S-VeT smoothly, you will need to install the following tools.
    1. SpecC reference compiler version 2.2.0
    2. NuSMV
    3. CVC Lite
    4. ILOG Cplex


Contact

    We appreciate for any comment and/or bug reports from you. Also, if you have any question, please feel free to contact me.