Add single-port bus compliance. Fix adapter not re-arbitrating following an ERROR response, causing a squashed younger load-store to remain presented to the bus.

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

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

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

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

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

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

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)
 );
 
 // ----------------------------------------------------------------------------

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,

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