Formally Specified Digital Logic for Pervasively Reconfigurable Computing
summary
Formal spec of a proposed reversible asynchronous universal cell is given in TLA+ with a translated, verified simulation in miniKanren translation, and the implementation model and simulator live on GitHub. Claims: single primitive supports reversible parity‑conserving logic, pool‑based async handshakes, three phases (wire/stem/processor), and Turing‑completeness via reduction from RL‑EMs. The abstract machine expands to about 25 states for stem handling. The work reports a working simulation and mechanized checks rather than just high‑level examples.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 4:56Reversible Logic
- 9:14Permutation
- 12:24Universal Cell
- 16:44Universal Tools
- 20:54Universal Memory
- 31:30Formal Model
- 37:12Abstract State Machines
- 46:19Universal Computation
related talks
24mA Big-Step Compositional Continuation-Passing Semantics for WebAssembly
29mVerification of WebAssembly Features
46mProgramming Systems for Analog Hardware
01h 06mAs low-level as possible, but no lower
28mCombinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
26mAn MLIR Dialect for WebAssembly
05mLighting talks and closing discussion
35mVeracruz: Privacy-preserving mutliparty computation using trusted hardware