UCLID5

Understanding the repository layout:

• examples/: Example UCLID5 models (including tutorial examples in examples/tutorial).
• lib/: Dependencies (e.g., Z3).
• project/: Build scripts.
• src/main/scala/: UCLID5 source code.
• src/test/scala/: UCLID5 test suite.
• test/: Test programs for UCLID5.
• tutorial/: UCLID5 tutorial (LaTeX source).
• vim/: Vim syntax highlighting for UCLID5.

To use UCLID5 without compiling from source, download the latest release from the GitHub releases page. The executable uclid is located in the bin/ subdirectory of the downloaded package.

# Download from https://github.com/uclid-org/uclid/releases
# The binary is in the bin/ directory
./bin/uclid <your_model>.ucl

To build UCLID5 from source, you need SBT (version 1.0 or greater) in addition to the standard prerequisites (Z3 with Java bindings and OpenJDK).

Run the following command from the root directory to compile and test the project. If successful, you can create a universal package using sbt universal:packageBin.

# Compile and test
sbt update clean compile "set fork:=true" test

# Create a universal package
sbt universal:packageBin

# Install the resulting package
unzip uclid-0.9.5.zip
cd uclid-0.9.5
export PATH=$PATH:$PWD/bin

Beyond the basic tutorial, the examples/ directory contains specialized models for security, hyperproperties, and hardware verification:

• CPU Isolation: cpu_induction.ucl extends the Chapter 4 CPU model by adding an isolated mode of execution and proving non-interference between isolated and normal modes via induction.
• Security (Setuid): setuid.ucl implements an automaton based on the paper Setuid Demystified (Chen, Wagen, and Dean, Usenix Security 2002). setuid_fixed.ucl provides a corrected version of this model.
• Hyperproperties: two-safety.ucl demonstrates how to verify a 2-safety property using self-composition (based on Lee & Seshia, Chapter 17).
• Processor Verification: simple-datapath.ucl demonstrates Burch-Dill style correspondence (refinement) checking, based on original UCLID research (Bryant, Lahiri, Seshia, CAV'02).

Beyond primitives, UCLID allows for structured data types:

• Enums: Defined using enum { ID1, ID2, ... }. The default value is the first identifier in the list.
• Tuples: An ordered collection of types, e.g., {int, boolean}. Fields are internally named _1, _2, etc.
• Records: Named collections of fields with specific types, e.g., record { x: int, y: bool }.
• Maps: Functions mapping input types to an output type, e.g., int * bool -> real.
• Arrays: Collections of a specific type, e.g., [int * int] -> bool (an array of pairs mapping to a boolean).

The VCD class acts as an accumulator for signal changes. It maintains an internal map of wires and valuesAtTime.

• Wire Management: When wireChanged is called, the class checks if the wire exists. If not, it creates a new Wire object, assigns it a unique VCD ID using getIdString, and places it in the appropriate hierarchical Scope based on its dot-separated name (e.g., top.sub.signal).
• Change Tracking: It only stores changes that represent a new value (isNewValue). This prevents the output file from being bloated with redundant data.
• Hierarchical Scopes: The class supports a single top-level scope and automatically builds sub-scopes as you provide dot-separated wire names.

UCLID5 uses UclidSynonymMap and the ULContext object to manage the mapping between UCLID5 types and SMT-LIB2 types. This is critical when propagating information from SMT solvers (like counterexamples) back into the UCLID5 language.

• UclidSynonymMap: A bidirectional map between Type and SynonymType (identifiers). It allows looking up a type by its name or finding the name associated with a specific type.
• ULContext: A singleton that maintains the global context for type synonyms. It tracks:
  • origTypeMap: The original synonym map from the input .ucl file.
  • postTypeMap: The reconstructed type map from an SMT query or counterexample.

ULContext provides utility methods to validate identifiers against the current context, such as checkEnum, checkField, and checkUninterpretedField.

Every node in the UCLID5 Abstract Syntax Tree (AST) is part of a hierarchy that supports error reporting and unique identification.

• ASTNode: The base trait for all elements in the AST. Every node is automatically assigned a unique integer ID via the IdGenerator.
• PositionedNode: A trait that allows nodes to carry positional information (filename and line number).
• ASTPosition: Represents the location of a node, consisting of an optional filename and a Scala Position object. It provides errorString() for generating human-readable error messages (e.g., "at file.ucl, line 10").
• ASTNode.introducePos: A utility used during parsing to attach position information to nodes, ensuring that errors can be traced back to specific lines in the source code.

The VCD module uses three primary data structures to represent a simulation trace:

• Wire: Represents a signal. It contains the name, a unique VCD id, the width in bits, and its hierarchical path.
• Change: Represents a specific value held by a Wire. It includes logic to serialize values into VCD formats (e.g., binary b1010 for vectors or single bits for scalars).
• Scope: Represents a module or hierarchical level. It contains a collection of wires and subScopes to build the tree structure required by the VCD format.