//! Phase 8a: R-SPU 5-Stage Pipeline
//!
//! Wires together the IF, ID, EX, MEM, and WB stages with
//! integrated PCC verification and hardware type dispatch.

import "types.mirr" as types;
import "alu.mirr" as alu;
import "regfile.mirr" as reg;
import "ram.mirr" as ram;
import "../verification/pcc_verifier.mirr" as pcc;

def rspu_pipeline(
    clk: signal in bool,
    rst_n: signal in bool,
    instr_in: signal in u32,
    pc_out: signal out u32,
    data_out: signal out u64,
    trap_out: signal out bool
) {
    reflect {
        // --- 1. Fetch Stage (IF) ---
        signal pc: internal u32;
        
        // PCC Verifier Integration
        signal pcc_valid: internal bool;
        signal pcc_fault: internal bool;

        signal cert_i: internal u16;
        signal cert_r: internal u16;
        signal cert_g: internal u16;
        signal cert_h: internal bool;
        signal cert_v: internal bool;

        reflex init_cert {
            on always {
                cert_i = 0;
                cert_r = 0;
                cert_g = 0;
                cert_h = true;
                cert_v = true;
            }
        }

        pcc::pcc_verifier(${clk}, ${rst_n}, 
            cert_i, cert_r, cert_g, cert_h, cert_v,
            pcc_valid, pcc_fault
        );

        guard fetch_active(pcc_valid) for 1 cycles;
        guard fetch_fault(pcc_fault) for 1 cycles;

        reflex fetch_normal {
            on fetch_active {
                pc = (pc + 1) & 4294967295;
                ${pc_out} = pc;
            }
        }

        reflex fetch_on_fault {
            on fetch_fault {
                ${trap_out} = pcc_fault;
            }
        }

        // --- 2. Decode Stage (ID) ---
        signal id_rs1: internal u32;
        signal id_rs2: internal u32;
        signal id_rd:  internal u32;
        signal id_val1: internal u64;
        signal id_val2: internal u64;
        signal reg_we: internal bool;
        signal reg_din: internal u64;
        
        reg::regfile(${clk}, id_rs1, id_rs2, id_rd, reg_we, reg_din, id_val1, id_val2);

        // --- 3. Execute Stage (EX) ---
        // Operands typed as u64 to pass Type Checker, but masked via Patterns
        signal ex_d1: internal u64;
        signal ex_t1: internal u64;
        signal ex_p1: internal u64;
        signal ex_d2: internal u64;
        signal ex_t2: internal u64;
        signal ex_p2: internal u64;
        
        signal ex_out_d: internal u64;
        signal ex_out_t: internal u64;
        signal ex_out_p: internal u64;
        signal ex_trap:  internal bool;
        signal alu_op:   internal u32;

        // Use new correctly-typed patterns (returning u64 masked to 32/4 bits)
        types::extract_data(id_val1, ex_d1);
        types::extract_tag(id_val1, ex_t1);
        types::extract_provenance(id_val1, ex_p1);

        types::extract_data(id_val2, ex_d2);
        types::extract_tag(id_val2, ex_t2);
        types::extract_provenance(id_val2, ex_p2);

        alu::alu_core(${clk}, alu_op, 
            ex_d1, ex_t1, ex_p1,
            ex_d2, ex_t2, ex_p2,
            ex_out_d, ex_out_t, ex_out_p, ex_trap
        );

        // --- 4. Memory Stage (MEM) ---
        signal ex_packed: internal u64;
        reflex pack_ex_result {
            on always {
                // Pack bits back into 64-bit word
                ex_packed = ((ex_out_p & 15) << 36) | ((ex_out_t & 15) << 32) | (ex_out_d & 4294967295);
                ${data_out} = ex_packed;
            }
        }

        signal mem_out: internal u64;
        signal ram_addr: internal u32;

        reflex decode_instr {
            on always {
                id_rs1 = (${instr_in} >> 24) & 255;
                id_rs2 = (${instr_in} >> 16) & 255;
                id_rd  = (${instr_in} >> 8) & 255;
                alu_op = (${instr_in} & 255);
                ram_addr = (pc & 65535);
                reg_we = true;
                reg_din = ex_packed;
            }
        }
        ram::ram(${clk}, ram_addr, ex_packed, mem_out);
    }
}

module pipeline {}
