|
|
---
|
|
|
license: mit
|
|
|
tags:
|
|
|
- formal-verification
|
|
|
- coq
|
|
|
- threshold-logic
|
|
|
- neuromorphic
|
|
|
- arithmetic
|
|
|
- adder
|
|
|
---
|
|
|
|
|
|
# tiny-RippleCarry2Bit-verified
|
|
|
|
|
|
Formally verified 2-bit ripple carry adder. Chains two full adders to add two 2-bit numbers with 100% accuracy.
|
|
|
|
|
|
## Architecture
|
|
|
|
|
|
| Component | Value |
|
|
|
|-----------|-------|
|
|
|
| Inputs | 4 (a1, a0, b1, b0) |
|
|
|
| Outputs | 3 (cout, s1, s0) |
|
|
|
| Neurons | 8 (2 full adders × 4 neurons each) |
|
|
|
| Parameters | 24 (2 full adders × 12 params each) |
|
|
|
| Layers | 2 (chained full adders) |
|
|
|
| Activation | Heaviside step |
|
|
|
|
|
|
## Key Properties
|
|
|
|
|
|
- 100% accuracy (16/16 input combinations correct)
|
|
|
- Coq-proven correctness
|
|
|
- Compositional construction from verified full adders
|
|
|
- Produces 3-bit output (sum can be 0-6, requiring 3 bits)
|
|
|
- Compatible with neuromorphic hardware
|
|
|
|
|
|
## Circuit Structure
|
|
|
|
|
|
```
|
|
|
a1 a0 b1 b0
|
|
|
| | | |
|
|
|
| +--+--+ |
|
|
|
| | |
|
|
|
| FA0 (cin=0)
|
|
|
| | |
|
|
|
| s0 c0
|
|
|
| | |
|
|
|
+--+--+-----+
|
|
|
|
|
|
|
FA1
|
|
|
|
|
|
|
s1 c1
|
|
|
```
|
|
|
|
|
|
First full adder adds least significant bits (a0 + b0 + 0), producing sum bit s0 and carry c0. Second full adder adds most significant bits with the carry (a1 + b1 + c0), producing s1 and final carry cout.
|
|
|
|
|
|
## Usage
|
|
|
|
|
|
```python
|
|
|
import torch
|
|
|
from safetensors.torch import load_file
|
|
|
|
|
|
weights = load_file('ripplecarry2bit.safetensors')
|
|
|
|
|
|
def full_adder_sim(a, b, cin):
|
|
|
sum_out = a ^ b ^ cin
|
|
|
carry_out = (a & b) | (cin & (a ^ b))
|
|
|
return sum_out, carry_out
|
|
|
|
|
|
def ripple_carry_2bit(a1, a0, b1, b0):
|
|
|
s0, c0 = full_adder_sim(a0, b0, 0)
|
|
|
s1, cout = full_adder_sim(a1, b1, c0)
|
|
|
return cout, s1, s0
|
|
|
|
|
|
# Test
|
|
|
print(ripple_carry_2bit(1, 1, 1, 0)) # 3 + 2 = 5 -> (1, 0, 1)
|
|
|
print(ripple_carry_2bit(1, 0, 1, 0)) # 2 + 2 = 4 -> (1, 0, 0)
|
|
|
print(ripple_carry_2bit(0, 1, 0, 1)) # 1 + 1 = 2 -> (0, 1, 0)
|
|
|
```
|
|
|
|
|
|
## Verification
|
|
|
|
|
|
**Coq Theorem**:
|
|
|
```coq
|
|
|
Theorem ripple_carry_2bit_correct : forall a1 a0 b1 b0,
|
|
|
ripple_carry_2bit a1 a0 b1 b0 = ripple_carry_2bit_spec a1 a0 b1 b0.
|
|
|
```
|
|
|
|
|
|
Proven axiom-free via exhaustive case analysis on all 16 input combinations.
|
|
|
|
|
|
Full proof: [coq-circuits/Arithmetic/RippleCarry2Bit.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Arithmetic/RippleCarry2Bit.v)
|
|
|
|
|
|
## Properties
|
|
|
|
|
|
- **Commutative**: Adding A + B equals B + A
|
|
|
- **Identity**: Adding 0 preserves the value
|
|
|
- **Compositional**: Built from two verified FullAdder circuits
|
|
|
|
|
|
## Citation
|
|
|
|
|
|
```bibtex
|
|
|
@software{tiny_ripplecarry2bit_verified_2025,
|
|
|
title={tiny-RippleCarry2Bit-verified: Formally Verified 2-Bit Ripple Carry Adder},
|
|
|
author={Norton, Charles},
|
|
|
url={https://huggingface.co/phanerozoic/tiny-RippleCarry2Bit-verified},
|
|
|
year={2025}
|
|
|
}
|
|
|
```
|
|
|
|
