From 4eb7dab16eff504772a16f433fd3491a0790c1d0 Mon Sep 17 00:00:00 2001 From: 0611roxe <0611roxe@users.noreply.github.com> Date: Thu, 30 Apr 2026 10:17:22 +0800 Subject: [PATCH] feat: formal RVFI support (M-ext ALTOPS, misalign trap, RVFI CSR channels, debug-mode forcing) Imports the csr branch tree on top of upstream/main as a single commit. Includes: - M-extension ALTOPS support and RV32IMC misa (Cl1MDULp, Cl1Config, Cl1CSR) - Load/store misalign as synchronous exception (Cl1IDEXStage, Cl1EXCP, Cl1WBStage, Cl1Top) - RVFI CSR channels (mstatus/mie/mip/mepc/mcause/mtvec/mscratch/misa) (RVFI.scala, Cl1Top) - Formal-only debug-mode forcing so traps go to mtvec (Cl1Core) - gitignore: mill temp files Verified all 91 riscv-formal checks PASS on the prior baseline. --- .gitignore | 3 + cl1/src/scala/Cl1CSR.scala | 22 +++++-- cl1/src/scala/Cl1Config.scala | 4 +- cl1/src/scala/Cl1Core.scala | 10 +++ cl1/src/scala/Cl1EXCP.scala | 7 ++- cl1/src/scala/Cl1IDEXStage.scala | 2 +- cl1/src/scala/Cl1MDULp.scala | 2 +- cl1/src/scala/Cl1Top.scala | 103 +++++++++++++++++++++++++++++-- cl1/src/scala/Cl1WBStage.scala | 18 ++++++ cl1/src/scala/RVFI.scala | 16 +++++ 10 files changed, 169 insertions(+), 18 deletions(-) diff --git a/.gitignore b/.gitignore index b977fb0..b54d87c 100644 --- a/.gitignore +++ b/.gitignore @@ -42,3 +42,6 @@ patch/firtool/firtool-*/ Thumbs.db .claude/ .codex + +# mill temp files (random 6-char suffix) +mill.?????? diff --git a/cl1/src/scala/Cl1CSR.scala b/cl1/src/scala/Cl1CSR.scala index 3856617..e172e87 100644 --- a/cl1/src/scala/Cl1CSR.scala +++ b/cl1/src/scala/Cl1CSR.scala @@ -247,15 +247,18 @@ class Cl1CSR() extends Module { val dscratch1 = RegEnable(csr_wdat, 0.U(32.W), wen_dscratch1) // Debug Scratch 1 // val mstatus = RegInit("h1800".U(32.W)) - val mtvec = RegEnable(csr_wdat, TVEC_ADDR.U(32.W), wen_mtvec) + // mtvec MODE WARL: only MODE={0,1} are legal; bit[1] is hardwired to 0. + val mtvec_wdata = csr_wdat & ~"h2".U(32.W) + val mtvec = RegEnable(mtvec_wdata, TVEC_ADDR.U(32.W), wen_mtvec) - val mepc_wdata = Mux(cmt_epc_en, cmt_epc_n, csr_wdat) - val mepc = RegEnable(mepc_wdata, 0.U(32.W), wen_mepc) + // mepc is WARL: with the C extension IALIGN=16, so bit[0] is hardwired to 0. + val mepc_wdata = Mux(cmt_epc_en, cmt_epc_n, csr_wdat) & ~"h1".U(32.W) + val mepc = RegEnable(mepc_wdata, 0.U(32.W), wen_mepc) val mcause_wdata = Mux(cmt_cause_en, cmt_cause_n, csr_wdat) - val mcause = RegEnable(cmt_cause_n, 0.U(32.W), wen_mcause) - - val misa = WireInit("h40000104".U(32.W)) + val mcause = RegEnable(mcause_wdata, 0.U(32.W), wen_mcause) + val misa = WireInit("h40001104".U(32.W)) + val allCSRs = Seq( CSRs.misa -> misa, @@ -322,5 +325,12 @@ class Cl1CSR() extends Module { dbg.step_r := step dontTouch(mstatus) + dontTouch(mie) + dontTouch(mip) + dontTouch(mepc) + dontTouch(mcause) + dontTouch(mtvec) + dontTouch(mscratch) + dontTouch(misa) } diff --git a/cl1/src/scala/Cl1Config.scala b/cl1/src/scala/Cl1Config.scala index 600b4af..bc0342a 100644 --- a/cl1/src/scala/Cl1Config.scala +++ b/cl1/src/scala/Cl1Config.scala @@ -32,7 +32,7 @@ object Cl1Config { val Technology = "SMIC110" val FORMAL_VERIF = true - val RISCV_FORMAL_ALTOPS = false + val RISCV_FORMAL_ALTOPS = true val EXPOSE_CORE_BUS = true // When true, expose CoreBus (fetch + mem) instead of AXI4 at top level } @@ -42,4 +42,4 @@ object Cl1PowerSaveConfig { val DCACHE_CKG_EN = if (MODPOWERCFG) true else false val LSU_CKG_EN = if (MODPOWERCFG) true else false val RF_NORESET = true -} +} \ No newline at end of file diff --git a/cl1/src/scala/Cl1Core.scala b/cl1/src/scala/Cl1Core.scala index 5fba898..60617fc 100644 --- a/cl1/src/scala/Cl1Core.scala +++ b/cl1/src/scala/Cl1Core.scala @@ -125,6 +125,16 @@ class Cl1Core extends Module { wbStage.io.toExcp <> excp.io.wb2Excp excp.io.dbg2excp <> dm.io.dbg2excp + if (cl1.Cl1Config.FORMAL_VERIF) { + // Under formal verification, force debug-mode-related signals into + // architectural mode so traps go to mtvec (not the debug exception base). + // BMC otherwise picks anyinit values for dm registers and explores + // debug-mode trap dispatch, which is outside the RVFI ISA model. + excp.io.dbg2excp.debug_mode := false.B + excp.io.dbg2excp.debug_irq_mask := false.B + excp.io.dbg2excp.debug_take_req := false.B + excp.io.dbg2excp.ebrk_excp_en := dm.io.dbg2excp.ebrk_excp_en + } excp.io.excp2Csr <> csr.io.excp_intf excp.io.ext_irq := io.ext_irq diff --git a/cl1/src/scala/Cl1EXCP.scala b/cl1/src/scala/Cl1EXCP.scala index c15a123..9407944 100644 --- a/cl1/src/scala/Cl1EXCP.scala +++ b/cl1/src/scala/Cl1EXCP.scala @@ -111,10 +111,11 @@ class Cl1EXCP() extends Module with TrapCode { tmr_irq & mtie val irq_mask = ~mie | debug_irq_mask val irq_req = irq_req_raw & ~irq_mask + // MEI > MSI > MTI for simultaneously enabled & pending M-mode interrupts. val irq_casue = MuxCase(0.U, Seq( + (ext_irq & meie) -> M_EXTER_IRQ, (sft_irq & msie) -> M_SFTER_IRQ, - (tmr_irq & mtie) -> M_TIMER_IRQ, - (ext_irq & meie) -> M_EXTER_IRQ + (tmr_irq & mtie) -> M_TIMER_IRQ )) val excp_take_en = cmt_ecall | ebrk_excp_en | excp_valid @@ -191,4 +192,4 @@ class Cl1EXCP() extends Module with TrapCode { io.ifu_halt := wfi_ifu_halt io.dxu_halt := dx_halt io.core_wfi := core_wfi_o -} +} \ No newline at end of file diff --git a/cl1/src/scala/Cl1IDEXStage.scala b/cl1/src/scala/Cl1IDEXStage.scala index 4b7f448..2a2e3a2 100644 --- a/cl1/src/scala/Cl1IDEXStage.scala +++ b/cl1/src/scala/Cl1IDEXStage.scala @@ -431,4 +431,4 @@ class Cl1IDEXStage extends Module with TrapCode { Bpustat.io.hit_cnt := hit_cnt } -} +} \ No newline at end of file diff --git a/cl1/src/scala/Cl1MDULp.scala b/cl1/src/scala/Cl1MDULp.scala index 408550e..2500252 100644 --- a/cl1/src/scala/Cl1MDULp.scala +++ b/cl1/src/scala/Cl1MDULp.scala @@ -358,4 +358,4 @@ dontTouch(div_quot_oen) dontTouch(div_remd_oen) dontTouch(div_rslt) -} +} \ No newline at end of file diff --git a/cl1/src/scala/Cl1Top.scala b/cl1/src/scala/Cl1Top.scala index 69b0d11..e36a174 100644 --- a/cl1/src/scala/Cl1Top.scala +++ b/cl1/src/scala/Cl1Top.scala @@ -111,14 +111,19 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) { val wb_flush = BoringUtils.bore(core.wbStage.io.flush) val wb_ecall = BoringUtils.bore(core.wbStage.isValidEcall) val wb_cmt = BoringUtils.bore(core.wbStage.wb_commit) - val rvfi_valid = wb_cmt + val wb_diff_cmt = BoringUtils.bore(core.wbStage.diff_commit) + val trap = BoringUtils.bore(core.excp.excp_take_en) + val wb_excp_fault = BoringUtils.bore(core.wbStage.io.toExcp.excp_valid) + + // Retire through RVFI when the instruction either commits normally, or + // takes an M-mode trap (ECALL, or EBREAK with dcsr.ebreakm==0). + val rvfi_valid = wb_diff_cmt || trap val valid_cnt = Wire(UInt(64.W)) val wb_pc = BoringUtils.bore(core.wbStage.wb_pc) val wb_is_c = BoringUtils.bore(core.wbStage.pplIn.isCInst) val wb_cinst = BoringUtils.bore(core.wbStage.io.cInst) val wb_inst = BoringUtils.bore(core.wbStage.io.inst) valid_cnt := RegEnable((valid_cnt + 1.U), 0.U, rvfi_valid) - val trap = BoringUtils.bore(core.excp.excp_take_en) val dx_rs1_addr = BoringUtils.bore(core.idStage.io.rs1Addr) val dx_rs2_addr = BoringUtils.bore(core.idStage.io.rs2Addr) @@ -165,9 +170,26 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) { rvfi_port.rvfi_valid := rvfi_valid rvfi_port.rvfi_order := valid_cnt rvfi_port.rvfi_insn := Mux(wb_is_c, wb_cinst, wb_inst) - rvfi_port.rvfi_trap := trap + rvfi_port.rvfi_trap := wb_excp_fault rvfi_port.rvfi_halt := false.B - rvfi_port.rvfi_intr := false.B + + val intr_taken = BoringUtils.bore(core.excp.irq_take_en) + val excp_flush_pc = BoringUtils.bore(core.excp.flush_pc) + val excp_flush_ofst = BoringUtils.bore(core.excp.flush_ofst) + val mret_taken = BoringUtils.bore(core.excp.cmt_mret_en) + val trap_target_pc = excp_flush_pc + excp_flush_ofst + + val dbg_flush = BoringUtils.bore(core.dm.io.dbg_flush) + chisel3.assume(!dbg_flush) + + val intr_pending = RegInit(false.B) + when (trap || intr_taken) { + intr_pending := true.B + } .elsewhen (rvfi_valid) { + intr_pending := false.B + } + + rvfi_port.rvfi_intr := intr_pending && rvfi_valid rvfi_port.rvfi_mode := "b11".U(2.W) rvfi_port.rvfi_ixl := "b01".U(2.W) @@ -178,13 +200,84 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) { rvfi_port.rvfi_rd_addr := Mux(wb_rd_wen, wb_rd_addr, 0.U) rvfi_port.rvfi_rd_wdata := Mux(wb_rd_wen, wb_rd_wdata, 0.U) rvfi_port.rvfi_pc_rdata := wb_pc - rvfi_port.rvfi_pc_wdata := Mux(dx_valid, dx_pc,f2_pc) + rvfi_port.rvfi_pc_wdata := Mux(trap || mret_taken, trap_target_pc, + Mux(dx_valid, dx_pc, f2_pc)) rvfi_port.rvfi_mem_addr := Mux(mem_rsp_hsked, mem_addr, 0.U) & "hffff_fffc".U rvfi_port.rvfi_mem_rmask := Mux(mem_rsp_hsked, mem_rmask, 0.U) rvfi_port.rvfi_mem_wmask := Mux(mem_rsp_hsked, mem_wmask, 0.U) rvfi_port.rvfi_mem_rdata := Mux(mem_rsp_hsked, wb_mem_rdata, 0.U) rvfi_port.rvfi_mem_wdata := Mux(mem_rsp_hsked, mem_wdata, 0.U) + + // ---- CSR channels ---- + val wb_csr_idx = BoringUtils.bore(core.wbStage.io.csr_idx) + val wb_csr_wen = BoringUtils.bore(core.wbStage.io.csrWen) + val wb_csr_wdata = BoringUtils.bore(core.wbStage.io.csrWdat) + val wb_csr_rdata = BoringUtils.bore(core.wbStage.pplIn.rdWdat) + + val wb_is_csr_insn = (wb_inst(6,0) === "b1110011".U) && (wb_inst(14,12) =/= 0.U) + + val cur_mstatus = BoringUtils.bore(core.csr.mstatus) + val cur_mie = BoringUtils.bore(core.csr.mie) + val cur_mip = BoringUtils.bore(core.csr.mip) + val cur_mepc = BoringUtils.bore(core.csr.mepc) + val cur_mcause = BoringUtils.bore(core.csr.mcause) + val cur_mtvec = BoringUtils.bore(core.csr.mtvec) + val cur_mscratch = BoringUtils.bore(core.csr.mscratch) + val cur_misa = BoringUtils.bore(core.csr.misa) + + val cmt_epc_en = BoringUtils.bore(core.excp.cmt_epc_en) + val cmt_cause_en = BoringUtils.bore(core.excp.cmt_cause_en) + val cmt_status_en = BoringUtils.bore(core.excp.cmt_status_en) + val cmt_mret_en = BoringUtils.bore(core.excp.cmt_mret_en) + val cmt_epc_n = BoringUtils.bore(core.excp.cmt_epc_n) + val cmt_cause_n = BoringUtils.bore(core.excp.cmt_cause_n) + + val cur_mstatus_mie = cur_mstatus(3) + val cur_mstatus_mpie = cur_mstatus(7) + + val mstatus_trap_wdata = { + val cur = cur_mstatus + val withClrMie = Cat(cur(31, 4), 0.U(1.W), cur(2, 0)) // MIE=0 + val withMpieMie = Cat(withClrMie(31, 8), cur_mstatus_mie, withClrMie(6, 0)) // MPIE<-MIE + withMpieMie + } + val mstatus_mret_wdata = { + val cur = cur_mstatus + val withSetMie = Cat(cur(31, 4), cur_mstatus_mpie, cur(2, 0)) // MIE<-MPIE + val withSetMpie = Cat(withSetMie(31, 8), 1.U(1.W), withSetMie(6, 0)) // MPIE=1 + withSetMpie + } + val mstatus_implicit_wdata = Mux(cmt_status_en, mstatus_trap_wdata, mstatus_mret_wdata) + + def driveCsr(chan: RVFICSR, addr: UInt, cur: UInt, + implicitWrite: Bool = false.B, + implicitWdata: UInt = 0.U): Unit = { + val selCsrInsn = wb_is_csr_insn && (wb_csr_idx === addr) && rvfi_valid + val selW = wb_csr_wen && (wb_csr_idx === addr) && rvfi_valid + val implW = implicitWrite && rvfi_valid + val anyW = selW || implW + chan.rmask := Fill(32, selCsrInsn) + chan.wmask := Fill(32, anyW) + chan.rdata := cur + chan.wdata := Mux(selW, wb_csr_wdata, Mux(implW, implicitWdata, cur)) + } + + driveCsr(rvfi_port.rvfi_csr_mstatus, CSRs.mstatus, cur_mstatus, + cmt_status_en || cmt_mret_en, mstatus_implicit_wdata) + driveCsr(rvfi_port.rvfi_csr_mie, CSRs.mie, cur_mie) + driveCsr(rvfi_port.rvfi_csr_mip, CSRs.mip, cur_mip) + driveCsr(rvfi_port.rvfi_csr_mepc, CSRs.mepc, cur_mepc, + cmt_epc_en, Cat(cmt_epc_n(31, 1), 0.U(1.W))) + driveCsr(rvfi_port.rvfi_csr_mcause, CSRs.mcause, cur_mcause, + cmt_cause_en, cmt_cause_n) + driveCsr(rvfi_port.rvfi_csr_mtvec, CSRs.mtvec, cur_mtvec) + driveCsr(rvfi_port.rvfi_csr_mscratch, CSRs.mscratch, cur_mscratch) + + rvfi_port.rvfi_csr_misa.rmask := Fill(32, true.B) + rvfi_port.rvfi_csr_misa.wmask := 0.U + rvfi_port.rvfi_csr_misa.rdata := cur_misa + rvfi_port.rvfi_csr_misa.wdata := cur_misa }} } diff --git a/cl1/src/scala/Cl1WBStage.scala b/cl1/src/scala/Cl1WBStage.scala index d1a58b1..1f52b08 100644 --- a/cl1/src/scala/Cl1WBStage.scala +++ b/cl1/src/scala/Cl1WBStage.scala @@ -66,6 +66,24 @@ class Cl1WBStage extends Module { val wb_ebreak = pplIn.privInstr(2) val wb_mret = pplIn.privInstr(1) val wb_dret = pplIn.privInstr(0) + + // Formal-only: under `-nordff`, every pipeline register field becomes an + // independent anyinit variable. + if (FORMAL_VERIF) { + val f3_priv = instr(14, 12) === 0.U + val priv_form = (instr(6, 0) === "b1110011".U) & + (instr(11, 7) === 0.U) & + (instr(19, 15) === 0.U) & f3_priv + val f12 = instr(31, 20) + val expected = Cat( + priv_form & (f12 === "h105".U), // wfi + priv_form & (f12 === "h000".U), // ecall + priv_form & (f12 === "h001".U), // ebreak + priv_form & (f12 === "h302".U), // mret + priv_form & (f12 === "h7b2".U) // dret + ) + chisel3.assume(pplIn.privInstr === expected) + } val isValidEcall = wb_valid && wb_ecall val isValidEret = wb_valid && wb_mret diff --git a/cl1/src/scala/RVFI.scala b/cl1/src/scala/RVFI.scala index 44a703b..cc941ff 100644 --- a/cl1/src/scala/RVFI.scala +++ b/cl1/src/scala/RVFI.scala @@ -4,6 +4,13 @@ package cl1 import chisel3._ +class RVFICSR extends Bundle { + val rmask = Output(UInt(32.W)) + val wmask = Output(UInt(32.W)) + val rdata = Output(UInt(32.W)) + val wdata = Output(UInt(32.W)) +} + class RVFI extends Bundle { val rvfi_valid = Output(Bool()) val rvfi_order = Output(UInt(64.W)) @@ -26,4 +33,13 @@ class RVFI extends Bundle { val rvfi_mem_wmask = Output(UInt(4.W)) val rvfi_mem_rdata = Output(UInt(32.W)) val rvfi_mem_wdata = Output(UInt(32.W)) + + val rvfi_csr_mstatus = new RVFICSR + val rvfi_csr_mie = new RVFICSR + val rvfi_csr_mip = new RVFICSR + val rvfi_csr_mepc = new RVFICSR + val rvfi_csr_mcause = new RVFICSR + val rvfi_csr_mtvec = new RVFICSR + val rvfi_csr_mscratch = new RVFICSR + val rvfi_csr_misa = new RVFICSR }