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.

Intended Use

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 file.


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: eps pdf
BV/Hybrid runtime and problem size ratios: eps pdf


32-bit Linux binary: v2ucl
64-bit Linux binary: v2ucl
Demo files: tgz

The final version of the paper can be found here: memocode2010-atlas.pdf


32-bit binary
64-bit binary


ATLAS is released under the BSD license.


For information on how to use ATLAS see the user-guide. The user-guide is also located in the doc directory of the source distribution.

Download gzipped tarball containing all examples: memocode-2010-examples.tgz (180MB, expands to 860MB)

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.