From 12205f12c7e23888c4c07edc1713068e5d1ac47d Mon Sep 17 00:00:00 2001 From: Luke Wren Date: Sun, 30 May 2021 11:22:36 +0100 Subject: [PATCH] Add instruction fetch match check --- .../formal/instruction_fetch_match/.gitignore | 1 + test/formal/instruction_fetch_match/Makefile | 6 + test/formal/instruction_fetch_match/disasm.py | 14 +++ .../hazard3_formal_regression.vh | 66 ++++++++++ test/formal/instruction_fetch_match/tb.f | 4 + test/formal/instruction_fetch_match/tb.v | 117 ++++++++++++++++++ 6 files changed, 208 insertions(+) create mode 100644 test/formal/instruction_fetch_match/.gitignore create mode 100644 test/formal/instruction_fetch_match/Makefile create mode 100755 test/formal/instruction_fetch_match/disasm.py create mode 100644 test/formal/instruction_fetch_match/hazard3_formal_regression.vh create mode 100644 test/formal/instruction_fetch_match/tb.f create mode 100644 test/formal/instruction_fetch_match/tb.v diff --git a/test/formal/instruction_fetch_match/.gitignore b/test/formal/instruction_fetch_match/.gitignore new file mode 100644 index 0000000..c9e55a7 --- /dev/null +++ b/test/formal/instruction_fetch_match/.gitignore @@ -0,0 +1 @@ +disasm.s diff --git a/test/formal/instruction_fetch_match/Makefile b/test/formal/instruction_fetch_match/Makefile new file mode 100644 index 0000000..1c937e6 --- /dev/null +++ b/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 diff --git a/test/formal/instruction_fetch_match/disasm.py b/test/formal/instruction_fetch_match/disasm.py new file mode 100755 index 0000000..c1938d3 --- /dev/null +++ b/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") diff --git a/test/formal/instruction_fetch_match/hazard3_formal_regression.vh b/test/formal/instruction_fetch_match/hazard3_formal_regression.vh new file mode 100644 index 0000000..3f80aba --- /dev/null +++ b/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 + + diff --git a/test/formal/instruction_fetch_match/tb.f b/test/formal/instruction_fetch_match/tb.f new file mode 100644 index 0000000..8debe7b --- /dev/null +++ b/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 . diff --git a/test/formal/instruction_fetch_match/tb.v b/test/formal/instruction_fetch_match/tb.v new file mode 100644 index 0000000..e66dc89 --- /dev/null +++ b/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