diff --git a/bhv/cv32e40x_wrapper.sv b/bhv/cv32e40x_wrapper.sv index 57370391..10211ff1 100644 --- a/bhv/cv32e40x_wrapper.sv +++ b/bhv/cv32e40x_wrapper.sv @@ -33,6 +33,7 @@ `include "cv32e40x_sleep_unit_sva.sv" `include "cv32e40x_rvfi_sva.sv" `include "cv32e40x_sequencer_sva.sv" + `include "cv32e40x_clic_int_controller_sva.sv" `endif `include "cv32e40x_wrapper.vh" @@ -215,7 +216,12 @@ module cv32e40x_wrapper .prefetch_valid_if_i (core_i.if_stage_i.prefetch_valid), .prefetch_is_tbljmp_ptr_if_i (core_i.if_stage_i.prefetch_is_tbljmp_ptr), .*); - bind cv32e40x_cs_registers: core_i.cs_registers_i cv32e40x_cs_registers_sva #(.SMCLIC(SMCLIC)) cs_registers_sva (.*); + bind cv32e40x_cs_registers: + core_i.cs_registers_i + cv32e40x_cs_registers_sva + #(.SMCLIC(SMCLIC)) + cs_registers_sva (.wb_valid_i (core_i.wb_valid), + .*); bind cv32e40x_load_store_unit: core_i.load_store_unit_i cv32e40x_load_store_unit_sva #(.DEPTH (DEPTH)) load_store_unit_sva ( @@ -263,11 +269,9 @@ module cv32e40x_wrapper .branch_taken_in_ex (core_i.controller_i.controller_fsm_i.branch_taken_ex), .exc_cause (core_i.controller_i.controller_fsm_i.exc_cause), // probed controller signals - .ctrl_fsm_ns (core_i.controller_i.controller_fsm_i.ctrl_fsm_ns), .ctrl_debug_mode_n (core_i.controller_i.controller_fsm_i.debug_mode_n), .ctrl_pending_debug (core_i.controller_i.controller_fsm_i.pending_debug), .ctrl_debug_allowed (core_i.controller_i.controller_fsm_i.debug_allowed), - .ctrl_pending_nmi (core_i.controller_i.controller_fsm_i.pending_nmi), .ctrl_pending_interrupt (core_i.controller_i.controller_fsm_i.pending_interrupt), .ctrl_interrupt_allowed (core_i.controller_i.controller_fsm_i.interrupt_allowed), .id_stage_multi_cycle_id_stall (core_i.id_stage_i.multi_cycle_id_stall), @@ -283,9 +287,19 @@ module cv32e40x_wrapper .irq_ack (core_i.irq_ack), .mie_n (core_i.cs_registers_i.mie_n), .mie_we (core_i.cs_registers_i.mie_we), - .clic_irq_q (core_i.gen_clic_interrupt.clic_int_controller_i.clic_irq_q), - .clic_irq_level_q (core_i.gen_clic_interrupt.clic_int_controller_i.clic_irq_level_q), .*); +generate +if (SMCLIC) begin : clic_asserts + bind cv32e40x_clic_int_controller: + core_i.gen_clic_interrupt.clic_int_controller_i + cv32e40x_clic_int_controller_sva + clic_int_controller_sva (.ctrl_pending_interrupt (core_i.controller_i.controller_fsm_i.pending_interrupt), + .ctrl_interrupt_allowed (core_i.controller_i.controller_fsm_i.interrupt_allowed), + .ctrl_fsm (core_i.ctrl_fsm), + .dcsr (core_i.dcsr), + .*); +end +endgenerate bind cv32e40x_sleep_unit: core_i.sleep_unit_i cv32e40x_sleep_unit_sva diff --git a/rtl/cv32e40x_controller.sv b/rtl/cv32e40x_controller.sv index a8d9b197..2e355ece 100644 --- a/rtl/cv32e40x_controller.sv +++ b/rtl/cv32e40x_controller.sv @@ -79,6 +79,7 @@ module cv32e40x_controller import cv32e40x_pkg::*; input logic [1:0] lsu_err_wb_i, // LSU bus error in WB stage input logic lsu_busy_i, // LSU is busy with outstanding transfers input logic lsu_interruptible_i, // LSU may be interrupted + input logic lsu_valid_wb_i, // LSU is valid in WB (factors in rvalid from either OBI bus or write buffer) // jump/branch signals input logic branch_decision_ex_i, // branch decision signal from EX ALU @@ -182,6 +183,7 @@ module cv32e40x_controller import cv32e40x_pkg::*; .wb_valid_i ( wb_valid_i ), .last_op_wb_i ( last_op_wb_i ), .abort_op_wb_i ( abort_op_wb_i ), + .lsu_valid_wb_i ( lsu_valid_wb_i ), .lsu_interruptible_i ( lsu_interruptible_i ), diff --git a/rtl/cv32e40x_controller_bypass.sv b/rtl/cv32e40x_controller_bypass.sv index ab3c5c13..c74dfe14 100644 --- a/rtl/cv32e40x_controller_bypass.sv +++ b/rtl/cv32e40x_controller_bypass.sv @@ -144,7 +144,12 @@ module cv32e40x_controller_bypass import cv32e40x_pkg::*; // This is needed because the data bypass from EX uses csr_rdata, and for mnxti this is actually mstatus and not the result // that will be written to the register file. Could be optimized to only stall when the result from the CSR instruction is used in ID, // but the common usecase is a CSR access followed by a branch using the mnxti result in the RF, so it would likely stall in most cases anyway. - assign ctrl_byp_o.mnxti_stall = csr_mnxti_read_i; + assign ctrl_byp_o.mnxti_id_stall = csr_mnxti_read_i; + + // Stall EX stage when an mnxti is in EX and an LSU instruction is in WB. + // This is needed to make sure that any external interrupt clearing (due to a LSU instruction) gets picked + // up correctly by the mnxti access. + assign ctrl_byp_o.mnxti_ex_stall = csr_mnxti_read_i && (ex_wb_pipe_i.lsu_en && ex_wb_pipe_i.instr_valid); genvar i; generate diff --git a/rtl/cv32e40x_controller_fsm.sv b/rtl/cv32e40x_controller_fsm.sv index cfef6126..b31d3fd8 100644 --- a/rtl/cv32e40x_controller_fsm.sv +++ b/rtl/cv32e40x_controller_fsm.sv @@ -75,6 +75,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // From LSU (WB) input mpu_status_e lsu_mpu_status_wb_i, // MPU status (WB timing) input logic data_stall_wb_i, // WB stalled by LSU + input logic lsu_valid_wb_i, // LSU instruction in WB is valid input logic lsu_busy_i, // LSU is busy with outstanding transfers input logic lsu_interruptible_i, // LSU can be interrupted @@ -228,6 +229,9 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; logic sequence_in_progress_id; logic id_stage_haltable; + // Flag that is high during the cycle after an LSU instruction finishes in WB + logic interrupt_blanking_q; + assign sequence_interruptible = !sequence_in_progress_wb; assign id_stage_haltable = !sequence_in_progress_id; @@ -440,10 +444,10 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // Once the first part of a table jump has finished in WB, we are not allowed to take interrupts before the last part finishes. This can be detected when the last // part of a table jump is in either EX or WB. - assign interrupt_allowed = lsu_interruptible_i && debug_interruptible && !fencei_ongoing && !xif_in_wb && sequence_interruptible; + assign interrupt_allowed = lsu_interruptible_i && debug_interruptible && !fencei_ongoing && !xif_in_wb && sequence_interruptible && !interrupt_blanking_q; - // Allowing NMI's follow the same rule as regular interrupts. - assign nmi_allowed = interrupt_allowed; + // Allowing NMI's follow the same rule as regular interrupts, except we don't need to regard blanking of NMIs after a load/store. + assign nmi_allowed = lsu_interruptible_i && debug_interruptible && !fencei_ongoing && !xif_in_wb && sequence_interruptible; // Do not allow interrupts if in debug mode, or single stepping without dcsr.stepie set. assign debug_interruptible = !(debug_mode_q || (dcsr_i.step && !dcsr_i.stepie)); @@ -521,7 +525,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // Sequences: If we need to halt for debug or interrupt not allowed due to a sequence, we must check if we can // actually halt the ID stage or not. Halting the same sequence that causes *_allowed to go to 0 // may cause a deadlock. - ctrl_fsm_o.halt_id = ctrl_byp_i.jalr_stall || ctrl_byp_i.load_stall || ctrl_byp_i.csr_stall || ctrl_byp_i.wfi_stall || ctrl_byp_i.mnxti_stall || + ctrl_fsm_o.halt_id = ctrl_byp_i.jalr_stall || ctrl_byp_i.load_stall || ctrl_byp_i.csr_stall || ctrl_byp_i.wfi_stall || ctrl_byp_i.mnxti_id_stall || (((pending_interrupt && !interrupt_allowed) || (pending_nmi && !nmi_allowed) || (pending_nmi_early)) && debug_interruptible && id_stage_haltable) || (pending_debug && !debug_allowed && id_stage_haltable); @@ -530,7 +534,7 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; // Also halting EX if an offloaded instruction in WB may cause an exception, such that a following offloaded // instruction can correctly receive commit_kill. // Halting EX when an instruction in WB may cause an interrupt to become pending. - ctrl_fsm_o.halt_ex = ctrl_byp_i.minstret_stall || ctrl_byp_i.xif_exception_stall || ctrl_byp_i.irq_enable_stall; + ctrl_fsm_o.halt_ex = ctrl_byp_i.minstret_stall || ctrl_byp_i.xif_exception_stall || ctrl_byp_i.irq_enable_stall || ctrl_byp_i.mnxti_ex_stall; ctrl_fsm_o.halt_wb = 1'b0; // By default no stages are killed @@ -1020,6 +1024,18 @@ module cv32e40x_controller_fsm import cv32e40x_pkg::*; end end + // Flop used to track LSU instructions in WB. High in the cycle after an LSU instruction + // leaves WB. + // Used for disregarding interrupts one cycle after a load/store to make sure the + // interrupt controller propagates the inputs through its flops. + always_ff @(posedge clk, negedge rst_n) begin + if (rst_n == 1'b0) begin + interrupt_blanking_q <= 1'b0; + end else begin + interrupt_blanking_q <= ex_wb_pipe_i.instr_valid && ex_wb_pipe_i.lsu_en; + end + end + // Flops for fencei handshake request always_ff @(posedge clk, negedge rst_n) begin if (rst_n == 1'b0) begin diff --git a/rtl/cv32e40x_core.sv b/rtl/cv32e40x_core.sv index 89d20e51..e226f39f 100644 --- a/rtl/cv32e40x_core.sv +++ b/rtl/cv32e40x_core.sv @@ -851,6 +851,7 @@ module cv32e40x_core import cv32e40x_pkg::*; .lsu_err_wb_i ( lsu_err_wb ), .lsu_busy_i ( lsu_busy ), .lsu_interruptible_i ( lsu_interruptible ), + .lsu_valid_wb_i ( lsu_valid_wb ), // jump/branch control .branch_decision_ex_i ( branch_decision_ex ), diff --git a/rtl/include/cv32e40x_pkg.sv b/rtl/include/cv32e40x_pkg.sv index 2379055c..4d25fbce 100644 --- a/rtl/include/cv32e40x_pkg.sv +++ b/rtl/include/cv32e40x_pkg.sv @@ -1204,7 +1204,8 @@ typedef struct packed { logic load_stall; // Stall due to load operation logic csr_stall; logic wfi_stall; - logic mnxti_stall; // Stall due to mnxti CSR access in EX + logic mnxti_id_stall; // Stall ID due to mnxti CSR access in EX + logic mnxti_ex_stall; // Stall EX due to LSU instruction in WB logic minstret_stall; // Stall due to minstret/h read in EX logic deassert_we; // Deassert write enable and special insn bits logic id_stage_abort; // Same signal as deassert_we, with better name for use in the controller. diff --git a/sva/cv32e40x_clic_int_controller_sva.sv b/sva/cv32e40x_clic_int_controller_sva.sv new file mode 100644 index 00000000..58496430 --- /dev/null +++ b/sva/cv32e40x_clic_int_controller_sva.sv @@ -0,0 +1,76 @@ +// Copyright 2022 Silicon Labs, Inc. +// +// This file, and derivatives thereof are licensed under the +// Solderpad License, Version 2.0 (the "License"). +// +// Use of this file means you agree to the terms and conditions +// of the license and are in full compliance with the License. +// +// You may obtain a copy of the License at: +// +// https://solderpad.org/licenses/SHL-2.0/ +// +// Unless required by applicable law or agreed to in writing, software +// and hardware implementations thereof distributed under the License +// is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS +// OF ANY KIND, EITHER EXPRESSED OR IMPLIED. +// +// See the License for the specific language governing permissions and +// limitations under the License. + +//////////////////////////////////////////////////////////////////////////////// +// Engineer: Øystein Knauserud - oystein.knauserud@silabs.com // +// // +// Design Name: cv32e40x_clic_int_controller_sva // +// Project Name: CV32E40X // +// Language: SystemVerilog // +// // +// Description: Assertions reltated to the CLIC interrupt controller // +// // +//////////////////////////////////////////////////////////////////////////////// + +module cv32e40x_clic_int_controller_sva + import uvm_pkg::*; + import cv32e40x_pkg::*; + ( + input logic clk, + input logic rst_n, + + input logic irq_req_ctrl_o, + input logic clic_irq_q, + input logic [7:0] clic_irq_level_q, + + input logic ctrl_pending_interrupt, + input logic ctrl_interrupt_allowed, + + input ctrl_fsm_t ctrl_fsm, + input dcsr_t dcsr + + ); + + + // Check that a pending interrupt is taken as soon as possible after being enabled + property p_clic_enable; + @(posedge clk) disable iff (!rst_n) + ( !irq_req_ctrl_o + ##1 + irq_req_ctrl_o && $stable(clic_irq_q) && $stable(clic_irq_level_q) && !(ctrl_fsm.debug_mode || (dcsr.step && !dcsr.stepie)) + |-> (ctrl_pending_interrupt && ctrl_interrupt_allowed)); + endproperty; + + a_clic_enable: assert property(p_clic_enable) + else `uvm_error("core", "Interrupt not taken soon enough after enabling"); + + // Check a pending interrupt that is disabled is actually not taken + property p_clic_disable; + @(posedge clk) disable iff (!rst_n) + ( irq_req_ctrl_o + ##1 + !irq_req_ctrl_o && $stable(clic_irq_q) && $stable(clic_irq_level_q) + |-> !(ctrl_pending_interrupt && ctrl_interrupt_allowed)); + endproperty; + + a_clic_disable: assert property(p_clic_disable) + else `uvm_error("core", "Interrupt taken after disabling"); +endmodule // cv32e40x_cs_registers_sva + diff --git a/sva/cv32e40x_core_sva.sv b/sva/cv32e40x_core_sva.sv index dd65d8df..94f2cf7e 100644 --- a/sva/cv32e40x_core_sva.sv +++ b/sva/cv32e40x_core_sva.sv @@ -79,17 +79,13 @@ module cv32e40x_core_sva input logic ctrl_debug_allowed, input logic ctrl_interrupt_allowed, input logic ctrl_pending_interrupt, - input ctrl_state_e ctrl_fsm_ns, input ctrl_byp_t ctrl_byp, - input logic ctrl_pending_nmi, - // probed cs_registers signals + // probed cs_registers signals input logic [31:0] cs_registers_mie_q, input logic [31:0] cs_registers_mepc_n, input mcause_t cs_registers_csr_cause_i, // From controller input mcause_t cs_registers_mcause_q, // From cs_registers, flopped mcause - input mstatus_t cs_registers_mstatus_q, - input logic clic_irq_q, - input logic [7:0] clic_irq_level_q); + input mstatus_t cs_registers_mstatus_q); if (SMCLIC) begin property p_clic_mie_tieoff; @@ -484,31 +480,7 @@ end a_tbljmp_stall: assert property(p_tbljmp_stall) else `uvm_error("core", "Table jump not stalled while CSR is written"); -if (SMCLIC) begin - // Check that a pending interrupt is taken as soon as possible after being enabled - property p_clic_enable; - @(posedge clk) disable iff (!rst_ni) - ( !irq_req_ctrl - ##1 - irq_req_ctrl && $stable(clic_irq_q) && $stable(clic_irq_level_q) && !(ctrl_fsm.debug_mode || (dcsr.step && !dcsr.stepie)) - |-> (ctrl_pending_interrupt && ctrl_interrupt_allowed)); - endproperty; - - a_clic_enable: assert property(p_clic_enable) - else `uvm_error("core", "Interrupt not taken soon enough after enabling"); - - // Check a pending interrupt that is disabled is actually not taken - property p_clic_disable; - @(posedge clk) disable iff (!rst_ni) - ( irq_req_ctrl - ##1 - !irq_req_ctrl && $stable(clic_irq_q) && $stable(clic_irq_level_q) - |-> !(ctrl_pending_interrupt && ctrl_interrupt_allowed)); - endproperty; - - a_clic_disable: assert property(p_clic_disable) - else `uvm_error("core", "Interrupt taken after disabling"); -end else begin +if (!SMCLIC) begin // Check that a pending interrupt is taken as soon as possible after being enabled property p_mip_mie_write_enable; @(posedge clk) disable iff (!rst_ni) @@ -533,5 +505,18 @@ end else begin a_mip_mie_write_disable: assert property(p_mip_mie_write_disable) else `uvm_error("core", "Interrupt taken after disabling"); end + +// Clearing external interrupts via a store instruction causes irq_i to go low the next cycle. + // The interrupt controller uses flopped versions of irq_i, and thus we need to disregard interrupts + // for one cycle after an rvalid has been observed. +property p_no_irq_after_lsu; + @(posedge clk) disable iff (!rst_ni) + ( wb_valid && ex_wb_pipe.lsu_en && ex_wb_pipe.instr_valid + |=> + !ctrl_interrupt_allowed); +endproperty; + +a_no_irq_after_lsu: assert property(p_no_irq_after_lsu) + else `uvm_error("core", "Interrupt taken after disabling"); endmodule // cv32e40x_core_sva diff --git a/sva/cv32e40x_cs_registers_sva.sv b/sva/cv32e40x_cs_registers_sva.sv index bcfaaa17..5502492f 100644 --- a/sva/cv32e40x_cs_registers_sva.sv +++ b/sva/cv32e40x_cs_registers_sva.sv @@ -34,9 +34,17 @@ module cv32e40x_cs_registers_sva input logic rst_n, input ctrl_fsm_t ctrl_fsm_i, input id_ex_pipe_t id_ex_pipe_i, + input ex_wb_pipe_t ex_wb_pipe_i, input logic [31:0] csr_rdata_o, input logic csr_we_int, - input logic [1:0] mtvec_mode_o + input logic [1:0] mtvec_mode_o, + input logic wb_valid_i, + input logic mnxti_we, + input logic mintstatus_we, + input logic mcause_we, + input logic [31:0] clic_pa_o, + input logic clic_pa_valid_o + ); @@ -53,6 +61,19 @@ module cv32e40x_cs_registers_sva assert property (@(posedge clk) disable iff (!rst_n) 1'b1 |-> mtvec_mode_o == 2'b11) else `uvm_error("cs_registers", "mtvec_mode is not 2'b11 in CLIC mode") + + // Accesses to MNXTI are stalled in EX if there is a LSU instruction in WB. + // Thus no mnxti should be in WB (clic_pa_valid_o) the cycle after an LSU instruction + // is done in WB. + property p_no_mnxti_after_lsu; + @(posedge clk) disable iff (!rst_n) + ( wb_valid_i && ex_wb_pipe_i.lsu_en && ex_wb_pipe_i.instr_valid + |=> + !clic_pa_valid_o); + endproperty; + + a_no_mnxti_after_lsu: assert property(p_no_mnxti_after_lsu) + else `uvm_error("core", "Mnxti should not we in WB the cycle after an LSU instruction"); end endmodule // cv32e40x_cs_registers_sva