Version: 0.1 (beta)
c2ucl is a tool that abstracts C++ code into a high-level model in the
UCLID modeling language.
It currently supports a subset of C++ that
has been found useful in the verification of low-level software, such
as CPU emulators and hypervisors.
The abstraction enables formal
verification of the software using the UCLID verification system.
The intended use of c2ucl is to enable the use of the UCLID toolkit
for verifying properties of C or C++ code.
It is released under a "modified" BSD license permitting any kind of use including for
commercial, research, or educational purposes.
Please see the LICENSE
Please download the tarball for 64-bit binaries (Linux and MacOS), some examples, and a README.
The README contains instructions on both installing and using c2ucl.
This page illustrates how to use v2ucl, the tool for abstracting
Verilog to UCLID, described in the paper
available below. To see the demo, first download the demo and the
appropriate version of v2ucl below. For your convenience, there is a
link to a copy of the paper and graphs which compare our novel
hybrid BV/Term-Level models against pure BV models.
BV/Hybrid runtimes for varying flits/packet:
BV/Hybrid runtime and problem size ratios:
32-bit Linux binary: v2ucl
64-bit Linux binary: v2ucl
Demo files: tgz
The final version of the paper can be found here:
ATLAS is released under the
For information on how to use ATLAS see the
The user-guide is also located in the doc directory of the source distribution.
Download gzipped tarball containing all
Note about USB example: There are two CRC modules present, a 16-bit and 5-bit version. Both
modules pass random simulation testing, however, only the 16-bit CRC module is abstracted. The
5-bit CRC module is only present in the original USB design, not the refined
design. Therefore, abstracting the 5-bit CRC module will not benefit performance because it
isn't in the cone-of-influence of the property being checked.