File size: 4,495 Bytes
e20f4bc |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 |
---
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}
}
```
|