#model-checking #formal-verification #ic3

nightly bin+lib rIC3

rIC3: An efficient hardware model checker

7 stable releases

new 1.3.3 Jan 12, 2025
1.3.2 Jan 2, 2025
1.3.1 Dec 22, 2024

#195 in Hardware support

Download history 225/week @ 2024-12-04 201/week @ 2024-12-11 181/week @ 2024-12-18 9/week @ 2024-12-25 154/week @ 2025-01-01 116/week @ 2025-01-08

506 downloads per month

GPL-3.0 license

750KB
5.5K SLoC

rIC3 Hardware Model Checker

License: GPL v3 CI Crates.io

HWMCC

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

To view the submission for HWMCC'24, please checkout the HWMCC24 branch or download the binary release at https://github.com/gipsyh/rIC3-HWMCC24.

rIC3 Tool Flow

Image of rIC3 toolflow

Install From Crates.io

cargo install rIC3

Install From Source

Currently, some dependency libraries are linked through pre-compiled static files in the repository, and they have a dependency on the glibc version. Ubuntu 20.04 or later works fine.

  • Install the Rust compiler https://www.rust-lang.org/
  • Switch to nightly rustup default nightly
  • git clone --recurse-submodules https://github.com/gipsyh/rIC3
  • Build cd rIC3 && cargo b --release
  • Run cargo r --release -- <AIGER FILE>
  • Install cargo install --path .

Run

  • 16-threads Portfolio rIC3 <AIGER FILE>
  • single-thread IC3 rIC3 -e ic3 <AIGER FILE>

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

Without obtaining authorization, rIC3 is not allowed to be used for any commercial purposes.

Dependencies

~58–87MB
~1.5M SLoC