From 7284b27c2ee584770a312bbdba57fc04b19d20da Mon Sep 17 00:00:00 2001 From: 0611roxe <0611roxe@users.noreply.github.com> Date: Wed, 24 Jun 2026 11:15:09 +0800 Subject: [PATCH] fix(formal): repair RVFI retire and memory fault reporting --- Makefile | 7 ++++++- cl1/src/scala/Cl1Top.scala | 35 +++++++++++++++++++++++------------ cl1/src/scala/RVFI.scala | 3 +++ 3 files changed, 32 insertions(+), 13 deletions(-) diff --git a/Makefile b/Makefile index 1f88cec..1737812 100644 --- a/Makefile +++ b/Makefile @@ -10,6 +10,7 @@ DUMP_WAVE := PWR_ANALYSIS :=1 CL1_TEST_MODE ?= cache CL1_PLATFORM ?= simple_soc +CL1_AXI_FORMAL_CACHE_IDXW ?= 1 CONFIG_DBG = n CONFIG_NETSIM = n @@ -72,7 +73,7 @@ WAVE ?= gtkwave # Phony Targets .DEFAULT_GOAL := verilog -.PHONY: all verilog verilog-sim verilog-full-cache-axi verilog-full-soc-syn verilog-full-soc-diff verilog-no-cache verilog-rvfi verilog-rvfi-axi verilog-rvfi-cache help reformat checkformat clean run +.PHONY: all verilog verilog-sim verilog-full-cache-axi verilog-full-soc-syn verilog-full-soc-diff verilog-no-cache verilog-rvfi verilog-rvfi-axi verilog-rvfi-axi-cache verilog-rvfi-cache help reformat checkformat clean run # Generate Verilog FIRTOOL_VERSION = 1.105.0 @@ -125,6 +126,10 @@ verilog-rvfi: verilog-rvfi-axi: $(call gen_verilog,CL1_TEST_MODE=cache CL1_TOP_NAME=Cl1Top_RVFI_AXI CL1_FORMAL_VERIF=true CL1_RISCV_FORMAL_ALTOPS=true CL1_HAS_ICACHE=false CL1_HAS_DCACHE=false,Cl1Top_RVFI_AXI) +# RVFI with riscv-formal M-extension alternative ops, AXI exposed, I/D cache enabled. +verilog-rvfi-axi-cache: + $(call gen_verilog,CL1_TEST_MODE=cache CL1_TOP_NAME=Cl1Top_AXI_CACHE CL1_FORMAL_VERIF=true CL1_RISCV_FORMAL_ALTOPS=true CL1_HAS_ICACHE=true CL1_HAS_DCACHE=true CL1_SYN=false CL1_FORMAL_CACHE_IDXW=$(CL1_AXI_FORMAL_CACHE_IDXW),Cl1Top_AXI_CACHE) + # RVFI with riscv-formal M-extension alternative ops, AXI exposed, minimal cache. verilog-rvfi-cache: $(call gen_verilog,CL1_TEST_MODE=cache CL1_TOP_NAME=Cl1Top_RVFI_CACHE CL1_FORMAL_VERIF=true CL1_RISCV_FORMAL_ALTOPS=true CL1_HAS_ICACHE=true CL1_HAS_DCACHE=true CL1_SYN=false,Cl1Top_RVFI_CACHE) diff --git a/cl1/src/scala/Cl1Top.scala b/cl1/src/scala/Cl1Top.scala index c486238..7869bcc 100644 --- a/cl1/src/scala/Cl1Top.scala +++ b/cl1/src/scala/Cl1Top.scala @@ -113,12 +113,14 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) { val wb_valid = BoringUtils.bore(core.wbStage.wb_valid) 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 trap = BoringUtils.bore(core.excp.excp_req) + val wb_diff_cmt = BoringUtils.bore(core.wbStage.diff_commit) + val trap_req = BoringUtils.bore(core.excp.excp_req) val wb_excp_fault = BoringUtils.bore(core.wbStage.io.toExcp.excp_valid) + val wb_excp_code = BoringUtils.bore(core.wbStage.io.toExcp.excp_code) - // Retire through RVFI when the instruction commits at writeback. - val rvfi_valid = wb_cmt + // RVFI valid is a retire pulse. Exception requests are control-flow requests + // and can remain asserted while WB is stalled, so they must not create retires. + val rvfi_valid = wb_diff_cmt 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) @@ -168,9 +170,15 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) { val mem_wmask = RegEnable(mem_wmask_n, 0.U, mem_req_hsked) val mem_wdata = RegEnable(mem_wdata_n, 0.U, mem_req_hsked) + val inst_access_fault = rvfi_valid && wb_excp_fault && (wb_excp_code === 1.U) + val load_access_fault = rvfi_valid && wb_excp_fault && (wb_excp_code === 5.U) + val store_access_fault = rvfi_valid && wb_excp_fault && (wb_excp_code === 7.U) + val data_access_fault = load_access_fault || store_access_fault + val mem_fault = inst_access_fault || data_access_fault + 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_insn := Mux(inst_access_fault, 0.U, Mux(wb_is_c, wb_cinst, wb_inst)) rvfi_port.rvfi_trap := wb_excp_fault rvfi_port.rvfi_halt := false.B @@ -179,13 +187,13 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) { val excp_flush_ofst = BoringUtils.bore(core.excp.flush_ofst) val mret_taken = BoringUtils.bore(core.excp.cmt_mret_en) val cur_excp_mtvec = BoringUtils.bore(core.csr.mtvec) - val trap_target_pc = Mux(trap, Cat(cur_excp_mtvec(31, 2), 0.U(2.W)), excp_flush_pc + excp_flush_ofst) + val trap_target_pc = Mux(trap_req, Cat(cur_excp_mtvec(31, 2), 0.U(2.W)), 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) { + when (trap_req || intr_taken) { intr_pending := true.B } .elsewhen (rvfi_valid) { intr_pending := false.B @@ -202,14 +210,17 @@ 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(trap || mret_taken, trap_target_pc, + rvfi_port.rvfi_pc_wdata := Mux(trap_req || 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) - 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_addr := Mux(mem_rsp_hsked || data_access_fault, mem_addr, 0.U) + rvfi_port.rvfi_mem_rmask := Mux(data_access_fault, 0.U, Mux(mem_rsp_hsked, mem_rmask, 0.U)) + rvfi_port.rvfi_mem_wmask := Mux(data_access_fault, 0.U, 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) + rvfi_port.rvfi_mem_wdata := Mux(mem_rsp_hsked || store_access_fault, mem_wdata, 0.U) + rvfi_port.rvfi_mem_fault := mem_fault + rvfi_port.rvfi_mem_fault_rmask := Mux(load_access_fault, mem_rmask, 0.U) + rvfi_port.rvfi_mem_fault_wmask := Mux(store_access_fault, mem_wmask, 0.U) // ---- CSR channels ---- val wb_csr_idx = BoringUtils.bore(core.wbStage.io.csr_idx) diff --git a/cl1/src/scala/RVFI.scala b/cl1/src/scala/RVFI.scala index 3acec50..791b3dc 100644 --- a/cl1/src/scala/RVFI.scala +++ b/cl1/src/scala/RVFI.scala @@ -33,6 +33,9 @@ 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_mem_fault = Output(Bool()) + val rvfi_mem_fault_rmask = Output(UInt(4.W)) + val rvfi_mem_fault_wmask = Output(UInt(4.W)) val rvfi_csr_mstatus = new RVFICSR val rvfi_csr_mie = new RVFICSR