diff --git a/hdl/hazard3_core.v b/hdl/hazard3_core.v index 36e4446..d48d080 100644 --- a/hdl/hazard3_core.v +++ b/hdl/hazard3_core.v @@ -470,6 +470,9 @@ always @ (posedge clk) if (rst_n) begin // Neither of these are write-address-phase. if (x_amo_phase == 3'h4) assert($past(x_amo_phase) != 3'h2); + // Make sure M is unstalled for passing store data through in phase 2 + if (x_amo_phase == 3'h2) + assert(!m_stall); end `endif @@ -769,6 +772,14 @@ always @ (posedge clk or negedge rst_n) begin end end +`ifdef FORMAL +always @ (posedge clk) if (rst_n) begin + // D bus errors must always squash younger load/stores + if ($past(bus_dph_err_d && !bus_dph_ready_d)) + assert(!bus_aph_req_d); +end +`endif + // Datapath flops always @ (posedge clk or negedge rst_n) begin if (!rst_n) begin diff --git a/hdl/hazard3_cpu_1port.v b/hdl/hazard3_cpu_1port.v index af0a91d..f4019d0 100644 --- a/hdl/hazard3_cpu_1port.v +++ b/hdl/hazard3_cpu_1port.v @@ -152,7 +152,7 @@ always @ (posedge clk or negedge rst_n) begin bus_hold_aph <= 1'b0; bus_gnt_id_prev <= 2'h0; end else begin - bus_hold_aph <= ahblm_htrans[1] && !ahblm_hready; + bus_hold_aph <= ahblm_htrans[1] && !ahblm_hready && !ahblm_hresp; bus_gnt_id_prev <= {bus_gnt_i, bus_gnt_d}; end end diff --git a/test/formal/bus_compliance_1port/Makefile b/test/formal/bus_compliance_1port/Makefile new file mode 100644 index 0000000..29d7a87 --- /dev/null +++ b/test/formal/bus_compliance_1port/Makefile @@ -0,0 +1,8 @@ +DOTF=tb.f +TOP=tb +YOSYS_SMT_SOLVER=z3 +DEPTH=25 + +all: bmc + +include $(SCRIPTS)/formal.mk diff --git a/test/formal/bus_compliance_1port/tb.f b/test/formal/bus_compliance_1port/tb.f new file mode 100644 index 0000000..c901c4e --- /dev/null +++ b/test/formal/bus_compliance_1port/tb.f @@ -0,0 +1,4 @@ +file tb.v +file ../common/ahbl_slave_assumptions.v +file ../common/ahbl_master_assertions.v +list $HDL/hazard3.f diff --git a/test/formal/bus_compliance_1port/tb.v b/test/formal/bus_compliance_1port/tb.v new file mode 100644 index 0000000..b8e31dd --- /dev/null +++ b/test/formal/bus_compliance_1port/tb.v @@ -0,0 +1,132 @@ +// Assume bus responses are well-formed, assert that bus requests are +// well-formed. + +module tb; + +reg clk; +reg rst_n = 1'b0; +always @ (posedge clk) + rst_n <= 1'b1; + +// ---------------------------------------------------------------------------- +// DUT + +(* keep *) wire [31:0] ahblm_haddr; +(* keep *) wire ahblm_hwrite; +(* keep *) wire ahblm_hexcl; +(* keep *) wire [1:0] ahblm_htrans; +(* keep *) wire [2:0] ahblm_hsize; +(* keep *) wire [2:0] ahblm_hburst; +(* keep *) wire [3:0] ahblm_hprot; +(* keep *) wire ahblm_hmastlock; +(* keep *) wire ahblm_hready; +(* keep *) wire ahblm_hexokay; +(* keep *) wire ahblm_hresp; +(* keep *) wire [31:0] ahblm_hwdata; +(* keep *) wire [31:0] ahblm_hrdata; + +localparam W_DATA = 32; + +(* keep *) wire dbg_req_halt; +(* keep *) wire dbg_req_halt_on_reset; +(* keep *) wire dbg_req_resume; +(* 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_1port dut ( + .clk (clk), + .rst_n (rst_n), + + .ahblm_haddr (ahblm_haddr), + .ahblm_hwrite (ahblm_hwrite), + .ahblm_hexcl (ahblm_hexcl), + .ahblm_htrans (ahblm_htrans), + .ahblm_hsize (ahblm_hsize), + .ahblm_hburst (ahblm_hburst), + .ahblm_hprot (ahblm_hprot), + .ahblm_hmastlock (ahblm_hmastlock), + .ahblm_hready (ahblm_hready), + .ahblm_hexokay (ahblm_hexokay), + .ahblm_hresp (ahblm_hresp), + .ahblm_hwdata (ahblm_hwdata), + .ahblm_hrdata (ahblm_hrdata), + + .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) +); + +// ---------------------------------------------------------------------------- +// Bus properties + +// -1 -> unconstrained, >=0 -> max length +localparam MAX_BUS_STALL = -1; + +ahbl_slave_assumptions #( + .MAX_BUS_STALL (MAX_BUS_STALL) +) d_assumptions ( + .clk (clk), + .rst_n (rst_n), + + .dst_hready_resp (ahblm_hready), + .dst_hready (ahblm_hready), + .dst_hresp (ahblm_hresp), + .dst_hexokay (ahblm_hexokay), + .dst_haddr (ahblm_haddr), + .dst_hwrite (ahblm_hwrite), + .dst_htrans (ahblm_htrans), + .dst_hsize (ahblm_hsize), + .dst_hburst (ahblm_hburst), + .dst_hprot (ahblm_hprot), + .dst_hmastlock (ahblm_hmastlock), + .dst_hexcl (ahblm_hexcl), + .dst_hwdata (ahblm_hwdata), + .dst_hrdata (ahblm_hrdata) +); + +ahbl_master_assertions d_assertions ( + .clk (clk), + .rst_n (rst_n), + + .src_hready (ahblm_hready), + .src_hresp (ahblm_hresp), + .src_hexokay (ahblm_hexokay), + .src_haddr (ahblm_haddr), + .src_hwrite (ahblm_hwrite), + .src_htrans (ahblm_htrans), + .src_hsize (ahblm_hsize), + .src_hburst (ahblm_hburst), + .src_hprot (ahblm_hprot), + .src_hmastlock (ahblm_hmastlock), + .src_hexcl (ahblm_hexcl), + .src_hwdata (ahblm_hwdata), + .src_hrdata (ahblm_hrdata) +); + +endmodule diff --git a/test/formal/bus_compliance_2port/Makefile b/test/formal/bus_compliance_2port/Makefile index 254b0e0..29d7a87 100644 --- a/test/formal/bus_compliance_2port/Makefile +++ b/test/formal/bus_compliance_2port/Makefile @@ -1,6 +1,6 @@ DOTF=tb.f TOP=tb -YOSYS_SMT_SOLVER=boolector +YOSYS_SMT_SOLVER=z3 DEPTH=25 all: bmc diff --git a/test/formal/bus_compliance_2port/tb.v b/test/formal/bus_compliance_2port/tb.v index 3d9e21b..325cdac 100644 --- a/test/formal/bus_compliance_2port/tb.v +++ b/test/formal/bus_compliance_2port/tb.v @@ -53,7 +53,9 @@ localparam W_DATA = 32; (* keep *) wire dbg_instr_caught_exception; (* keep *) wire dbg_instr_caught_ebreak; -(* keep *) wire [15:0] irq; +(* keep *) wire [31:0] irq; +(* keep *) wire soft_irq; +(* keep *) wire timer_irq; hazard3_cpu_2port dut ( .clk (clk), @@ -99,7 +101,9 @@ hazard3_cpu_2port dut ( .dbg_instr_caught_exception (dbg_instr_caught_exception), .dbg_instr_caught_ebreak (dbg_instr_caught_ebreak), - .irq (irq) + .irq (irq), + .soft_irq (soft_irq), + .timer_irq (timer_irq) ); // ---------------------------------------------------------------------------- diff --git a/test/formal/common/ahbl_master_assertions.v b/test/formal/common/ahbl_master_assertions.v index db46f53..86e34cd 100644 --- a/test/formal/common/ahbl_master_assertions.v +++ b/test/formal/common/ahbl_master_assertions.v @@ -64,7 +64,7 @@ always @ (posedge clk) if (rst_n) begin: dst_ahbl_req_properties // HSIZE appropriate for bus width assert(8 << src_hsize <= W_DATA); // No deassertion or change of active request - if ($past(src_htrans[1] && !src_hready)) begin + if ($past(src_htrans[1] && !src_hready && !src_hresp)) begin assert($stable({ src_htrans, src_hwrite, diff --git a/test/formal/instruction_fetch_match/Makefile b/test/formal/instruction_fetch_match/Makefile index 1c937e6..059f772 100644 --- a/test/formal/instruction_fetch_match/Makefile +++ b/test/formal/instruction_fetch_match/Makefile @@ -1,6 +1,6 @@ DOTF=tb.f TOP=tb -YOSYS_SMT_SOLVER=boolector +YOSYS_SMT_SOLVER=z3 DEFINES=HAZARD3_FORMAL_REGRESSION include $(SCRIPTS)/formal.mk