Deterministic Compute
Built From First Principles
A formally specified processor architecture
for predictable execution, matrix acceleration,
and verification-first hardware.
Full five-stage scalar pipeline with register file, instruction queue, and cycle-accurate waveform display. Watch forwarding resolve hazards in real time.
Every architectural state transition is explainable. Same input, same output, same cycle count. H=0.0 nats entropy — proven in Lean 4.
Formal methods integrated into development. 12 theorems proven in Lean 4. Zero sorry. Zero Mathlib. Kernel axioms only.
RTL designed for FPGA and ASIC implementation. No vendor lock-in. No proprietary IP blocks. Synthesizable from source.
Click any instruction to view its encoding, latency, pipeline behavior, and formal specification.
Hover over each stage to explore its internal structure and responsibilities.
Every claim about ORTHO32 behavior is backed by machine-checked proof. Verification is architecture, not afterthought.
Details intentionally withheld while intellectual property protection is in progress.
From FPGA prototyping to ASIC tape-out. No fake specs, no invented clock speeds — only real milestones.
Xilinx Artix-7 and Kintex-7 synthesis targets. Primary development and validation platform.
Target families: Artix-7 (XC7A100T+), Kintex-7 (XC7K160T+)
Toolchain: Vivado synthesis + place-and-route
Validation: Cycle-accurate RTL simulation match
28nm and 14nm process node exploration. Post-FPGA validation milestone.
Target nodes: 28nm (initial), 14nm (future)
Design flow: logic synthesis → floorplanning → timing closure
Tape-out: pending FPGA validation + funding
Host-attached deterministic compute card. Standard PCIe form factor.
Interface: PCIe Gen3 x8 minimum
Host communication: DMA + MMIO control registers
Use case: Deterministic AI inference, cryptographic workloads
Compact FPGA module for embedded deterministic compute.
Form factor: M.2 2280 or 22110
Power budget: 10-25W TDP
Use case: Edge AI, real-time control systems
Complete FPGA board, toolchain, and documentation for researchers and engineers.
Includes: FPGA board, USB-JTAG programmer, power supply
Software: Full RTL source, synthesis scripts, example programs
Documentation: ISA manual, pipeline guide, verification workflow
Pipeline design, timing guarantees, microarchitecture
Instruction encodings, register conventions, ABI
SystemVerilog implementation, module hierarchy
Proof tactics, theorem statements, axiom audit
Pipeline, ISA, RTL, timing proofs
Verilator testbenches, waveform traces
Public interface, disclosed properties
Entropy proof, mathematical foundations
Assembly language, calling conventions
Sample programs, benchmarks, tests
We don't publish TOPS, TFLOPS, or benchmark rankings. Here's what we prove instead.
We don't publish TOPS because peak throughput isn't the goal. Predictable latency is. We don't race benchmarks because determinism isn't measured in FLOPS. When your AI inference must complete in exactly 768 cycles — not "approximately" 768, not "usually" 768, but mathematically guaranteed 768 — that's when ORTHO32 matters.