From cd3125b6e508f12d1b9001a690152ffcae4ae334 Mon Sep 17 00:00:00 2001 From: Luke Wren Date: Fri, 27 May 2022 21:48:45 +0100 Subject: [PATCH] Add new bus signals on instruction_fetch_match/tb.v --- test/formal/instruction_fetch_match/tb.v | 140 +++++++++++++++-------- 1 file changed, 92 insertions(+), 48 deletions(-) diff --git a/test/formal/instruction_fetch_match/tb.v b/test/formal/instruction_fetch_match/tb.v index e66dc89..4a97f28 100644 --- a/test/formal/instruction_fetch_match/tb.v +++ b/test/formal/instruction_fetch_match/tb.v @@ -11,61 +11,101 @@ always @ (posedge clk) // ---------------------------------------------------------------------------- // DUT -(* keep *) wire [31:0] i_haddr; -(* keep *) wire i_hwrite; -(* keep *) wire [1:0] i_htrans; -(* keep *) wire [2:0] i_hsize; -(* keep *) wire [2:0] i_hburst; -(* keep *) wire [3:0] i_hprot; -(* keep *) wire i_hmastlock; -(* keep *) wire i_hready; -(* keep *) wire i_hresp; -(* keep *) wire [31:0] i_hwdata; -(* keep *) wire [31:0] i_hrdata; +(* keep *) wire [31:0] i_haddr; +(* keep *) wire i_hwrite; +(* keep *) wire [1:0] i_htrans; +(* keep *) wire [2:0] i_hsize; +(* keep *) wire [2:0] i_hburst; +(* keep *) wire [3:0] i_hprot; +(* keep *) wire i_hmastlock; +(* keep *) wire i_hready; +(* keep *) wire i_hresp; +(* keep *) wire [31:0] i_hwdata; +(* keep *) wire [31:0] i_hrdata; -(* keep *) wire [31:0] d_haddr; -(* keep *) wire d_hwrite; -(* keep *) wire [1:0] d_htrans; -(* keep *) wire [2:0] d_hsize; -(* keep *) wire [2:0] d_hburst; -(* keep *) wire [3:0] d_hprot; -(* keep *) wire d_hmastlock; -(* keep *) wire d_hready; -(* keep *) wire d_hresp; -(* keep *) wire [31:0] d_hwdata; -(* keep *) wire [31:0] d_hrdata; +(* keep *) wire [31:0] d_haddr; +(* keep *) wire d_hwrite; +(* keep *) wire [1:0] d_htrans; +(* keep *) wire [2:0] d_hsize; +(* keep *) wire [2:0] d_hburst; +(* keep *) wire [3:0] d_hprot; +(* keep *) wire d_hmastlock; +(* keep *) wire d_hexcl; +(* keep *) wire d_hready; +(* keep *) wire d_hresp; +(* keep *) wire d_hexokay; +(* keep *) wire [31:0] d_hwdata; +(* keep *) wire [31:0] d_hrdata; -(* keep *) reg [15:0] irq; +localparam W_DATA = 32; + +// Don't allow debug, as this breaks the CIR == mem[PC] invariant that we're trying to test. +(* keep *) wire dbg_req_halt = 1'b0; +(* keep *) wire dbg_req_halt_on_reset = 1'b0; +(* keep *) wire dbg_req_resume = 1'b0; + +(* keep *) wire dbg_halted; +(* keep *) wire dbg_running; +(* keep *) wire [W_DATA-1:0] dbg_data0_rdata; +(* keep *) wire [W_DATA-1:0] dbg_data0_wdata; +(* keep *) wire dbg_data0_wen; +(* keep *) wire [W_DATA-1:0] dbg_instr_data; +(* keep *) wire dbg_instr_data_vld; +(* keep *) wire dbg_instr_data_rdy; +(* keep *) wire dbg_instr_caught_exception; +(* keep *) wire dbg_instr_caught_ebreak; + +(* keep *) wire [31:0] irq; +(* keep *) wire soft_irq; +(* keep *) wire timer_irq; hazard3_cpu_2port dut ( - .clk (clk), - .rst_n (rst_n), + .clk (clk), + .rst_n (rst_n), - .i_haddr (i_haddr), - .i_hwrite (i_hwrite), - .i_htrans (i_htrans), - .i_hsize (i_hsize), - .i_hburst (i_hburst), - .i_hprot (i_hprot), - .i_hmastlock (i_hmastlock), - .i_hready (i_hready), - .i_hresp (i_hresp), - .i_hwdata (i_hwdata), - .i_hrdata (i_hrdata), + .i_haddr (i_haddr), + .i_hwrite (i_hwrite), + .i_htrans (i_htrans), + .i_hsize (i_hsize), + .i_hburst (i_hburst), + .i_hprot (i_hprot), + .i_hmastlock (i_hmastlock), + .i_hready (i_hready), + .i_hresp (i_hresp), + .i_hwdata (i_hwdata), + .i_hrdata (i_hrdata), - .d_haddr (d_haddr), - .d_hwrite (d_hwrite), - .d_htrans (d_htrans), - .d_hsize (d_hsize), - .d_hburst (d_hburst), - .d_hprot (d_hprot), - .d_hmastlock (d_hmastlock), - .d_hready (d_hready), - .d_hresp (d_hresp), - .d_hwdata (d_hwdata), - .d_hrdata (d_hrdata), + .d_haddr (d_haddr), + .d_hwrite (d_hwrite), + .d_htrans (d_htrans), + .d_hsize (d_hsize), + .d_hburst (d_hburst), + .d_hprot (d_hprot), + .d_hmastlock (d_hmastlock), + .d_hexcl (d_hexcl), + .d_hready (d_hready), + .d_hresp (d_hresp), + .d_hexokay (d_hexokay), + .d_hwdata (d_hwdata), + .d_hrdata (d_hrdata), - .irq (irq) + .dbg_req_halt (dbg_req_halt), + .dbg_req_halt_on_reset (dbg_req_halt_on_reset), + .dbg_req_resume (dbg_req_resume), + .dbg_halted (dbg_halted), + .dbg_running (dbg_running), + .dbg_data0_rdata (dbg_data0_rdata), + .dbg_data0_wdata (dbg_data0_wdata), + .dbg_data0_wen (dbg_data0_wen), + .dbg_instr_data (dbg_instr_data), + .dbg_instr_data_vld (dbg_instr_data_vld), + .dbg_instr_data_rdy (dbg_instr_data_rdy), + .dbg_instr_caught_exception (dbg_instr_caught_exception), + .dbg_instr_caught_ebreak (dbg_instr_caught_ebreak), + + .irq (irq), + .soft_irq (soft_irq), + .timer_irq (timer_irq) ); // ---------------------------------------------------------------------------- @@ -83,6 +123,7 @@ ahbl_slave_assumptions #( .dst_hready_resp (i_hready), .dst_hready (i_hready), .dst_hresp (i_hresp), + .dst_hexokay (1'b0), .dst_haddr (i_haddr), .dst_hwrite (i_hwrite), .dst_htrans (i_htrans), @@ -90,6 +131,7 @@ ahbl_slave_assumptions #( .dst_hburst (i_hburst), .dst_hprot (i_hprot), .dst_hmastlock (i_hmastlock), + .dst_hexcl (1'b0), .dst_hwdata (i_hwdata), .dst_hrdata (i_hrdata) ); @@ -103,6 +145,7 @@ ahbl_slave_assumptions #( .dst_hready_resp (d_hready), .dst_hready (d_hready), .dst_hresp (d_hresp), + .dst_hexokay (d_hexokay), .dst_haddr (d_haddr), .dst_hwrite (d_hwrite), .dst_htrans (d_htrans), @@ -110,6 +153,7 @@ ahbl_slave_assumptions #( .dst_hburst (d_hburst), .dst_hprot (d_hprot), .dst_hmastlock (d_hmastlock), + .dst_hexcl (d_hexcl), .dst_hwdata (d_hwdata), .dst_hrdata (d_hrdata) );