Downloads
From UclidWiki
Download UCLID
The current release is UCLID version 3.0 (beta). The main new feature in v3.0 is the support for finite-precision bit-vector arithmetic.
We currently have a bytecode distribution, containing documentation, examples, and bytecode. Currently version 3.0 is only available for Linux on x86 architectures (both 32 and 64 bit). Installation instructions are in the README file. Version 3.0 uses Ofer Strichman's psep library (but you do not need to separately download and install it).
UCLID is largely implemented in Moscow ML. To use UCLID, you will also need to download and install the following support software before installing UCLID:
- Moscow ML, version 2.00 or higher
- Perl version 5.0 or higher
- One or more SAT solvers supported by UCLID (e.g., Minisat) -- see the README file.
Download the user manual in PDF.
UCLID is released under the BSD license. See the "LICENSE" file included in the distribution.
If you download and use UCLID, please let us know by e-mailing Bryan Brady or Sanjit Seshia (for e-mail addresses, see here).
Example UCLID models
Here are some examples of purely term-level UCLID specifications that are mentioned in our CAV'02 and FMCAD'02 papers:
- Out-of-order Execution Unit
- DLX Pipelined Processor
- Steven German's cache coherence protocol: Buggy version 1 and Buggy version 2
For other examples, including bit-vector examples, look in the tarfile.
Benchmarks formulas generated from UCLID
Here are tarred-gzipped files containing some benchmark formulas in different formats (as given below):
- A set of Valid CLU logic formulas in Stanford Validity Checker (SVC) format tgz (480 kB)
- A set of Unsatisfiable Boolean formulas in DIMACS Conjunctive Normal Form (CNF) format tgz (7.1MB)
- A set of benchmarks for Pseudo-Boolean Constraint Solvers. All input formulas are unsatisfiable. A README file in the tarball describes the format. tgz (19MB)
The benchmarks above are somewhat dated. A newer set of benchmarks will be posted soon.
