Synchronization Verification Tool (S-VeT)
This work is supported by Semiconductor Technology Academic Research Center (STARC)
and Japan Society for the Promotion of Science (JSPS)
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.
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.
SpecC reference compiler version 2.2.0
We appreciate for any comment and/or bug reports from you. Also, if you have any question, please feel free to contact me.