/****************************************************************************
 * fwrisc_formal_arith_checker.sv
 ****************************************************************************/

`include "fwrisc_formal_opcode_defines.svh"
/**
 * Module: fwrisc_formal_ldst_checker
 * 
 * TODO: Add module documentation
 */
module fwrisc_tracer(
		input			clock,
		input			reset,
		// Current instruction
		input [31:0]	pc,
		input [31:0]	instr,
		// True during execute stage. 
		// Note that write-back will occur at the same time
		input			ivalid,
		// ra, rb
		input [5:0]		ra_raddr,
		input [31:0]	ra_rdata,
		input [5:0]		rb_raddr,
		input [31:0]	rb_rdata,
		// rd
		input [5:0]		rd_waddr,
		input [31:0]	rd_wdata,
		input			rd_write,
		// memory access
		input [31:0]	maddr,
		input [31:0]	mdata,
		input [3:0]		mstrb,
		input			mwrite,
		input 			mvalid		
		);
	reg[31:0]			in_regs[63:0];
	reg[31:0]			out_regs[63:0];
	reg					out_regs_w[63:0];
	wire[31:0]			fwrisc_formal_drdata;
	
	genvar i;
	for (i=0; i<64; i++) begin
		always @(posedge clock) if (reset) out_regs_w[i] <= 0;
	end

	reg[5:0] 	rd, rs1, rs2;
	reg[6:0]	opcode;
	reg[2:0]	funct3;
	reg[6:0]	funct7;
	reg[31:12]	imm_31_12;
	reg[31:0]	imm_11_0;
	reg[31:0]	imm_11_0_u;
	reg[31:0]	pc_r;

	always @(posedge clock) begin
		// Capture at the end of EXECUTE
		if (ivalid) begin
			rd <= `rd(instr);
			rs1 <= `rs1(instr);
			rs2 <= `rs2(instr);
			opcode <= `opcode(instr);
			funct3 <= `funct3(instr);
			funct7 <= `funct7(instr);
			imm_31_12 <= instr[31:12];
			imm_11_0  <= $signed(instr[31:20]);
			imm_11_0_u  <= instr[31:20];
			pc_r <= pc;
		end
	end
	
	reg[5:0] ra_raddr_r, rb_raddr_r;
	
	always @(posedge clock) begin
		ra_raddr_r <= ra_raddr;
		rb_raddr_r <= rb_raddr;
		
		if (reset == 0) begin
			if (rd_write) begin
				out_regs_w[rd_waddr] <= 1;
				out_regs[rd_waddr] <= rd_wdata;
			end
			in_regs[ra_raddr_r] <= ra_rdata;
			in_regs[rb_raddr_r] <= rb_rdata;
		end
	end
	
	reg ivalid_r;
	always @(posedge clock) begin
		if (reset == 1) begin
			ivalid_r <= 0;
		end else begin
			ivalid_r <= ivalid;
			
			assert(pc == fwrisc_formal_drdata);
		
			// Writing to $zero is never expected
			assert(out_regs_w[0] == 0);
			
			cover(ivalid_r == 1);
			
			if (ivalid_r) begin
				case (opcode)
					7'b0110011: begin // register
						case (funct3)
							3'b000: begin // add
								if (funct7 == 7'b0000000) begin
									assert(rd == 0 || out_regs[rd] == in_regs[rs1] + in_regs[rs2]);
								end else begin
									assert(rd == 0 || out_regs[rd] == in_regs[rs1] - in_regs[rs2]);
								end
							end
							3'b001: begin // sll
								assert(rd == 0 || out_regs[rd] == ((in_regs[rs2] << in_regs[rs1]) & 32'hffffffff));
							end
							3'b010: begin // slt
								assert(rd == 0 || out_regs[rd] == ($signed(in_regs[rs1]) < $signed(in_regs[rs2]))?1:0);
							end
							3'b011: begin // sltu
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] < in_regs[rs2])?1:0);
							end
							3'b100: begin // xor
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] ^ in_regs[rs2]));
							end
							3'b101: begin // srl/sra
								if (funct7 == 7'b0000000) begin
									assert(rd == 0 || out_regs[rd] == (in_regs[rs1] >> in_regs[rs2]));
								end else begin
									assert(rd == 0 || out_regs[rd] == (in_regs[rs1] >>> in_regs[rs2]));
								end
							end
							3'b110: begin // or
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] | in_regs[rs2]));
							end
							3'b111: begin // and
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] & in_regs[rs2]));
							end
						endcase
					end
					
					7'b0010011: begin // immediate
						case (funct3)
							3'b000: begin // addi
								assert(rd == 0 || out_regs[rd] == in_regs[rs1] + imm_11_0);
							end
							3'b001: begin // slli
								assert(rd == 0 || out_regs[rd] == ((in_regs[rs1] << rs2) & 32'hffffffff));
							end
							3'b010: begin // slti
								assert(rd == 0 || out_regs[rd] == ($signed(in_regs[rs1]) < $signed(imm_11_0))?1:0);
							end
							3'b011: begin // sltiu
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] < imm_11_0_u)?1:0);
							end
							3'b100: begin // xori
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] ^ imm_11_0_u));
							end
							3'b101: begin // srli
								if (funct7[5]) begin
									assert(rd == 0 || out_regs[rd] == in_regs[rs1] >>> rs2);
								end else begin
									assert(rd == 0 || out_regs[rd] == in_regs[rs1] >> rs2);
								end
							end
							3'b110: begin // ori
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] | imm_11_0_u));
							end
							3'b111: begin // andi
								assert(rd == 0 || out_regs[rd] == (in_regs[rs1] & imm_11_0_u));
							end
						endcase
					end
					
					7'b0010111: begin // auipc
						assert(rd == 0 || out_regs[rd] == (pc_r + $signed(imm_31_12)));
					end
						
					7'b0110111: begin // lui
						assert(rd == 0 || out_regs[rd] == {imm_31_12, 12'h000});
					end
				
					// Unknown opcode
					default: begin
						assert(0);
					end
				endcase
			end
		end
	end
	
	genvar chk_i;
	for (chk_i=1; chk_i<64; chk_i++) begin
		if (chk_i != 'h3f) begin
		always @(posedge clock) 
			// NOTE: ignore writes to the TEMP register
			if (reset == 0 && ivalid_r) begin
				assert(out_regs_w[chk_i] == (chk_i == rd));
				out_regs_w[chk_i] <= 0;
			end
		end
	end


endmodule