Hazard3/test/formal/frontend_fetch_match/tb.v

// Instantiate frontend. Generate bus responses where data is a known function
// of addresses. Attach a dummy program counter which either increments
// sequentially or follows jump requests asserted to the frontend.
//
// Assert that CIR is always equal to mem[PC].
//
// This is similar to the instruction_fetch_match testcase, but struggles less
// with depth because only the frontend is present. This testcase also places
// fewer constraints (i.e. ones implicit in the processor) on the frontend,
// so may chase out some latent bugs.

`default_nettype none

module tb #(
`include "hazard3_config.vh"
);

reg clk;
reg rst_n = 1'b0;
always @ (posedge clk)
	rst_n <= 1'b1;

// ----------------------------------------------------------------------------
// DUT

(*keep*) wire              mem_size;
(*keep*) wire [31:0]       mem_addr;
(*keep*) wire              mem_priv;
(*keep*) wire              mem_addr_vld;
(*keep*) wire              mem_addr_rdy;
(*keep*) wire [31:0]       mem_data;
(*keep*) wire              mem_data_err;
(*keep*) wire              mem_data_vld;

(*keep*) wire [31:0]       jump_target;
(*keep*) wire              jump_priv;
(*keep*) wire              jump_target_vld;
(*keep*) wire              jump_target_rdy;

(*keep*) wire              btb_set;
(*keep*) wire [31:0]       btb_set_src_addr;
(*keep*) wire [31:0]       btb_set_target_addr;
(*keep*) wire              btb_clear;

(*keep*) wire [31:0]       cir;
(*keep*) wire [1:0]        cir_vld;
(*keep*) wire [1:0]        cir_use;
(*keep*) wire [1:0]        cir_err;
(*keep*) reg               cir_flush_behind;

(*keep*) wire [4:0]        predecode_rs1_coarse;
(*keep*) wire [4:0]        predecode_rs2_coarse;
(*keep*) wire [4:0]        predecode_rs1_fine;
(*keep*) wire [4:0]        predecode_rs2_fine;

(*keep*) wire              debug_mode;
(*keep*) wire [31:0]       dbg_instr_data;
(*keep*) wire              dbg_instr_data_vld;
(*keep*) wire              dbg_instr_data_rdy;


hazard3_frontend #(
`include "hazard3_config_inst.vh"
) dut (
	.clk                  (clk),
	.rst_n                (rst_n),

	.mem_size             (mem_size),
	.mem_addr             (mem_addr),
	.mem_priv             (mem_priv),
	.mem_addr_vld         (mem_addr_vld),
	.mem_addr_rdy         (mem_addr_rdy),
	.mem_data             (mem_data),
	.mem_data_err         (mem_data_err),
	.mem_data_vld         (mem_data_vld),

	.jump_target          (jump_target),
	.jump_priv            (jump_priv),
	.jump_target_vld      (jump_target_vld),
	.jump_target_rdy      (jump_target_rdy),

	.btb_set              (btb_set),
	.btb_set_src_addr     (btb_set_src_addr),
	.btb_set_target_addr  (btb_set_target_addr),
	.btb_clear            (btb_clear),

	.cir                  (cir),
	.cir_vld              (cir_vld),
	.cir_use              (cir_use),
	.cir_err              (cir_err),
	.cir_flush_behind     (cir_flush_behind),

	.predecode_rs1_coarse (predecode_rs1_coarse),
	.predecode_rs2_coarse (predecode_rs2_coarse),
	.predecode_rs1_fine   (predecode_rs1_fine),
	.predecode_rs2_fine   (predecode_rs2_fine),

	.debug_mode           (debug_mode),
	.dbg_instr_data       (dbg_instr_data),
	.dbg_instr_data_vld   (dbg_instr_data_vld),
	.dbg_instr_data_rdy   (dbg_instr_data_rdy)
);

// ----------------------------------------------------------------------------
// Constraints

// TODO this only covers the possibilities of the 2-port processor:

(*keep*) wire        hready;
(*keep*) reg  [31:0] haddr_dphase;
(*keep*) reg         htrans_vld_dphase;

assign mem_addr_rdy = hready;
assign mem_data_vld = hready && htrans_vld_dphase;

assign mem_data = htrans_vld_dphase && hready ? {
	haddr_dphase[16:2], 1'b1,
	haddr_dphase[16:2], 1'b0
} : 32'h0;

always @ (posedge clk or negedge rst_n) begin
	if (!rst_n) begin
		haddr_dphase <= 32'h0;
		htrans_vld_dphase <= 1'b0;
	end else if (hready) begin
		htrans_vld_dphase <= mem_addr_vld;
		if (mem_addr_vld) begin
			haddr_dphase <= mem_addr;
		end
	end
end

assign debug_mode = 1'b0;
assign dbg_instr_data_vld = 1'b0;

// Don't consume nonexistent data
always assume(cir_use <= cir_vld);

// Always consume an amount consistent with the instruction size (as the
// frontend also considers instruction size when a cir_flush_behind occurs)
always assume(cir_use == 0 || cir_use == (cir[1:0] == 2'b11 ? 2'd2 : 2'd1));

assign jump_target[0] = 1'b0;

// flush_behind is always due to an instruction in D, so should only happen
// when the CIR is fully valid.
assign cir_flush_behind = jump_target_vld && jump_target_rdy && ~|cir_use &&
	cir_vld >= (cir[1:0] == 2'b11 ? 2'd2 : 2'd1);

reg cir_locked;
reg [31:0] jump_target_prev;
always @ (posedge clk or negedge rst_n) begin
	if (!rst_n) begin
		cir_locked <= 1'b0;
		jump_target_prev <= 32'h0;
	end else begin
		cir_locked <= (cir_locked || cir_flush_behind) && ~|cir_use;
		jump_target_prev <= jump_target;
		if (cir_locked) begin
			assume(jump_target == jump_target_prev);
			assume(!jump_target_vld);
		end
	end
end

// Jump should not be asserted on the first cycle after reset, as this *will*
// change the fetch address and screw things up. We don't check this in
// hardware (as it's assumed to be impossible in the real processor), just
// assert on it inside the frontend.
always @ (posedge clk) assume(!(jump_target_vld && !$past(rst_n)));

// TODO would be nice to cover this here as well as in the full-core test
assign btb_set = 1'b0;
assign btb_clear = 1'b0;

// ----------------------------------------------------------------------------
// Properties

reg [31:0] pc;

always if (!EXTENSION_C) assume(!pc[1]);

always @ (posedge clk or negedge rst_n) begin
	if (!rst_n) begin
		pc <= RESET_VECTOR;
	end else if (jump_target_vld && jump_target_rdy) begin
		pc <= cir_flush_behind ? pc : jump_target;
	end else if (cir_locked && |cir_use) begin
		pc <= jump_target;
	end else begin
		pc <= pc + {cir_use, 1'b0};
	end
end

always @ (posedge clk) if (rst_n) begin
	// Sanity check
	assert(cir_vld < 2'd3);
	// Instruction data the frontend claims is valid must match the data in
	// memory at the corresponding address.
	if (cir_vld >= 2'd1) begin
		assert(cir[15:0] == pc[16:1]);
	end
	// Note that following a flush_behind the upper half of the CIR may be
	// nonsequential with the lower half, if and only if the lower half
	// contains a 16-bit instruction.
	if (cir_vld >= 2'd2 && cir[1:0] == 2'b11) begin
		assert(cir[31:16] == pc[16:1] + 16'd1);
	end
end

endmodule