Feature/rv32

.github/workflows/build.yml

@@ -7,6 +7,10 @@ on:
     branches: [ main, master ]
   workflow_dispatch:
 
+permissions:
+  deployments: write
+  contents: write
+
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -98,11 +102,96 @@ jobs:
     - name: Run Compiler improvement tests (complement, lambda, hw_let)
       run: lake env lean Tests/CompilerTests.lean
 
+    # ---- Oracle Accuracy Tests ----
+
+    - name: Run oracle accuracy tests (halt loop detection, timer skip, MIE/MTIE guard)
+      run: lake exe oracle-accuracy-test
+
     # ---- SVParser Tests ----
 
-    - name: "Run SVParser tests (11 tests: parse, lower, JIT, PicoRV32, C firmware)"
+    - name: "Run SVParser tests (34 tests: parse, lower, JIT, pcpi_mul, byte-lane, replication)"
       run: lake exe svparser-test
 
+    # ---- RV32 JIT vs Verilator Benchmark ----
+    # Signal DSL RV32 SoC (122 registers, 4-stage pipeline)
+    # Runs 10M cycles with both backends, compares cyc/s
+
+    - name: Install Verilator
+      run: sudo apt-get install -y verilator
+
+    - name: Build Verilator simulation
+      run: cd verilator && make build
+
+    - name: "Build JIT shared library (.so)"
+      run: |
+        cd verilator
+        g++ -O2 -std=c++17 -shared -fPIC -o generated_soc_jit.so generated_soc_jit.cpp
+
+    - name: "Build benchmark binaries"
+      run: |
+        cd verilator
+        # JIT bench
+        g++ -O2 -std=c++17 -o jit_bench tb_jit_bench.cpp -ldl
+        # Verilator bench — link model objects but exclude tb_soc.o (has its own main)
+        VERILATOR_ROOT=$(verilator --getenv VERILATOR_ROOT)
+        g++ -O2 -std=c++17 -o verilator_bench tb_verilator_bench.cpp \
+            $(ls obj_dir/*.o | grep -v tb_soc) \
+            -Iobj_dir -I${VERILATOR_ROOT}/include -I${VERILATOR_ROOT}/include/vltstd \
+            -lpthread
+
+    - name: "Run RV32 benchmark (10M cycles, Verilator vs JIT)"
+      run: |
+        cd verilator
+        CYCLES=10000000
+
+        echo "=== Verilator Benchmark ==="
+        ./verilator_bench ../firmware/firmware.hex $CYCLES 2>&1 | tee verilator_output.txt
+
+        echo ""
+        echo "=== JIT Benchmark ==="
+        ./jit_bench ../firmware/firmware.hex $CYCLES ./generated_soc_jit.so 2>&1 | tee jit_output.txt
+
+    - name: Parse benchmark results
+      run: |
+        cd verilator
+        # Extract cycles/sec from Verilator output
+        VERILATOR_CPS=$(grep -oE '[0-9]+ cycles/sec' verilator_output.txt | head -1 | awk '{print $1}')
+        # Extract cycles/sec from JIT output (Benchmark 1: pure eval+tick)
+        JIT_PURE_CPS=$(grep 'cycles/sec' jit_output.txt | head -1 | grep -oE '[0-9]+ cycles/sec' | awk '{print $1}')
+        # Benchmark 4: evalTick (fused)
+        JIT_FUSED_CPS=$(grep 'cycles/sec' jit_output.txt | grep -A0 'evalTick' | grep -oE '[0-9]+ cycles/sec' | head -1 | awk '{print $1}')
+        # Benchmark 5: evalTick + 6 wires
+        JIT_6WIRE_CPS=$(grep 'cycles/sec' jit_output.txt | tail -1 | grep -oE '[0-9]+ cycles/sec' | awk '{print $1}')
+
+        echo "Verilator:        ${VERILATOR_CPS:-0} cyc/s"
+        echo "JIT eval+tick:    ${JIT_PURE_CPS:-0} cyc/s"
+        echo "JIT evalTick:     ${JIT_FUSED_CPS:-0} cyc/s"
+        echo "JIT evalTick+6w:  ${JIT_6WIRE_CPS:-0} cyc/s"
+
+        cat <<EOF > ../rv32-bench-results.json
+        [
+          { "name": "Verilator (10M cycles)", "unit": "cycles/sec", "value": ${VERILATOR_CPS:-0} },
+          { "name": "JIT eval+tick (10M cycles)", "unit": "cycles/sec", "value": ${JIT_PURE_CPS:-0} },
+          { "name": "JIT evalTick fused (10M cycles)", "unit": "cycles/sec", "value": ${JIT_FUSED_CPS:-0} },
+          { "name": "JIT evalTick+6wires (10M cycles)", "unit": "cycles/sec", "value": ${JIT_6WIRE_CPS:-0} }
+        ]
+        EOF
+        cat ../rv32-bench-results.json
+
+    - name: Store RV32 benchmark result
+      uses: benchmark-action/github-action-benchmark@v1
+      if: github.event_name == 'push'
+      with:
+        name: RV32 SoC Simulation Benchmark (Verilator vs JIT)
+        tool: customBiggerIsBetter
+        output-file-path: rv32-bench-results.json
+        benchmark-data-dir-path: dev/rv32-bench
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        auto-push: true
+        alert-threshold: "80%"
+        comment-on-alert: true
+        fail-on-alert: false
+
     # ---- Unit Tests ----
 
     - name: Run full test suite (481 tests)

.gitignore

@@ -45,3 +45,4 @@ Thumbs.db
 plans/
 Sparkle/Verification/Generated/
 Examples/CDC/gen/
+verilator/generated_soc_jit.cpp

README.md

@@ -26,8 +26,9 @@ Sparkle ships with production-grade IP cores — each with pure Lean specs, form
 |----|-------------|:------:|:-----:|---------|
 | **[BitNet b1.58](docs/BitNet.md)** | Formally verified LLM inference accelerator. Ternary weights, Q16.16 datapath, dual architecture (1-cycle vs 12-cycle) | 60+ theorems | Full | 202K / 99K cells |
 | **[YOLOv8n-WorldV2](docs/YOLOv8.md)** | Open-vocabulary object detection. INT4/INT8 quantized, 15 modules, CLIP text embeddings | Golden validation | Full | Backbone + Neck + Head |
-| **[RV32IMA SoC](docs/RV32.md)** | RISC-V CPU — boots Linux 6.6.0. 4-stage pipeline, Sv32 MMU, UART, CLINT. JIT at 13M cyc/s (1.17x Verilator) | ISA proofs | Full | 122 registers |
-| **[SV→Sparkle Transpiler](docs/RV32.md#sv-transpiler)** | Parse Verilog → JIT + formal verification. `verilog!` macro, `assert` auto-proof via `bv_decide`, type-safe JIT wrappers. C firmware: Fib, Sort, GCD | 6+ theorems | JIT | 11 parser tests |
+| **[RV32IMA SoC](docs/RV32.md)** | RISC-V CPU — boots Linux 6.6.0. 4-stage pipeline, Sv32 MMU, UART, CLINT. JIT at 13M cyc/s (1.17x Verilator). 102 formal proofs including Signal DSL ↔ spec equivalence | 102 theorems | Full | 122 registers |
+| **[AXI4-Lite Bus](docs/RV32.md)** | Verified AXI4-Lite slave/master. Protocol compliance (valid persistence, deadlock-free), synthesizable | 14 theorems | Full | 23 sim tests |
+| **[SV→Sparkle Transpiler](docs/RV32.md#sv-transpiler)** | Parse Verilog → JIT + formal verification. `verilog!` macro, `assert` auto-proof via `bv_decide`. PicoRV32 M-ext (MUL/DIV/REM) operational. 34 CI-safe tests | 6+ theorems | JIT | 34 tests |
 | **[H.264 Codec](docs/H264.md)** | Baseline Profile encoder + decoder. Hardware MP4 muxer produces playable files. 14 modules | 15+ theorems | Full | 709-byte MP4 output |
 | **[CDC Infrastructure](docs/CDC.md)** | Lock-free multi-clock simulation. SPSC queue (210M ops/sec), rollback mechanism, JIT.runCDC | 12 theorems | C++ | 2-thread Time-Warping |
 
@@ -799,10 +800,12 @@ Contributions welcome! Areas of interest:
 - [x] ~~**Type-Safe JIT Wrappers**~~ - Done (Phase 45): `SimInput`/`SimOutput`/`Simulator` generated by `verilog!` macro
 - [x] ~~**Signal Operator Refactoring**~~ - Done (Phase 46): Mixed Signal/BitVec operators (`a + 1#8`, `1#64 <<< b`), compiler fix for inline expansion
 - [x] ~~**Imperative `<~` Assignment**~~ - Done (Phase 47): `Signal.circuit` macro with `<~` register assignment, unified `Signal.loop` memoization
-- [ ] **Linux Boot Idle-Loop Skipping** - Extend dynamic oracle to detect WFI/idle loops during Linux boot
+- [x] ~~**AXI4-Lite Bus Protocol**~~ - Done (Phase 48): Verified slave/master, 14 proofs, 23 sim tests, synthesizable
+- [x] ~~**RV32I Formal Verification**~~ - Done (Phase 49): 102 theorems, **MSTATUS WPRI bug found**, Signal DSL ↔ spec equivalence
+- [x] ~~**Linux Boot Idle-Loop Skipping**~~ - Done (Phase 50): MIE/MTIE interrupt guard, WFI fast-path, 4 CI oracle accuracy tests
 - [ ] **Verified Standard IP — Parameterized FIFO** - Generic depth/width FIFO with power-of-2 depth
 - [ ] **Verified Standard IP — N-way Arbiter** - Generalize 2-client round-robin arbiter to N clients
-- [ ] **Verified Standard IP — AXI4-Lite / TileLink** - Bus protocol interfaces with formal properties
+- [ ] **Verified Standard IP — TileLink / AXI4 Interconnect** - Full AXI4 (bursts, IDs) and TileLink
 - [ ] **GPGPU / Vector Core** - Apply the Verification-Driven Design (VDD) framework to highly concurrent, memory-bound accelerator architectures
 - [ ] **FPGA Tape-out Flow** - End-to-end examples deploying Sparkle-generated Linux SoCs to physical FPGAs
 

Sparkle/Backend/CppSim.lean

@@ -413,13 +413,16 @@ def emitModule (m : Module) (design : Option Design := none)
       | none => internalWires.filter fun (w : Port) =>
           let sn := sanitizeName w.name
           sn.startsWith "_gen_" || tickRefs.contains sn
+    -- Collect memory names to avoid declaring them as local scalars
+    let memoryNames := m.body.filterMap fun s => match s with
+      | .memory name _ _ _ _ _ _ _ _ _ => some (sanitizeName name) | _ => none
     let localWires := match observableWires with
       | some ws => internalWires.filter fun (w : Port) =>
           let sn := sanitizeName w.name
-          !ws.contains sn && !tickRefs.contains sn
+          !ws.contains sn && !tickRefs.contains sn && !memoryNames.contains sn
       | none => internalWires.filter fun (w : Port) =>
           let sn := sanitizeName w.name
-          !sn.startsWith "_gen_" && !tickRefs.contains sn
+          !sn.startsWith "_gen_" && !tickRefs.contains sn && !memoryNames.contains sn
 
     let wireDecls := memberWires.map fun (p : Port) =>
       s!"    {emitCppType p.ty} {sanitizeName p.name};"

Sparkle/Core/Oracle.lean

@@ -48,6 +48,17 @@ structure SelfLoopConfig where
   skipToTimerCompare : Bool := false
   /-- Maximum cycles to skip per trigger (caps skipToTimerCompare distance) -/
   maxSkip : Nat := 10_000_000
+  /-- Guard: check MIE (global interrupt enable) and MTIE (timer interrupt enable)
+      before performing timer-compare skip. Prevents skipping when interrupts
+      are disabled (the timer interrupt wouldn't fire anyway). -/
+  checkInterruptEnable : Bool := false
+  /-- Register index for MSTATUS CSR (contains MIE at bit 3) -/
+  mstatusRegIdx : UInt32 := 58
+  /-- Register index for MIE CSR (contains MTIE at bit 7) -/
+  mieRegIdx : UInt32 := 59
+  /-- WFI fast-path: when set, the oracle checks if the instruction at this
+      wire index is WFI (0x10500073) and triggers immediately (threshold=1). -/
+  wfiWireArrayIdx : Option Nat := none
 
 /-- Mutable state for the self-loop detector -/
 structure SelfLoopState where
@@ -75,14 +86,34 @@ def mkSelfLoopOracle (config : SelfLoopConfig)
     let pc := vals[config.pcWireArrayIdx]?.getD 0
     let st ← stateRef.get
 
+    -- WFI fast-path: if WFI wire is provided and active, trigger immediately
+    let isWFI := match config.wfiWireArrayIdx with
+      | some idx => (vals[idx]?.getD 0) != 0
+      | none => false
+
     -- Check if PC is within tolerance of anchor (handles multi-instruction loops)
     let pcDiff := if pc >= st.anchorPC then pc - st.anchorPC else st.anchorPC - pc
     let isNearAnchor := pcDiff <= config.pcTolerance
 
-    if isNearAnchor then
+    -- WFI overrides the threshold: trigger after just 1 cycle of WFI
+    let effectiveThreshold := if isWFI then 1 else config.threshold
+
+    if isNearAnchor || isWFI then
       let newCount := st.sameCount + 1
-      if newCount >= config.threshold then
-        -- Self-loop detected — skip forward
+      if newCount >= effectiveThreshold then
+        -- Self-loop detected — attempt skip
+
+        -- Guard: check interrupt enable before timer-compare skip
+        if config.checkInterruptEnable then do
+          let mstatus ← JIT.getReg handle config.mstatusRegIdx
+          let mieReg ← JIT.getReg handle config.mieRegIdx
+          let globalIE := (mstatus.toNat >>> 3) &&& 1    -- MSTATUS.MIE (bit 3)
+          let timerIE := (mieReg.toNat >>> 7) &&& 1      -- MIE.MTIE (bit 7)
+          if globalIE == 0 || timerIE == 0 then
+            -- Interrupts disabled — timer skip would be futile
+            stateRef.set { st with sameCount := newCount }
+            return none
+
         -- Read current CLINT timer values
         let oldLo ← JIT.getReg handle config.mtimeLoRegIdx
         let oldHi ← JIT.getReg handle config.mtimeHiRegIdx
@@ -131,6 +162,7 @@ def mkSelfLoopOracle (config : SelfLoopConfig)
 
 /-- Create a boot-optimized oracle for Linux boot idle-loop skipping.
     Uses timer-compare-aware skipping with wider PC tolerance (32 bytes).
+    Enables MIE/MTIE guard to avoid skipping when interrupts are disabled.
     Resets sameCount after each trigger so the timer interrupt can fire. -/
 def mkBootOracle (config : SelfLoopConfig := {})
     : IO ((JITHandle → Nat → Array UInt64 → IO (Option Nat)) × IO.Ref SelfLoopState) :=
@@ -145,6 +177,10 @@ def mkBootOracle (config : SelfLoopConfig := {})
     mtimecmpHiRegIdx := config.mtimecmpHiRegIdx
     skipToTimerCompare := true
     maxSkip := config.maxSkip
+    checkInterruptEnable := true
+    mstatusRegIdx := config.mstatusRegIdx
+    mieRegIdx := config.mieRegIdx
+    wfiWireArrayIdx := config.wfiWireArrayIdx
   }
 
 end Sparkle.Core.Oracle