rIC3 Hardware Model Checker

LLM-Assisted Model Checking

rIC3 supports LLM-accelerated model checking through invariant generation. For details, see the paper CIll: CTI-Guided Invariant Generation via LLMs for Model Checking. The prompt and VCD inspection MCP tools are located under the tools directory. For a concrete example, see https://github.com/gipsyh/cill-exp

HWMCC

rIC3 achieved first place in both the bit-level track and the word-level bit-vector track at the 2024 and 2025 Hardware Model Checking Competition (HWMCC).

rIC3 Tool Flow

Install From Crates.io

cargo install rIC3

Install From Source

rIC3 can be compiled on both Linux and macOS.

• Install the Rust compiler
• Clone the repository: git clone --recurse-submodules https://github.com/gipsyh/rIC3
• Install Bitwuzla from https://github.com/bitwuzla/bitwuzla (required by wlbmc)
• Install Yosys from https://github.com/YosysHQ/yosys and Yosys-Slang from https://github.com/gipsyh/yosys-slang/tree/ric3 (required by the project-based flow and CIll)
• Build cd rIC3 && cargo b --release
• Run cargo r --release -- check <AIGER/BTOR> portfolio
• Install cargo install --path .

Usage

• Project-based RTL flow: if your design directory contains a ric3.toml, run verification directly from that directory with ric3 run.

  [dut]
  # Top-level module name
  top = "counter"
  # RTL source files used to build the DUT
  files = ["counter.sv"]
  # Reset signal name; prefix with "!" for an active-low reset
  reset = "!rst_n"
  

  For complete runnable examples, see examples/.

• Direct AIG/BTOR checking:

  • 16-threads Portfolio ric3 check <AIGER/BTOR> portfolio
  • single-thread IC3 ric3 check <AIGER/BTOR> ic3

Docker

• build image: docker build -t ric3 .
• run: docker run -v <AIGER/BTOR>:/model.<aig/btor> ric3 check model.<aig/btor> portfolio

Publications

• [CAV2025] The rIC3 Hardware Model Checker
• [CAV2025] Deeply Optimizing the SAT Solver for the IC3 Algorithm
• [DAC2024] Predicting Lemmas in Generalization of IC3
• [arXiv] Extended CTG Generalization and Dynamic Adjustment of Generalization Strategies in IC3
• [arXiv] CIll: CTI-Guided Invariant Generation via LLMs for Model Checking

Copyright (C) 2023 - Present, Yuheng Su (gipsyh.icu@gmail.com). All rights reserved.