Yet Another Symbolic Model Verifier (yasmv) Development

Expert guidance for working with yasmv, a symbolic model checker that performs reachability analysis and step-by-step simulation using an SMV language dialect. Includes llvm2smv, a C-to-SMV translator for formal verification of C programs.

Project Structure

yasmv is a C++ project with the following key components:

1. **Parser** (`src/parser/`) - ANTLR3-based SMV language parser

2. **Model** (`src/model/`) - Model representation with modules, variables, and constraints

3. **Compiler** (`src/compiler/`) - Compiles models to internal representation

4. **Encoding** (`src/enc/`) - Manages encoding schemes (algebraic, monolithic, TCBI/UCBI)

5. **SAT Engine** (`src/sat/`) - MiniSat-based SAT solving with CNF encoding

6. **Algorithms** (`src/algorithms/`) - Core verification algorithms:

- `check/` - Consistency checking for initial states, transition relations, and constraints

- `reach/` - Forward/backward reachability

- `sim/` - Simulation

7. **Decision Diagrams** (`src/dd/`) - CUDD 2.5.0 for BDD/ADD manipulation

8. **Commands** (`src/cmd/`) - Interactive shell commands

9. **LLVM2SMV** (`llvm2smv/`) - C-to-SMV translator using LLVM backend

Development Workflow

1. Initial Setup

When setting up the project for the first time:

1. Extract the microcode before building:

```bash

tar xfj microcode.tar.bz2

```

2. Use the setup script for recommended configuration:

```bash

./setup.sh

make -j $(nproc)

```

3. For manual configuration:

```bash

autoreconf -vif

./configure

make -j $(nproc)

```

2. Building with LLVM2SMV Support

If working with C-to-SMV translation features:

```bash

Requires LLVM development libraries and clang

./configure --enable-llvm2smv

make -j $(nproc)

```

To build without llvm2smv:

```bash

./configure --disable-llvm2smv

make -j $(nproc)

```

3. Running Tests

Always set `YASMV_HOME` environment variable when running tests:

```bash

Run all tests

make test

Quick sanity tests

make short-test

Unit tests with Boost.Test

make unit-test

Full functional tests

make functional-test

```

**Run specific unit test suite:**

```bash

YASMV_HOME=`pwd` ./yasmv_tests --run_test=tests/expressions

```

**Run individual functional test:**

```bash

YASMV_HOME=`pwd` ./yasmv --quiet examples/maze/solvable8x8.smv < examples/maze/commands > out

diff -wB examples/maze/solvable8x8.out out

```

**Test llvm2smv (if enabled):**

```bash

make -C llvm2smv test

```

4. Code Quality and Formatting

Before committing code changes:

```bash

Runs clang-format and removes tabs/trailing whitespace

./tools/cleanup.sh

```

Architecture Guidelines

Design Patterns Used

Main Entry Point

`src/main.cc` initializes the interpreter, loads microcode, and runs the interactive shell.

LLVM2SMV Components

Important Development Notes

1. **Environment Variable**: Always set `YASMV_HOME` to the project root when running tests

2. **C++ Standards**: Main project uses compiler default standard; llvm2smv uses C++20

3. **Debug Builds**: Use `-O0` by default for easier debugging

4. **Microcode Requirement**: Must be extracted before building

5. **Distributed Compilation**: Project supports distcc

Current Focus Areas

From the project TODO:

Known Issues

When to Use This Skill

Use this skill when:

Example Commands

**Build and test workflow:**

```bash

1. Extract microcode

tar xfj microcode.tar.bz2

2. Configure and build

./setup.sh

make -j $(nproc)

3. Run tests

make test

4. Format code before commit

./tools/cleanup.sh

```

**Debug specific test:**

```bash

Set environment and run with verbose output

export YASMV_HOME=`pwd`

./yasmv examples/maze/solvable8x8.smv < examples/maze/commands

```