|
|
---
|
|
|
license: mit
|
|
|
tags:
|
|
|
- formal-verification
|
|
|
- coq
|
|
|
- threshold-logic
|
|
|
- neuromorphic
|
|
|
- arithmetic
|
|
|
- adder
|
|
|
---
|
|
|
|
|
|
# tiny-FullAdder-verified
|
|
|
|
|
|
Formally verified full adder circuit. Adds three 1-bit inputs (a, b, carry_in), producing sum and carry_out outputs with 100% accuracy.
|
|
|
|
|
|
## Architecture
|
|
|
|
|
|
| Component | Value |
|
|
|
|-----------|-------|
|
|
|
| Inputs | 3 (a, b, carry_in) |
|
|
|
| Outputs | 2 (sum, carry_out) |
|
|
|
| Neurons | 9 (2 HalfAdders + OR) |
|
|
|
| Parameters | 27 |
|
|
|
| Depth | 3 layers |
|
|
|
| Activation | Heaviside step |
|
|
|
|
|
|
## Key Properties
|
|
|
|
|
|
- 100% accuracy (8/8 input combinations correct)
|
|
|
- Coq-proven correctness
|
|
|
- Compositional design: 2 HalfAdders + OR gate
|
|
|
- Building block for ripple-carry adders
|
|
|
- Compatible with neuromorphic hardware
|
|
|
|
|
|
## Circuit Design
|
|
|
|
|
|
Composed from two half adders and an OR gate:
|
|
|
|
|
|
```
|
|
|
HalfAdder1: (a, b) -> (s1, c1)
|
|
|
HalfAdder2: (s1, carry_in) -> (sum, c2)
|
|
|
carry_out = OR(c1, c2)
|
|
|
```
|
|
|
|
|
|
**Components:**
|
|
|
- 2 HalfAdders: 4 neurons each (XOR + AND)
|
|
|
- 1 OR gate: 1 neuron
|
|
|
- Total: 9 neurons, 27 parameters, depth 3
|
|
|
|
|
|
## Usage
|
|
|
|
|
|
```python
|
|
|
import torch
|
|
|
from safetensors.torch import load_file
|
|
|
|
|
|
weights = load_file('fulladder.safetensors')
|
|
|
|
|
|
def heaviside(x):
|
|
|
return int(x >= 0)
|
|
|
|
|
|
def full_adder(a, b, carry_in):
|
|
|
# HalfAdder1: (a, b) -> (s1, c1)
|
|
|
inputs_ha1 = torch.tensor([float(a), float(b)])
|
|
|
|
|
|
or_out1 = heaviside((inputs_ha1 * weights['ha1.sum.layer1.or.weight']).sum() +
|
|
|
weights['ha1.sum.layer1.or.bias'])
|
|
|
nand_out1 = heaviside((inputs_ha1 * weights['ha1.sum.layer1.nand.weight']).sum() +
|
|
|
weights['ha1.sum.layer1.nand.bias'])
|
|
|
layer1_outs1 = torch.tensor([float(or_out1), float(nand_out1)])
|
|
|
s1 = heaviside((layer1_outs1 * weights['ha1.sum.layer2.weight']).sum() +
|
|
|
weights['ha1.sum.layer2.bias'])
|
|
|
c1 = heaviside((inputs_ha1 * weights['ha1.carry.weight']).sum() +
|
|
|
weights['ha1.carry.bias'])
|
|
|
|
|
|
# HalfAdder2: (s1, carry_in) -> (sum, c2)
|
|
|
inputs_ha2 = torch.tensor([float(s1), float(carry_in)])
|
|
|
|
|
|
or_out2 = heaviside((inputs_ha2 * weights['ha2.sum.layer1.or.weight']).sum() +
|
|
|
weights['ha2.sum.layer1.or.bias'])
|
|
|
nand_out2 = heaviside((inputs_ha2 * weights['ha2.sum.layer1.nand.weight']).sum() +
|
|
|
weights['ha2.sum.layer1.nand.bias'])
|
|
|
layer1_outs2 = torch.tensor([float(or_out2), float(nand_out2)])
|
|
|
sum_out = heaviside((layer1_outs2 * weights['ha2.sum.layer2.weight']).sum() +
|
|
|
weights['ha2.sum.layer2.bias'])
|
|
|
c2 = heaviside((inputs_ha2 * weights['ha2.carry.weight']).sum() +
|
|
|
weights['ha2.carry.bias'])
|
|
|
|
|
|
# Carry out: OR(c1, c2)
|
|
|
carry_inputs = torch.tensor([float(c1), float(c2)])
|
|
|
carry_out = heaviside((carry_inputs * weights['carry_or.weight']).sum() +
|
|
|
weights['carry_or.bias'])
|
|
|
|
|
|
return sum_out, carry_out
|
|
|
|
|
|
# Test
|
|
|
print(full_adder(0, 0, 0)) # (0, 0)
|
|
|
print(full_adder(1, 1, 0)) # (0, 1) - 1+1=2, sum=0, carry=1
|
|
|
print(full_adder(1, 1, 1)) # (1, 1) - 1+1+1=3, sum=1, carry=1
|
|
|
```
|
|
|
|
|
|
## Truth Table
|
|
|
|
|
|
| a | b | cin | sum | cout |
|
|
|
|---|---|-----|-----|------|
|
|
|
| 0 | 0 | 0 | 0 | 0 |
|
|
|
| 0 | 0 | 1 | 1 | 0 |
|
|
|
| 0 | 1 | 0 | 1 | 0 |
|
|
|
| 0 | 1 | 1 | 0 | 1 |
|
|
|
| 1 | 0 | 0 | 1 | 0 |
|
|
|
| 1 | 0 | 1 | 0 | 1 |
|
|
|
| 1 | 1 | 0 | 0 | 1 |
|
|
|
| 1 | 1 | 1 | 1 | 1 |
|
|
|
|
|
|
## Verification
|
|
|
|
|
|
**Coq Theorem**:
|
|
|
```coq
|
|
|
Theorem full_adder_correct : forall a b c,
|
|
|
full_adder a b c = full_adder_spec a b c.
|
|
|
```
|
|
|
|
|
|
Where `full_adder_spec` computes:
|
|
|
- `sum = a XOR b XOR c`
|
|
|
- `carry_out = (a AND b) OR (c AND (a XOR b))`
|
|
|
|
|
|
Proven axiom-free with verified properties:
|
|
|
- Commutativity in first two arguments
|
|
|
- Equivalence to half adder when carry_in = false
|
|
|
- Exhaustive correctness on all 8 input combinations
|
|
|
|
|
|
Full proof: [coq-circuits/Arithmetic/FullAdder.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Arithmetic/FullAdder.v)
|
|
|
|
|
|
## Applications
|
|
|
|
|
|
- Building block for multi-bit ripple-carry adders
|
|
|
- Component of ALU designs
|
|
|
- Foundational for all integer arithmetic circuits
|
|
|
- Educational hardware design
|
|
|
|
|
|
## Citation
|
|
|
|
|
|
```bibtex
|
|
|
@software{tiny_fulladder_verified_2025,
|
|
|
title={tiny-FullAdder-verified: Formally Verified Full Adder},
|
|
|
author={Norton, Charles},
|
|
|
url={https://huggingface.co/phanerozoic/tiny-FullAdder-verified},
|
|
|
year={2025}
|
|
|
}
|
|
|
```
|
|
|
|
