l0ng-ai
精选
tty7
tty7 is a fast, GPU-accelerated terminal workbench with persistent sessions, built-in input tools, SSH support, and coding agent awareness.
AI 仓库情报摘要
FR-AI / ANALYSIS为什么值得关注
它通过灵活的规格语法支持多种算术运算（如乘法、除法、点积）的严格数学验证，为硬件正确性提供强保证。
适合谁使用
- 硬件验证工程师
- 数字电路设计人员
- 形式化方法研究人员
- 学习电路验证的学生
典型使用场景
- 验证任意位宽的乘法器电路
- 检查带进位输入的加法器正确性
- 验证乘累加（MAC）单元
- 证明点积算术单元的正确性
项目优势
- 采用多项式消元技术实现数学上严格的验证
- 灵活的 --spec 语法支持多种算术运算
- 开源的 Rust 实现，命令行使用清晰
- 支持有符号和无符号整数算术
使用前须知
- 仅接受 AIGER (.aig) 格式的电路文件
- 默认模式假定电路为无截断的乘法器
- 规格语法在复杂场景下需要一定的学习成本
README 快速开始
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
相关仓库与替代方案
根据分类、Topic 和编程语言匹配的相似项目。
steelbrain
精选
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
精选
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.