Janus

 Janus🔗

Janus is a proof-first processor contract for deterministic standard-cell compute-in-memory. It is named for the two faces of the machine: a small control processor for general sequencing, and a branch-free kernel face for the resident weight path that must run at full rate.

The book is the source of truth. The definitions below are executable, the theorems are checked when the repository builds, and the generated RTL is tied to a documented boundary. There is no Janus silicon yet; the first RTL artifact is a simulator and synthesis target whose execute path is proved against the ISA model. Full reset/load/trace and parser-level SystemVerilog refinement are future work.

Contents

  1. 1. Status and Evidence
  2. 2. The Processor Contract
  3. 3. RTL Contract
  4. 4. RTL as a Lean DSL
  5. 5. Instruction Encoding
  6. 6. Fetch Refinement
  7. 7. Cell Lifecycle
  8. 8. Kernel Execution
  9. 9. Block-Float Arithmetic
  10. 10. Load and Utilization Models