Add instruction fetch match check

test/formal/instruction_fetch_match/.gitignore

@@ -0,0 +1 @@
+disasm.s

test/formal/instruction_fetch_match/Makefile

@@ -0,0 +1,6 @@
+DOTF=tb.f
+TOP=tb
+YOSYS_SMT_SOLVER=boolector
+DEFINES=HAZARD3_FORMAL_REGRESSION
+
+include $(SCRIPTS)/formal.mk

test/formal/instruction_fetch_match/disasm.py

@@ -0,0 +1,14 @@
+#!/usr/bin/env python3
+
+from os import system
+
+prog = []
+for l in open("bmc.log"):
+	if "Value for anyconst in tb.dut.core" in l:
+		prog.append(l.split(" ")[-1])
+with open("disasm.s", "w") as f:
+	for instr in prog:
+		f.write(f".word {instr}")
+
+system("riscv32-unknown-elf-gcc -c disasm.s")
+system("riscv32-unknown-elf-objdump -d -M numeric,no-aliases disasm.o")

test/formal/instruction_fetch_match/hazard3_formal_regression.vh

@@ -0,0 +1,66 @@
+// This file is included at the bottom of hazard3_core.v to provide internal
+// assertions. Here we are:
+//
+// - Attaching a memory with arbitrary constant contents to the instruction
+//   fetch port
+// - Asserting that, when CIR is valid, CIR contents matches the memory value
+//   at PC
+
+localparam MEM_SIZE_BYTES = 64;
+
+reg [31:0] instr_mem [0:MEM_SIZE_BYTES-1];
+reg [31:0] garbage;
+
+always @ (*) begin: constrain_mem_const
+	integer i;
+	for (i = 0; i < MEM_SIZE_BYTES / 4; i = i + 1)
+		assume(instr_mem[i] == $anyconst);
+end
+
+reg        dph_i_active;
+reg [2:0]  dph_i_size;
+reg [31:0] dph_i_addr;
+reg [31:0] dph_rdata_unmasked;
+
+always @ (posedge clk or negedge rst_n) begin
+	if (!rst_n) begin
+		dph_i_active <= 1'b0;
+		dph_i_size <= 3'd0;
+		dph_i_addr <= 32'h0;
+		dph_rdata_unmasked <= 32'h0;
+	end else if (bus_aph_ready_i) begin
+		dph_i_active <= bus_aph_req_i;
+		dph_i_size <= bus_hsize_i;
+		dph_i_addr <= bus_haddr_i;
+		if (bus_haddr_i < MEM_SIZE_BYTES)
+			dph_rdata_unmasked <= instr_mem[bus_haddr_i / 4];
+		else
+			dph_rdata_unmasked <= garbage;
+	end
+end
+
+always @ (*) begin: connect_rdata
+	integer i;
+	for (i = 0; i < 4; i = i + 1) begin
+		if (bus_dph_ready_i && i >= (dph_i_addr & 32'h3) && i < (dph_i_addr & 32'h3) + (32'd1 << dph_i_size))
+			assume(bus_rdata_i[i * 8 +: 8] == dph_rdata_unmasked[i * 8 +: 8]);
+		else
+			assume(bus_rdata_i == 8'h0);
+	end
+end
+
+always assume(d_pc < MEM_SIZE_BYTES);
+
+
+wire [31:0] expect_cir;
+assign expect_cir[15:0 ] = instr_mem[ d_pc      / 4] >> (d_pc[1] ? 16 : 0 );
+assign expect_cir[31:16] = instr_mem[(d_pc + 2) / 4] >> (d_pc[1] ? 0  : 16);
+
+always @ (posedge clk) if (rst_n) begin
+	if (fd_cir_vld >= 2'd1)
+		assert(fd_cir[15:0] == expect_cir[15:0]);
+	if (fd_cir_vld >= 2'd2 && d_pc <= MEM_SIZE_BYTES - 4)
+		assert(fd_cir[31:16] == expect_cir[31:16]);
+end
+
+

test/formal/instruction_fetch_match/tb.f

@@ -0,0 +1,4 @@
+file tb.v
+file ../common/ahbl_slave_assumptions.v
+list $HDL/hazard3.f
+include .

test/formal/instruction_fetch_match/tb.v

@@ -0,0 +1,117 @@
+// Just instantiate the DUT and constrain error/stall responses to be
+// sensible. Properties are hooked up inside the processor.
+
+module tb;
+
+reg clk;
+reg rst_n = 1'b0;
+always @ (posedge clk)
+	rst_n <= 1'b1;
+
+// ----------------------------------------------------------------------------
+// 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]  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 *) reg  [15:0]  irq;
+
+hazard3_cpu_2port dut (
+	.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),
+
+	.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),
+
+	.irq          (irq)
+);
+
+// ----------------------------------------------------------------------------
+// Bus properties
+
+// -1 -> unconstrained, >=0 -> max length
+localparam MAX_BUS_STALL = -1;
+
+ahbl_slave_assumptions #(
+	.MAX_BUS_STALL (MAX_BUS_STALL)
+) i_assumptions (
+	.clk             (clk),
+	.rst_n           (rst_n),
+
+	.dst_hready_resp (i_hready),
+	.dst_hready      (i_hready),
+	.dst_hresp       (i_hresp),
+	.dst_haddr       (i_haddr),
+	.dst_hwrite      (i_hwrite),
+	.dst_htrans      (i_htrans),
+	.dst_hsize       (i_hsize),
+	.dst_hburst      (i_hburst),
+	.dst_hprot       (i_hprot),
+	.dst_hmastlock   (i_hmastlock),
+	.dst_hwdata      (i_hwdata),
+	.dst_hrdata      (i_hrdata)
+);
+
+ahbl_slave_assumptions #(
+	.MAX_BUS_STALL (MAX_BUS_STALL)
+) d_assumptions (
+	.clk             (clk),
+	.rst_n           (rst_n),
+
+	.dst_hready_resp (d_hready),
+	.dst_hready      (d_hready),
+	.dst_hresp       (d_hresp),
+	.dst_haddr       (d_haddr),
+	.dst_hwrite      (d_hwrite),
+	.dst_htrans      (d_htrans),
+	.dst_hsize       (d_hsize),
+	.dst_hburst      (d_hburst),
+	.dst_hprot       (d_hprot),
+	.dst_hmastlock   (d_hmastlock),
+	.dst_hwdata      (d_hwdata),
+	.dst_hrdata      (d_hrdata)
+);
+
+endmodule