Kestrel-3

reg past_valid = 0;
always @(posedge i_clk) past_valid <= 1;

always #1 i_clk <= ~i_clk;






// After power-on, ROMA must be reset to put it into a known-good state.


always @(posedge i_clk)
if(!past_valid) begin
	assume(i_reset);
	assume(i_a_valid == 0);
end

always @(posedge i_clk)
if($past(i_reset)) begin
	assert(state_waiting_for_get_request);
	assert(!state_waiting_for_flash);
	assert(!state_waiting_to_deliver_results);
end

// The ROMA core exists in one of three major states, which execute sequentially
// and cyclicly:
//
// 1.  Waiting for a GET operation on the A-channel.
// 2.  Waiting for flash ROM to respond with the requested data.
// 3.  Waiting for the master to retrieve its payload on D-channel.

wire [2:0] states = {
	state_waiting_for_get_request,
	state_waiting_for_flash,
	state_waiting_to_deliver_results
};

always @(posedge i_clk)
if(past_valid && !i_reset)
assert((states == 3'b001) || (states == 3'b010) || (states == 3'b100));

always @(posedge i_clk)
if(past_valid && !$past(i_reset) && $fell(state_waiting_for_get_request))
	assert(state_waiting_for_flash);

always @(posedge i_clk)
if(past_valid && !$past(i_reset) && $fell(state_waiting_for_flash))
	assert(state_waiting_to_deliver_results);

always @(posedge i_clk)
if(past_valid && !$past(i_reset) && $fell(state_waiting_to_deliver_results))
	assert(state_waiting_for_get_request);


// Since we're expecting a GET operation only when we're waiting for one,
// we let o_a_ready serve as a flag indicating that to the outside world.

always @(*) assert(o_a_ready == state_waiting_for_get_request);


// When we get a GET request on A-channel, we must change states.

always @(posedge i_clk)
if(past_valid && !$past(i_reset) && $past(o_a_ready) && $past(i_a_valid) && ($past(i_a_opcode) == `A_OPC_GET)) begin
	assert(!state_waiting_for_get_request);
	assert(state_waiting_for_flash);
	assert(!state_waiting_to_deliver_results);
end


// Since waiting for flash ROM to complete means waiting for the entire commnad
// and address to be sent to the chip, and payload to come back from the chip,
// which totals 96 bits, we keep track of how many bits have transpired with
// bits_so_far, and we note that state_waiting_for_flash is asserted while this
// counter hasn't expired yet.

always @(*) assert(state_waiting_for_flash == (bits_so_far <= 96));


// After we're done transferring bits from the flash chip, the counter will
// have elapsed at most 97 times.

always @(posedge i_clk)
assert(bits_so_far <= 97);



// We note that state_waiting_to_deliver_results is asserted for the duration of
// the ROMA core's attempt to return results.  This matches o_d_valid's behavior
// precisely.

always @(*) assert(o_d_valid == state_waiting_to_deliver_results);


// After a system reset, the core must be in an idle state.
always @(posedge i_clk)
if($past(i_reset)) begin
	assert(bits_so_far == 97);
end


always @(*) cover(i_d_ready && o_d_valid && (o_d_data == 64'hDEADBEEFFEEDFACE));

[options]
mode prove
depth 200

[engines]
smtbmc

[script]
read -incdir ../../../../../include/verilog
read -formal -sv roma.v

	input i_a_valid;
	output o_a_ready;

	output reg [2:0] o_d_opcode;
	output [63:0] o_d_data;
	output [1:0] o_d_size;
	output reg [1:0] o_d_source;
	output o_d_valid;
	input i_d_ready;

	output o_spi_mosi;
	input i_spi_miso;
	output o_spi_clk;
	output reg o_spi_cs;

	// The three major states of the ROMA core.
	reg state_waiting_for_get_request;
	reg state_waiting_for_flash;
	reg state_waiting_to_deliver_results;

	always @(posedge i_clk) begin
		state_waiting_for_get_request <= state_waiting_for_get_request;
		state_waiting_for_flash <= state_waiting_for_flash;
		state_waiting_to_deliver_results <= state_waiting_to_deliver_results;

		if(i_reset) begin
			state_waiting_for_get_request <= 1;
			state_waiting_for_flash <= 0;
			state_waiting_to_deliver_results <= 0;
		end
		else if(o_a_ready && i_a_valid && (i_a_opcode == `A_OPC_GET)) begin
			state_waiting_for_get_request <= 0;
			state_waiting_for_flash <= 1;
			state_waiting_to_deliver_results <= 0;
		end
		else if(bits_so_far == 7'd96) begin
			state_waiting_for_get_request <= 0;
			state_waiting_for_flash <= 0;
			state_waiting_to_deliver_results <= 1;
		end
		else if(o_d_valid && i_d_ready) begin
			state_waiting_for_get_request <= 1;
			state_waiting_for_flash <= 0;
			state_waiting_to_deliver_results <= 0;
		end
	end


	reg [32:0] send_message;
	reg [6:0] bits_so_far;
	reg getting_data;

	wire is_read_request = (i_a_valid && o_a_ready && (i_a_opcode === `A_OPC_GET));
	wire can_start_receiving_data = (bits_so_far == 7'd32);
	wire finished_receiving_data = (bits_so_far == 7'd96);
	wire d_channel_handoff = (o_d_valid && i_d_ready);

	assign o_a_ready = state_waiting_for_get_request;
	assign o_d_valid = state_waiting_to_deliver_results;

	assign o_d_size = `D_SIZ_DWORD;
	assign o_spi_clk = i_clk & o_spi_cs;

	always @(posedge i_clk) begin

		o_d_opcode <= o_d_opcode;
		o_d_source <= o_d_source;

		if(i_reset) begin

			o_d_opcode <= 0;
		end
		else if(finished_receiving_data) begin

			o_d_opcode <= `D_OPC_GET_DATA;
			o_d_source <= i_a_source;
		end
		else if(d_channel_handoff) begin

			o_d_opcode <= 0;
		end
	end

	always @(posedge i_clk) begin
		o_spi_cs <= o_spi_cs;

		rxd[7:0], rxd[15:8], rxd[23:16], rxd[31:24],
		rxd[39:32], rxd[47:40], rxd[55:48], rxd[63:56]
	};

`ifdef FORMAL
	initial begin
		bits_so_far <= 97;

		state_waiting_for_get_request <= 1;
		state_waiting_for_flash <= 0;
		state_waiting_to_deliver_results <= 0;
	end

`include "properties.vf"
`endif

endmodule