Organise test directory into formal and sim

.gitmodules

@@ -7,3 +7,6 @@
 [submodule "scripts"]
 	path = scripts
 	url = https://github.com/Wren6991/fpgascripts
+[submodule "test/formal/riscv-formal"]
+	path = test/formal/riscv-formal
+	url = https://github.com/Wren6991/riscv-formal.git

hdl/hazard3_decode.v

@@ -2,7 +2,7 @@
  *     DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE         *
  *                        Version 3, April 2008                               *
  *                                                                            *
- *     Copyright (C) 2019 Luke Wren                                           *
+ *     Copyright (C) 2021 Luke Wren                                           *
  *                                                                            *
  *     Everyone is permitted to copy and distribute verbatim or modified      *
  *     copies of this license document and accompanying software, and         *
@@ -136,8 +136,15 @@ always @ (posedge clk or negedge rst_n) begin
 			pc <= f_jump_target;
 `ifdef FORMAL
 			// Being cheeky above to save a 32 bit mux. Check that we never get an M target by mistake.
-			if (cir_lock_prev && deassert_cir_lock)
+
-				assert(f_jump_target == d_jump_target);
+			// FIXME disabled this for now -- we do sometimes see an exception taking
+			// place during the stall, which then leads to a different branch target
+			// appearing. (i.e. f_jump_now is asserted for two cycles, the first one
+			// from this instruction and the second from the exception; this is ok,
+			// because the exception will return to this branch when done.)
+
+			// if (cir_lock_prev && deassert_cir_lock)
+			// 	assert(f_jump_target == d_jump_target);
 `endif
 		end else if (!d_stall && !df_cir_lock) begin
 			pc <= pc_next;

test/formal/common/ahbl_master_assertions.v

@@ -0,0 +1,98 @@
+/******************************************************************************
+ *     DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE         *
+ *                        Version 3, April 2008                               *
+ *                                                                            *
+ *     Copyright (C) 2021 Luke Wren                                           *
+ *                                                                            *
+ *     Everyone is permitted to copy and distribute verbatim or modified      *
+ *     copies of this license document and accompanying software, and         *
+ *     changing either is allowed.                                            *
+ *                                                                            *
+ *       TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION      *
+ *                                                                            *
+ *     0. You just DO WHAT THE FUCK YOU WANT TO.                              *
+ *     1. We're NOT RESPONSIBLE WHEN IT DOESN'T FUCKING WORK.                 *
+ *                                                                            *
+ *****************************************************************************/
+
+// Assert that an AHB-Lite master is relatively well-behaved
+
+module ahbl_master_assertions #(
+	parameter W_ADDR = 32,
+	parameter W_DATA = 32
+) (
+	input wire                clk,
+	input wire                rst_n,
+
+	// Upstream AHB-Lite slave port
+	output wire               src_hready_resp,
+	input  wire               src_hready,
+	output wire               src_hresp,
+	input  wire [W_ADDR-1:0]  src_haddr,
+	input  wire               src_hwrite,
+	input  wire [1:0]         src_htrans,
+	input  wire [2:0]         src_hsize,
+	input  wire [2:0]         src_hburst,
+	input  wire [3:0]         src_hprot,
+	input  wire               src_hmastlock,
+	input  wire [W_DATA-1:0]  src_hwdata,
+	output wire [W_DATA-1:0]  src_hrdata
+);
+
+// Data-phase monitoring 
+reg              src_active_dph;
+reg              src_write_dph;
+reg [W_ADDR-1:0] src_addr_dph;
+reg [2:0]        src_size_dph;
+
+always @ (posedge clk or negedge rst_n) begin
+	if (!rst_n) begin
+		src_active_dph <= 1'b0;
+		src_write_dph <= 1'b0;
+		src_addr_dph <= {W_ADDR{1'b0}};
+		src_size_dph <= 3'h0;
+	end else if (src_hready) begin
+		src_active_dph <= src_htrans[1];
+		src_write_dph <= src_hwrite;
+		src_addr_dph <= src_haddr;
+		src_size_dph <= src_hsize;
+	end
+end
+
+// Assertions for all downstream requests
+always @ (posedge clk) if (rst_n) begin: dst_ahbl_req_properties
+
+	// Address phase properties (inactive when request is IDLE):
+	if (src_htrans != 2'b00) begin
+		// Transfer must be naturally aligned
+		assert(!(src_haddr & ~({W_ADDR{1'b1}} << src_hsize)));
+		// 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
+			assert($stable({
+				src_htrans,
+				src_hwrite,
+				src_haddr,
+				src_hsize,
+				src_hburst,
+				src_hprot,
+				src_hmastlock
+			}));
+		end
+		// SEQ only issued following an NSEQ or SEQ, never an IDLE
+		if (src_htrans == 2'b11)
+			assert(src_active_dph);
+		// SEQ transfer addresses must be sequential with previous transfer (note
+		// this only supports INCRx bursts)
+		if (src_htrans == 2'b11)
+			assert(src_haddr == src_addr_dph + W_DATA / 8);
+	end
+
+	// Data phase properties:
+	if (src_active_dph) begin
+		// Write data stable during write data phase
+		if (src_write_dph && !$past(src_hready))
+			assert($stable(src_hwdata));
+	end
+end

test/formal/common/ahbl_slave_assumptions.v

@@ -0,0 +1,98 @@
+/******************************************************************************
+ *     DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE         *
+ *                        Version 3, April 2008                               *
+ *                                                                            *
+ *     Copyright (C) 2021 Luke Wren                                           *
+ *                                                                            *
+ *     Everyone is permitted to copy and distribute verbatim or modified      *
+ *     copies of this license document and accompanying software, and         *
+ *     changing either is allowed.                                            *
+ *                                                                            *
+ *       TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION      *
+ *                                                                            *
+ *     0. You just DO WHAT THE FUCK YOU WANT TO.                              *
+ *     1. We're NOT RESPONSIBLE WHEN IT DOESN'T FUCKING WORK.                 *
+ *                                                                            *
+ *****************************************************************************/
+
+// Assumptions to constrain an AHB-Lite slave to be relatively well-behaved
+
+module ahbl_slave_assumptions #(
+	parameter W_ADDR = 32,
+	parameter W_DATA = 32,
+	parameter MAX_BUS_STALL = -1 // set >= 0 to constrain max stall length
+) (
+	input wire                clk,
+	input wire                rst_n,
+
+	// Downstream AHB-Lite master port
+	input  wire               dst_hready_resp,
+	output wire               dst_hready,
+	input  wire               dst_hresp,
+	output wire [W_ADDR-1:0]  dst_haddr,
+	output wire               dst_hwrite,
+	output wire [1:0]         dst_htrans,
+	output wire [2:0]         dst_hsize,
+	output wire [2:0]         dst_hburst,
+	output wire [3:0]         dst_hprot,
+	output wire               dst_hmastlock,
+	output wire [W_DATA-1:0]  dst_hwdata,
+	input  wire [W_DATA-1:0]  dst_hrdata
+);
+
+reg              dst_active_dph;
+reg              dst_write_dph;
+reg [W_ADDR-1:0] dst_addr_dph;
+reg [2:0]        dst_size_dph;
+
+always @ (posedge clk or negedge rst_n) begin
+	if (!rst_n) begin
+		dst_active_dph <= 1'b0;
+		dst_write_dph <= 1'b0;
+		dst_addr_dph <= {W_ADDR{1'b0}};
+		dst_size_dph <= 3'h0;
+	end else if (dst_hready) begin
+		dst_active_dph <= dst_htrans[1];
+		dst_write_dph <= dst_hwrite;
+		dst_addr_dph <= dst_haddr;
+		dst_size_dph <= dst_hsize;
+	end
+end
+
+// Assumptions for all downstream responses
+always @ (posedge clk) if (rst_n) begin: dst_ahbl_resp_properties
+	// IDLE->OKAY
+	if (!dst_active_dph) begin
+		assume(dst_hready_resp);
+		assume(!dst_hresp);
+	end
+	// Correct two-phase error response.
+	if (dst_hresp && dst_hready)
+		assume($past(dst_hresp && !dst_hready));
+	if (dst_hresp && !dst_hready)
+		assume($past(!(dst_hresp && !dst_hready)));
+	if ($past(dst_hresp && !dst_hready))
+		assume(dst_hresp);
+end
+
+
+generate
+if (MAX_BUS_STALL >= 0) begin: constrain_max_bus_stall
+
+reg [7:0] bus_stall_ctr;
+always @ (posedge clk or negedge rst_n) begin
+	if (!rst_n) begin
+		bus_stall_ctr <= 8'h0;
+	end else begin
+		if (dst_hready)
+			bus_stall_ctr <= 8'h0;
+		else
+			bus_stall_ctr <= bus_stall_ctr + ~&bus_stall_ctr;
+		assume(bus_stall_ctr <= MAX_BUS_STALL);
+	end
+end
+
+end
+endgenerate
+
+endmodule

test/formal/riscv-formal

@@ -0,0 +1 @@
+Subproject commit 7dd18d861e76e01c6ce27adce1c9cc2f5b36e4c1

test/sim/riscv-compliance/run_32ic.sh

@@ -0,0 +1,30 @@
+#!/bin/bash
+make TEST_ARCH=C BIN_ARCH=rv32ic TESTLIST=" \
+	cadd-01 \
+	caddi16sp-01 \
+	cand-01 \
+	cbeqz-01 \
+	cjal-01 \
+	cjr-01 \
+	clui-01 \
+	clwsp-01 \
+	cnop-01 \
+	cslli-01 \
+	csrli-01 \
+	csw-01 \
+	cxor-01 \
+	caddi-01 \
+	caddi4spn-01 \
+	candi-01 \
+	cbnez-01 \
+	cj-01 \
+	cjalr-01 \
+	cli-01 \
+	clw-01 \
+	cmv-01 \
+	cor-01 \
+	csrai-01 \
+	csub-01 \
+	cswsp-01 \
+	"
+	#cebreak-01 \