diff --git a/rtl/cv32e40x_cs_registers.sv b/rtl/cv32e40x_cs_registers.sv index a1160824..27da23e3 100644 --- a/rtl/cv32e40x_cs_registers.sv +++ b/rtl/cv32e40x_cs_registers.sv @@ -202,10 +202,10 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; logic [31:0] mintthresh_q, mintthresh_n, mintthresh_rdata; logic mintthresh_we; - logic [31:0] mscratchcsw_q, mscratchcsw_n, mscratchcsw_rdata; + logic [31:0] mscratchcsw_n, mscratchcsw_rdata; logic mscratchcsw_we; - logic [31:0] mscratchcswl_q, mscratchcswl_n, mscratchcswl_rdata; + logic [31:0] mscratchcswl_n, mscratchcswl_rdata; logic mscratchcswl_we; logic [31:0] mclicbase_q, mclicbase_n, mclicbase_rdata; @@ -407,7 +407,18 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; // mscratchcsw: Scratch Swap for Multiple Privilege Modes CSR_MSCRATCHCSW: begin if (SMCLIC) begin - csr_rdata_int = mscratchcsw_rdata; + // CLIC spec 13.2 + // Depending on MPP, we return either mscratch_rdata or rs1 to rd. + // Safe to use mcause_rdata here (EX timing), as there is a generic stall of the ID stage + // whenever a CSR instruction follows another CSR instruction. Alternative implementation using + // a local forward of mcause_rdata is identical (SEC). + if (mcause_rdata.mpp != PRIV_LVL_M) begin + // Return mscratch for writing to GPR + csr_rdata_int = mscratch_rdata; + end else begin + // return rs1 for writing to GPR + csr_rdata_int = id_ex_pipe_i.alu_operand_a; + end end else begin csr_rdata_int = '0; illegal_csr_read = 1'b1; @@ -417,7 +428,18 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; // mscratchcswl: Scratch Swap for Interrupt Levels CSR_MSCRATCHCSWL: begin if (SMCLIC) begin - csr_rdata_int = mscratchcswl_rdata; + // CLIC spec 14.1 + // Depending on mcause.pil and mintstatus.mil, either mscratch or rs1 is returned to rd. + // Safe to use mcause_rdata and mintstatus_rdata here (EX timing), as there is a generic stall of the ID stage + // whenever a CSR instruction follows another CSR instruction. Alternative implementation using + // a local forward of mcause_rdata and mintstatus_rdata is identical (SEC). + if ((mcause_rdata.mpil == '0) != (mintstatus_rdata.mil == 0)) begin + // Return mscratch for writing to GPR + csr_rdata_int = mscratch_rdata; + end else begin + // return rs1 for writing to GPR + csr_rdata_int = id_ex_pipe_i.alu_operand_a; + end end else begin csr_rdata_int = '0; illegal_csr_read = 1'b1; @@ -646,10 +668,10 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; mintthresh_n = csr_wdata_int & CSR_MINTTHRESH_MASK; mintthresh_we = 1'b0; - mscratchcsw_n = csr_wdata_int; // todo: isssue 589 + mscratchcsw_n = mscratch_n; // mscratchcsw operates conditionally on mscratch mscratchcsw_we = 1'b0; - mscratchcswl_n = csr_wdata_int; // todo: isssue 589 + mscratchcswl_n = mscratch_n; // mscratchcswl operates conditionally on mscratch mscratchcswl_we = 1'b0; mie_n = '0; @@ -827,13 +849,22 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; CSR_MSCRATCHCSW: begin if (SMCLIC) begin - mscratchcsw_we = 1'b1; + // mscratchcsw operates on mscratch + // Writing only when mcause.mpp != PRIV_LVL_M + if (mcause_rdata.mpp != PRIV_LVL_M) begin + mscratchcsw_we = 1'b1; + mscratch_we = 1'b1; + end end end CSR_MSCRATCHCSWL: begin if (SMCLIC) begin - mscratchcswl_we = 1'b1; + // mscratchcswl operates on mscratch + if ((mcause_rdata.mpil == '0) != (mintstatus_rdata.mil == '0)) begin + mscratchcswl_we = 1'b1; + mscratch_we = 1'b1; + end end end @@ -1244,34 +1275,6 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; .rd_data_o ( mintthresh_q ) ); - cv32e40x_csr - #( - .WIDTH (32), - .RESETVALUE (32'h0) - ) - mscratchcsw_csr_i - ( - .clk ( clk ), - .rst_n ( rst_n ), - .wr_data_i ( mscratchcsw_n ), - .wr_en_i ( mscratchcsw_we ), - .rd_data_o ( mscratchcsw_q ) - ); - - cv32e40x_csr - #( - .WIDTH (32), - .RESETVALUE (32'h0) - ) - mscratchcswl_csr_i - ( - .clk ( clk ), - .rst_n ( rst_n ), - .wr_data_i ( mscratchcswl_n ), - .wr_en_i ( mscratchcswl_we ), - .rd_data_o ( mscratchcswl_q ) - ); - cv32e40x_csr #( .WIDTH (32), @@ -1322,10 +1325,6 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; assign mintthresh_q = 32'h0; - assign mscratchcsw_q = 32'h0; - - assign mscratchcswl_q = 32'h0; - assign mclicbase_q = 32'h0; end @@ -1346,8 +1345,6 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; assign mtvt_rdata = mtvt_q; assign mintstatus_rdata = mintstatus_q; assign mintthresh_rdata = mintthresh_q; - assign mscratchcsw_rdata = mscratchcsw_q; - assign mscratchcswl_rdata = mscratchcswl_q; assign mclicbase_rdata = mclicbase_q; assign mie_rdata = mie_q; @@ -1356,6 +1353,15 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; // if no interrupt is pending. assign mnxti_rdata = mnxti_irq_pending_i ? {mtvt_addr_o, mnxti_irq_id_i, 2'b00} : 32'h00000000; + // mscratchcsw_rdata breaks the regular convension for CSrs. Read data depend on mcause.mpp + // mscratch_rdata is returned if mcause.mpp differs from PRIV_LVL_M, otherwise rs1 is returned. + // This signal is only used by RVFI, and has WB timing (rs1 comes from ex_wb_pipe_i.csr_wdata, flopped version of id_ex_pipe.alu_operand_a) + assign mscratchcsw_rdata = (mcause_rdata.mpp != PRIV_LVL_M) ? mscratch_rdata : ex_wb_pipe_i.csr_wdata; + + // mscratchcswl_rdata breaks the regular convension for CSrs. Read data depend on mcause.pil and mintstatus.mil. + // This signal is only used by RVFI, and has WB timing (rs1 comes from ex_wb_pipe_i.csr_wdata, flopped version of id_ex_pipe.alu_operand_a) + assign mscratchcswl_rdata = ((mcause_rdata.mpil == '0) != (mintstatus_rdata.mil == 0)) ? mscratch_rdata : ex_wb_pipe_i.csr_wdata; + assign mip_rdata = mip_i; assign misa_rdata = MISA_VALUE; assign mstatush_rdata = 32'h0; @@ -1749,6 +1755,7 @@ module cv32e40x_cs_registers import cv32e40x_pkg::*; // Some signals are unused on purpose (typically they are used by RVFI code). Use them here for easier LINT waiving. assign unused_signals = tselect_we | tinfo_we | tcontrol_we | mstatush_we | misa_we | mip_we | mvendorid_we | - marchid_we | mimpid_we | mhartid_we | mconfigptr_we | mtval_we | (|mnxti_n); + marchid_we | mimpid_we | mhartid_we | mconfigptr_we | mtval_we | (|mnxti_n) | mscratchcsw_we | mscratchcswl_we | + (|mscratchcsw_rdata) | (|mscratchcswl_rdata) | (|mscratchcsw_n) | (|mscratchcswl_n); endmodule diff --git a/sva/cv32e40x_cs_registers_sva.sv b/sva/cv32e40x_cs_registers_sva.sv index c123268e..5b95dc8e 100644 --- a/sva/cv32e40x_cs_registers_sva.sv +++ b/sva/cv32e40x_cs_registers_sva.sv @@ -46,7 +46,13 @@ module cv32e40x_cs_registers_sva input logic clic_pa_valid_o, input mintstatus_t mintstatus_rdata, input privlvl_t priv_lvl_n, - input privlvl_t priv_lvl_rdata + input privlvl_t priv_lvl_rdata, + input logic [31:0] mscratch_rdata, + input mcause_t mcause_rdata, + csr_num_e csr_waddr, + input logic mscratch_we, + input logic instr_valid, + input csr_opcode_e csr_op ); @@ -90,6 +96,38 @@ module cv32e40x_cs_registers_sva a_htrap_interrupt_level: assert property(p_htrap_interrupt_level) else `uvm_error("cs_registers", "Horizontal trap taken caused interrupt level to change"); + + // Check that mscratch do not update due to mscratchcsw if the conditions are not right + property p_mscratchcsw_mscratch; + @(posedge clk) disable iff (!rst_n) + ( ex_wb_pipe_i.csr_en && (csr_waddr == CSR_MSCRATCHCSW) && (mcause_rdata.mpp == PRIV_LVL_M) + |=> $stable(mscratch_rdata)); + endproperty; + + a_mscratchcsw_mscratch: assert property(p_mscratchcsw_mscratch) + else `uvm_error("cs_registers", "Mscratch not stable after mscratwchsw with mpp=M"); + + // Check that mscratch do not update due to mscratchcswl if the conditions are not right + property p_mscratchcswl_mscratch; + @(posedge clk) disable iff (!rst_n) + ( ex_wb_pipe_i.csr_en && (csr_waddr == CSR_MSCRATCHCSWL) && !((mcause_rdata.mpil == '0) != (mintstatus_rdata.mil == '0)) + |=> $stable(mscratch_rdata)); + endproperty; + + a_mscratchcswl_mscratch: assert property(p_mscratchcswl_mscratch) + else `uvm_error("cs_registers", "Mscratch not stable after mscratwchswl"); + + // Check that mscratch is written by mscratchcswl when the conditions are right + property p_mscratchcswl_mscratch_we; + @(posedge clk) disable iff (!rst_n) + ( ex_wb_pipe_i.csr_en && (csr_waddr == CSR_MSCRATCHCSWL) && ((mcause_rdata.mpil == '0) != (mintstatus_rdata.mil == '0)) + && (csr_op != CSR_OP_READ) && instr_valid + |-> mscratch_we); + endproperty; + + a_mscratchcswl_mscratch_we: assert property(p_mscratchcswl_mscratch_we) + else `uvm_error("cs_registers", "Mscratch not written by mscratchcswl"); + end endmodule