l0ng-ai
Featured
tty7
tty7 is a fast, GPU-accelerated terminal workbench with persistent sessions, built-in input tools, SSH support, and coding agent awareness.
AI repository intelligence
FR-AI / ANALYSISWhy it is worth attention
It provides rigorous mathematical verification for gate-level circuits, supporting complex arithmetic functions like signed multiplication, division, and dot products via a flexible specification syntax.
Who it is for
- Hardware verification engineers
- Digital circuit designers
- Formal methods researchers
- Students learning about circuit verification
Use cases
- Verifying multiplier circuits of arbitrary bit widths
- Checking correctness of adders with carry-in
- Validating multiply-accumulate (MAC) units
- Proving correctness of dot product arithmetic units
Strengths
- Leverages polynomial elimination for mathematically sound verification
- Flexible --spec syntax supports a wide range of arithmetic operations
- Open-source implementation in Rust with clear CLI usage
- Supports both signed and unsigned integer arithmetic
Considerations
- Only accepts AIGER (.aig) file format for circuit input
- Default mode assumes the circuit is a multiplier without truncation
- Specification syntax may require learning effort for complex scenarios
README quick start
Arisca
Formal Verification for Arithmetic Circuits via Symbolic Computer Algebra
Arisca is a formal verification tool designed to rigorously prove the correctness of arithmetic circuit units. It employs Symbolic Computer Algebra (SCA) and polynomial elimination techniques to mathematically verify that a gate-level circuit implementation matches its arithmetic specification.
📦 Build
Ensure you have the Rust toolchain installed.
# Clone the repository
git clone https://github.com/LittleBlackCQ/arisca.git
cd arisca
# Initialize submodules
git submodule update --init --recursive
# Build the release binary
cargo build --release
🚀 Usage
Arisca processes AIGER (.aig) files.
cargo run --release --bin arisca [OPTIONS]
Default
When no --spec is given, Arisca assumes the circuit is a multiplier: it splits the input bits into two equal-width halves (e.g. a 128-input-bit circuit becomes 64×64), interprets both as unsigned integers, and checks that the full output (no truncation) equals their product.
cargo run --release --bin arisca examples/multiplier_simple.aig
Specifying the arithmetic function with --spec
The --spec flag describes how input bits are grouped into variables and what arithmetic relationship the circuit should satisfy.
Spec syntax
| Syntax | Meaning |
|---|---|
[n] | An unsigned variable of width n bits. Offsets auto-increment. |
[n:i] | A variable of width n bits, starting at bit index i. |
o[n] / o[n:i] | Same, but for output bits (used with =). |
+ | Addition |
- | Subtraction (binary). Also works as unary negation (e.g. -[n]). |
* | Multiplication |
( ) | Grouping |
= | Equation: golden polynomial = left − right |
Input bits are consumed left-to-right as [n] variables appear in the spec. Offsets can be explicit ([n:i]) or implicit (auto-increment from 0).
Examples
127×129-bit signed multiplier with truncated 250-bit output
cargo run --release --bin arisca examples/multiplier.aig \
--spec "[127]*[129]" --signed
--signed treats the MSB of each variable as a sign bit.
256-bit adder with carry-in
cargo run --release --bin arisca examples/adder.aig \
--spec "[1]+[256]+[256]"
63×65-bit multiply-accumulate with 128-bit addend
cargo run --release --bin a
Related repositories
Similar projects matched by category, topics, and programming language.
steelbrain
Featured
reims-vgpu
reims-vgpu is an experimental virtual GPU for macOS guests that uses QEMU to decode the guest's GPU command stream and execute it through Metal or Vulkan, leveraging the built-in AppleParavirtGPU driver without requiring custom kexts.
m-novotny
Featured
memguard-rs
A Rust library that provides secure memory handling primitives including zeroization on drop, memory locking, constant-time comparison, and compile-time guarded regions, with zero dependencies and no_std support.