diff --git a/hdl/hazard3_core.v b/hdl/hazard3_core.v index f70d69c..84ef382 100644 --- a/hdl/hazard3_core.v +++ b/hdl/hazard3_core.v @@ -901,7 +901,7 @@ hazard3_csr #( // Trap signalling .trap_addr (m_trap_addr), .trap_is_irq (m_trap_is_irq), - .m_trap_is_debug_entry (m_trap_is_debug_entry), + .trap_is_debug_entry (m_trap_is_debug_entry), .trap_enter_soon (m_trap_enter_soon), .trap_enter_vld (m_trap_enter_vld), .trap_enter_rdy (m_trap_enter_rdy), diff --git a/hdl/hazard3_cpu_2port.v b/hdl/hazard3_cpu_2port.v index 66ffa84..47110a1 100644 --- a/hdl/hazard3_cpu_2port.v +++ b/hdl/hazard3_cpu_2port.v @@ -65,14 +65,14 @@ module hazard3_cpu_2port #( output wire dbg_instr_caught_exception, output wire dbg_instr_caught_ebreak, // Optional debug system bus access patch-through - input wire [31:0] dbg_sbus_addr, + input wire [W_ADDR-1:0] dbg_sbus_addr, input wire dbg_sbus_write, input wire [1:0] dbg_sbus_size, input wire dbg_sbus_vld, output wire dbg_sbus_rdy, output wire dbg_sbus_err, - input wire [31:0] dbg_sbus_wdata, - output wire [31:0] dbg_sbus_rdata, + input wire [W_DATA-1:0] dbg_sbus_wdata, + output wire [W_DATA-1:0] dbg_sbus_rdata, // Level-sensitive interrupt sources input wire [NUM_IRQ-1:0] irq, // -> mip.meip @@ -111,7 +111,6 @@ wire core_hwrite_d; wire [W_DATA-1:0] core_wdata_d; wire [W_DATA-1:0] core_rdata_d; - hazard3_core #( `include "hazard3_config_inst.vh" ) core ( @@ -230,6 +229,7 @@ assign {bus_gnt_d, bus_gnt_s} = core_aph_req_d ? 2'b10 : dbg_sbus_vld && !bus_active_dph_s ? 2'b01 : 2'b00 ; + always @ (posedge clk or negedge rst_n) begin if (!rst_n) begin bus_active_dph_d <= 1'b0; @@ -242,10 +242,10 @@ end assign d_htrans = bus_gnt_d || bus_gnt_s ? HTRANS_NSEQ : HTRANS_IDLE; -assign d_haddr = bus_gnt_s ? dbg_sbus_addr : core_haddr_d; -assign d_hwrite = bus_gnt_s ? dbg_sbus_write : core_hwrite_d; -assign d_hsize = bus_gnt_s ? dbg_sbus_size : core_hsize_d; -assign d_hexcl = bus_gnt_s ? 1'b0 : core_aph_excl_d; +assign d_haddr = bus_gnt_s ? dbg_sbus_addr : core_haddr_d; +assign d_hwrite = bus_gnt_s ? dbg_sbus_write : core_hwrite_d; +assign d_hsize = bus_gnt_s ? {1'b0, dbg_sbus_size} : core_hsize_d; +assign d_hexcl = bus_gnt_s ? 1'b0 : core_aph_excl_d; assign d_hprot = { 2'b00, // Noncacheable/nonbufferable diff --git a/test/formal/bus_compliance_1port/tb.f b/test/formal/bus_compliance_1port/tb.f index c901c4e..6fd87e6 100644 --- a/test/formal/bus_compliance_1port/tb.f +++ b/test/formal/bus_compliance_1port/tb.f @@ -1,4 +1,5 @@ file tb.v file ../common/ahbl_slave_assumptions.v file ../common/ahbl_master_assertions.v +file ../common/sbus_assumptions.v list $HDL/hazard3.f diff --git a/test/formal/bus_compliance_2port/tb.f b/test/formal/bus_compliance_2port/tb.f index c901c4e..6fd87e6 100644 --- a/test/formal/bus_compliance_2port/tb.f +++ b/test/formal/bus_compliance_2port/tb.f @@ -1,4 +1,5 @@ file tb.v file ../common/ahbl_slave_assumptions.v file ../common/ahbl_master_assertions.v +file ../common/sbus_assumptions.v list $HDL/hazard3.f diff --git a/test/formal/bus_compliance_2port/tb.v b/test/formal/bus_compliance_2port/tb.v index 325cdac..a6e83f4 100644 --- a/test/formal/bus_compliance_2port/tb.v +++ b/test/formal/bus_compliance_2port/tb.v @@ -53,6 +53,15 @@ localparam W_DATA = 32; (* keep *) wire dbg_instr_caught_exception; (* keep *) wire dbg_instr_caught_ebreak; +(*keep*) wire [31:0] dbg_sbus_addr; +(*keep*) wire dbg_sbus_write; +(*keep*) wire [1:0] dbg_sbus_size; +(*keep*) wire dbg_sbus_vld; +(*keep*) wire dbg_sbus_rdy; +(*keep*) wire dbg_sbus_err; +(*keep*) wire [31:0] dbg_sbus_wdata; +(*keep*) wire [31:0] dbg_sbus_rdata; + (* keep *) wire [31:0] irq; (* keep *) wire soft_irq; (* keep *) wire timer_irq; @@ -101,6 +110,15 @@ hazard3_cpu_2port dut ( .dbg_instr_caught_exception (dbg_instr_caught_exception), .dbg_instr_caught_ebreak (dbg_instr_caught_ebreak), + .dbg_sbus_addr (dbg_sbus_addr), + .dbg_sbus_write (dbg_sbus_write), + .dbg_sbus_size (dbg_sbus_size), + .dbg_sbus_vld (dbg_sbus_vld), + .dbg_sbus_rdy (dbg_sbus_rdy), + .dbg_sbus_err (dbg_sbus_err), + .dbg_sbus_wdata (dbg_sbus_wdata), + .dbg_sbus_rdata (dbg_sbus_rdata), + .irq (irq), .soft_irq (soft_irq), .timer_irq (timer_irq) @@ -195,4 +213,18 @@ ahbl_master_assertions d_assertions ( .src_hrdata (d_hrdata) ); +sbus_assumptions sbus_assumptions ( + .clk (clk), + .rst_n (rst_n), + + .dbg_sbus_addr (dbg_sbus_addr), + .dbg_sbus_write (dbg_sbus_write), + .dbg_sbus_size (dbg_sbus_size), + .dbg_sbus_vld (dbg_sbus_vld), + .dbg_sbus_rdy (dbg_sbus_rdy), + .dbg_sbus_err (dbg_sbus_err), + .dbg_sbus_wdata (dbg_sbus_wdata), + .dbg_sbus_rdata (dbg_sbus_rdata) +); + endmodule diff --git a/test/formal/common/ahbl_master_assertions.v b/test/formal/common/ahbl_master_assertions.v index 86e34cd..0e272f8 100644 --- a/test/formal/common/ahbl_master_assertions.v +++ b/test/formal/common/ahbl_master_assertions.v @@ -1,5 +1,5 @@ /*****************************************************************************\ -| Copyright (C) 2021 Luke Wren | +| Copyright (C) 2021-2022 Luke Wren | | SPDX-License-Identifier: Apache-2.0 | \*****************************************************************************/ diff --git a/test/formal/common/ahbl_slave_assumptions.v b/test/formal/common/ahbl_slave_assumptions.v index a80e597..3188597 100644 --- a/test/formal/common/ahbl_slave_assumptions.v +++ b/test/formal/common/ahbl_slave_assumptions.v @@ -1,5 +1,5 @@ /*****************************************************************************\ -| Copyright (C) 2021 Luke Wren | +| Copyright (C) 2021-2022 Luke Wren | | SPDX-License-Identifier: Apache-2.0 | \*****************************************************************************/ diff --git a/test/formal/common/sbus_assumptions.v b/test/formal/common/sbus_assumptions.v new file mode 100644 index 0000000..bf749e1 --- /dev/null +++ b/test/formal/common/sbus_assumptions.v @@ -0,0 +1,52 @@ +/*****************************************************************************\ +| Copyright (C) 2022 Luke Wren | +| SPDX-License-Identifier: Apache-2.0 | +\*****************************************************************************/ + +// Properties for driving the debug module system bus access patch-through +// core interface in the bus property checks + +`default_nettype none + +module sbus_assumptions #( + parameter W_ADDR = 32, + parameter W_DATA = 32 +) ( + input wire clk, + input wire rst_n, + + input wire [W_ADDR-1:0] dbg_sbus_addr, + input wire dbg_sbus_write, + input wire [1:0] dbg_sbus_size, + input wire dbg_sbus_vld, + input wire dbg_sbus_rdy, + input wire dbg_sbus_err, + input wire [W_DATA-1:0] dbg_sbus_wdata, + input wire [W_DATA-1:0] dbg_sbus_rdata +); + +// Naturally aligned, no larger than bus +always assume(~|(dbg_sbus_addr & ~({32{1'b1}} << dbg_sbus_size))); +always assume(dbg_sbus_size < 2'h3); + +// No transfers whilst core is in reset +always assume(!(!rst_n && dbg_sbus_vld)); + +// No change or retraction of active transfer +always @ (posedge clk) if (rst_n) begin + if ($past(dbg_sbus_vld && !dbg_sbus_rdy)) begin + assume($stable({ + dbg_sbus_vld, + dbg_sbus_addr, + dbg_sbus_size, + dbg_sbus_write, + dbg_sbus_wdata + })); + end +end + +endmodule + +`ifndef YOSYS +`default_nettype wire +`endif diff --git a/test/sim/tb_cxxrtl/tb_multicore.v b/test/sim/tb_cxxrtl/tb_multicore.v index 35f4129..5345f4a 100644 --- a/test/sim/tb_cxxrtl/tb_multicore.v +++ b/test/sim/tb_cxxrtl/tb_multicore.v @@ -124,6 +124,15 @@ wire [N_HARTS-1:0] hart_instr_data_rdy; wire [N_HARTS-1:0] hart_instr_caught_exception; wire [N_HARTS-1:0] hart_instr_caught_ebreak; +wire [31:0] sbus_addr; +wire sbus_write; +wire [1:0] sbus_size; +wire sbus_vld; +wire sbus_rdy; +wire sbus_err; +wire [31:0] sbus_wdata; +wire [31:0] sbus_rdata; + hazard3_dm #( .N_HARTS (N_HARTS), .NEXT_DM_ADDR (0) @@ -159,7 +168,17 @@ hazard3_dm #( .hart_instr_data_vld (hart_instr_data_vld), .hart_instr_data_rdy (hart_instr_data_rdy), .hart_instr_caught_exception (hart_instr_caught_exception), - .hart_instr_caught_ebreak (hart_instr_caught_ebreak) + .hart_instr_caught_ebreak (hart_instr_caught_ebreak), + + .sbus_addr (sbus_addr), + .sbus_write (sbus_write), + .sbus_size (sbus_size), + .sbus_vld (sbus_vld), + .sbus_rdy (sbus_rdy), + .sbus_err (sbus_err), + .sbus_wdata (sbus_wdata), + .sbus_rdata (sbus_rdata) + ); // Generate resynchronised reset for CPU based on upstream reset and @@ -227,6 +246,16 @@ hazard3_cpu_1port #( .dbg_instr_caught_exception (hart_instr_caught_exception[0]), .dbg_instr_caught_ebreak (hart_instr_caught_ebreak [0]), + // SBA is routed through core 1, so tie off on core 0 + .dbg_sbus_addr (32'h0), + .dbg_sbus_write (1'b0), + .dbg_sbus_size (2'h0), + .dbg_sbus_vld (1'b0), + .dbg_sbus_rdy (), + .dbg_sbus_err (), + .dbg_sbus_wdata (32'h0), + .dbg_sbus_rdata (), + .irq (irq), .soft_irq (soft_irq[0]), .timer_irq (timer_irq) @@ -270,6 +299,15 @@ hazard3_cpu_1port #( .dbg_instr_caught_exception (hart_instr_caught_exception[1]), .dbg_instr_caught_ebreak (hart_instr_caught_ebreak [1]), + .dbg_sbus_addr (sbus_addr), + .dbg_sbus_write (sbus_write), + .dbg_sbus_size (sbus_size), + .dbg_sbus_vld (sbus_vld), + .dbg_sbus_rdy (sbus_rdy), + .dbg_sbus_err (sbus_err), + .dbg_sbus_wdata (sbus_wdata), + .dbg_sbus_rdata (sbus_rdata), + .irq (irq), .soft_irq (soft_irq[1]), .timer_irq (timer_irq)