LSC-1 / LSC-1µ v0.1.1 Final Package

v0.1.1 final-main release package

This bounded package describes final main after merged PR #45. It prepares a
new immutable version; it does not create, publish, move, overwrite, or delete
any tag or GitHub release. The existing v0.1 objects remain historical and
immutable.

v0.1 audit

• Annotated tag object b214d961f70c0693bf19a148814756126d818399
  dereferences to commit 14068d4a82803bc7e17f1219c29f4748bd257db7
  and tree e6c45d52125a7412b07428565c3243c676bea1a1.
• The published v0.1 release targets that commit, but its checked-in
  release/v0.1/MANIFEST.json and reproducibility record pin the earlier
  commit 6f45fd663792f1329036829c1670cefd78d66630 and tree
  1ffca601b105272bdbda5edb51a6c076dc4c328b.
• The preserved release/v0.1-candidate branch is
  b2f3f681fc1808a247e7f5d5de73f525dbc4c870; it is not final main.
• PR #45 retracts the unauditable ULX3S physical-run claim. This package does
  not inherit that claim.

Included boundary and receipts

MANIFEST.json pins final main's exact commit/tree, toolchains, frozen oracle,
exact-head CI, physical-flow jobs, GitHub artifact archive hashes, and selected
payload hashes. SHA256SUMS.txt covers the two canonical package documents.

The exact-main GDS run 31203929606 completed successfully. Its GDS, precheck,
gate-level test, and viewer jobs are identified in the manifest. The downloaded
artifacts record sky130A, open_pdks commit
8afc8346a57fe1ab7934ba5a6056ea8b43078e71, and LibreLane 3.0.3; their
archive and selected payload checksums were reproduced locally.

The exact-main Tiny Tapeout RTL run 31203929947 completed successfully. The
exact-main CI run 31203930126 is the authoritative executable-model,
SystemVerilog, Lean, formal/lint, mutation, and synthesis receipt for the
checked-in source and harnesses. Its formal/lsc1u_netlist_eq.sby harness
compares RTL with the historical release/v0.1 netlist (SHA-256
0c85d1afefddf1166e4b3047500f9c27a03ad7198c9c075f505c4536888c03c3), not
the selected exact-main physical-run netlist (SHA-256
97000459a97f1d775db06ed88fefb59e28fde09b27a5046aaadd036ad01e16bc).
The manifest records this boundary explicitly; no formal-equivalence claim is
made for the selected physical payload.

Explicit limitations

• These results apply to the reduced LSC-1u Tiny Tapeout profile where stated,
  not to full LSC-1 end-to-end behavior.
• Formal results retain each harness's assumptions and bounds. The historical
  v0.1 netlist comparison is bounded, not unbounded sequential equivalence, and
  does not cover the selected v0.1.1 physical payload.
• There is no completed Lean-to-RTL correspondence proof for the full design.
• GDS/precheck, gate-level simulation, and rendering are physical-design-flow
  evidence; they do not prove timing, power, analog behavior, manufacturability,
  shuttle acceptance, or correct fabricated silicon.
• No ULX3S board run is claimed. No FPGA hardware or fabricated ASIC was
  attached or physically validated for this package.
• GitHub artifact archives are service-produced ZIPs; payload hashes identify
  the release bytes independently of ZIP container metadata.
• The package contains receipts and hashes, not duplicated large binary
  artifacts. Reproduction requires downloading the retained artifacts from the
  pinned run.
• No tag, GitHub release, submission, publication, merge, or branch deletion is
  part of this preparation PR.

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