LSC-1 / LSC-1µ v0.1 Release Candidate
leanSilicon v0.1 Release Candidate
TL;DR
LSC-1µ is a formally-verified leanVM-b coprocessor targeting Tiny Tapeout shuttle SKY26c on SkyWater SKY130 130nm. LSC-1 is the full-featured variant for ULX3S ECP5 FPGA.
This release candidate includes:
- Three independently-certified equivalence bridges (Lean↔RTL, wrapper↔core, netlist↔RTL)
- FPGA silicon validation (SET/XOR/MUL/STATUS on ULX3S-85F)
- Reproducible GDS/OAS build with clean DRC
- Bundle artifacts: MANIFEST, SHA256SUMS, PINOUT, REPRODUCIBILITY
What is proven
| Layer | What | How | Status |
|---|---|---|---|
| GF(2^128) multiplier | Register-by-register cycle-accurate | SymbiYosys + ABC PDR (unbounded) | ✅ Proven |
| Protocol controller | Backpressure, reset, abort, DONE, opcodes | SymbiYosys + ABC PDR (unbounded) | ✅ Proven |
| Lean↔RTL refinement | One SET/XOR/MUL transaction stages & retires | Lean theorem (bounded) | ✅ Proven |
| Wrapper↔core composition | TT wrapper preserves core behavior | SymbiYosys + ABC PDR (unbounded) | ✅ Proven |
| Netlist↔RTL equivalence | Fixed v0.1 netlist vs RTL, 55 frames bounded | SymbiYosys bounded miter | ✅ Bounded (300-frame MUL/unbounded = future) |
| FPGA silicon | SET/XOR/MUL/STATUS on ULX3S-85F | UART harness vs Python oracle | ✅ All match |
What remains
- Netlist↔RTL: unbounded proof (currently bounded 55 frames)
- LSC-1 full equivalence (LSC-1µ is the verified profile)
- Physical bring-up after fabrication (requires Tiny Tapeout demoboard)
Artifacts
- Tag: v0.1 at commit 14068d4
- Bundle: release/v0.1/{MANIFEST.json, SHA256SUMS.txt, PINOUT.md, REPRODUCIBILITY.md}
- GDS/OAS: results/ (reproducible from OSS CAD Suite + SkyWater PDK)
- Bitstream: results/ulx3s-smoke-uart-20260725/ulx3s_bridge.bit