data/full_repos/permissive/426018168/src/sva/sva_darkriscv.sv
1: b"%Error: data/full_repos/permissive/426018168/src/sva/sva_darkriscv.sv:284: syntax error, unexpected '@', expecting ';'\ndefault clocking c0 @(posedge CLK); endclocking\n                    ^\n%Error: data/full_repos/permissive/426018168/src/sva/sva_darkriscv.sv:312: syntax error, unexpected property, expecting '#' or final\nassume_valid_idata: assume property( \n                           ^~~~~~~~\n%Error: data/full_repos/permissive/426018168/src/sva/sva_darkriscv.sv:316: syntax error, unexpected property, expecting '#' or final\nassume_imm_nonzero: assume property(\n                           ^~~~~~~~\n%Error: data/full_repos/permissive/426018168/src/sva/sva_darkriscv.sv:326: syntax error, unexpected property, expecting '#' or final\nassumme_rx_nonzero: assume property(\n                           ^~~~~~~~\n%Error: data/full_repos/permissive/426018168/src/sva/sva_darkriscv.sv:340: syntax error, unexpected ##, expecting TYPE-IDENTIFIER\n assert_WR_2_after_store: assert property( (IDATA ==? SW) |-> ##2 darkriscv.WR );\n                                                              ^~\n%Error: Exiting due to 5 error(s)\n"
module darkriscv_checker_sva(
    input             CLK,
    input             RES,
    input             HLT,

    input      [31:0] IDATA,
    
    input      [31:0] DATAI,
	

	input [19:0] uimm,
	input [11:0] iimm,
	input [6:0] simm1,
	input [5:0] bimm2,
	input [4:0] simm2,
	input bimm1, bimm3,


	input [4:0] rs1, rs2, rd
	
	);
	



typedef enum bit [2:0] {ITYPE, STYPE, UTYPE, RTYPE, JTYPE, BTYPE, INSTR_ERR} INSTR_TYPE;
INSTR_TYPE instr_type;
bit [31:0] instr;


typedef enum bit [5:0] {ADDI_OP, SLTI_OP, SLTIU_OP, ANDI_OP, ORI_OP, XORI_OP, JALR_OP, LW_OP, LH_OP, LHU_OP, LB_OP, LBU_OP, SLLI_OP, SRLI_OP, SRAI_OP, SW_OP, SH_OP, SB_OP, LUI_OP, AUIPC_OP, ADD_OP, SUB_OP, SLT_OP, SLTU_OP, AND_OP, OR_OP, XOR_OP, SLL_OP, SRL_OP, SRA_OP, JAL_OP, BEQ_OP, BNE_OP, BLT_OP, BLTU_OP, BGE_OP, BGEU_OP, OP_ERR} OP_TYPE;
OP_TYPE op_type;

itype IOP, ADDI, SLTI, SLTIU, ANDI, ORI, XORI, JALR, LW, LH, LHU, LB, LBU, SLLI, SRLI, SRAI;
stype SOP, SW, SH, SB;
utype UOP, LUI, AUIPC;
rtype ROP, ADD, SUB, SLT, SLTU, AND, OR, XOR, SLL, SRL, SRA;
jtype JOP, JAL;
btype BOP, BEQ, BNE, BLT, BLTU, BGE, BGEU;



wire [31:0] OPS [`NUM_OPS];
assign OPS = RES ? '{`NUM_OPS{'x}} : {ADDI, SLTI, SLTIU, ANDI, ORI, XORI, JALR, LW, LH, LHU, LB, LBU, SLLI, SRLI, SRAI, SW, SH, SB, LUI, AUIPC, ADD, SUB, SLT, SLTU, AND, OR, XOR, SLL, SRL, SRA, JAL, BEQ, BNE, BLT, BLTU, BGE, BGEU};



always_comb begin
	

	
	ADDI.funct3 = 0; ADDI.opcode 	= `MCC; ADDI.imm = iimm; 	ADDI.rs1 = rs1; 	ADDI.rd = rd;
	SLTI.funct3 = 2; SLTI.opcode 	= `MCC; SLTI.imm = iimm; 	SLTI.rs1 = rs1; 	SLTI.rd = rd;
	SLTIU.funct3 = 3; SLTIU.opcode 	= `MCC; SLTIU.imm = iimm; 	SLTIU.rs1 = rs1; 	SLTIU.rd = rd;
	XORI.funct3 = 4; XORI.opcode 	= `MCC; XORI.imm = iimm; 	XORI.rs1 = rs1; 	XORI.rd = rd;
	ANDI.funct3 = 7; ANDI.opcode 	= `MCC; ANDI.imm = iimm; 	ANDI.rs1 = rs1; 	ANDI.rd = rd;
	ORI.funct3 	= 6; ORI.opcode 	= `MCC; ORI.imm = iimm; 		ORI.rs1 = rs1; 		ORI.rd = rd;
	SLLI.funct3 = 1; SLLI.opcode 	= `MCC;	SLLI.imm = 0; 			SLLI.rs1 = rs1; 	SLLI.rd = rd;
	SRLI.funct3 = 5; SRLI.opcode 	= `MCC; SRLI.imm = 0; 			SRLI.rs1 = rs1; 	SRLI.rd = rd;
	SRAI.funct3 = 5; SRAI.opcode 	= `MCC; SRAI.imm = 32;			SRAI.rs1 = rs1; 	SRAI.rd = rd;
	
	LW.funct3 		= 2; LW.opcode 		= `LCC; LW.imm = iimm; 	LW.rs1 = rs1; 	LW.rd = rs1;
	LH.funct3 		= 1; LH.opcode 		= `LCC; LH.imm = iimm; 	LH.rs1 = rs1; 	LH.rd = rs1;
	LHU.funct3 		= 5; LHU.opcode 	= `LCC; LHU.imm = iimm; 	LHU.rs1 = rs1; 	LHU.rd = rs1;
	LB.funct3 		= 0; LB.opcode 		= `LCC; LB.imm = iimm; 	LB.rs1 = rs1; 	LB.rd = rs1;
	LBU.funct3 		= 4; LBU.opcode 	= `LCC; LBU.imm = iimm; 	LBU.rs1 = rs1; 	LBU.rd = rs1;
	
	JALR.funct3		= 0; JALR.opcode    = `JALR; JALR.imm = iimm; 	JALR.rs1 = rs1; 	JALR.rd = rs1;
	

	
	SW.funct3 		= 2; SW.opcode 		= `SCC; SW.imm1 = simm1; 	SW.rs1 = rs1;	SW.imm2 = simm2; 	SW.rs2 = rs2;
	SH.funct3 		= 1; SH.opcode 		= `SCC;	SH.imm1 = simm1; 	SH.rs1 = rs1;	SH.imm2 = simm2; 	SH.rs2 = rs2;
	SB.funct3 		= 0; SB.opcode 		= `SCC;	SB.imm1 = simm1; 	SB.rs1 = rs1;	SB.imm2 = simm2; 	SB.rs2 = rs2;
	

	
	LUI.opcode 		= `LUI;		LUI.imm = uimm; 	 	LUI.rd = UOP.rd;						
	AUIPC.opcode 	= `AUIPC;	AUIPC.imm = uimm; 	 	AUIPC.rd = UOP.rd;
	

	
	ADD.funct7		= 0; ADD.funct3		= 0;	ADD.opcode = `RCC; 	ADD.rs2 = rs2; 	ADD.rs1 = rs1; 	ADD.rd = rd;
	SUB.funct7		= 32; SUB.funct3	= 0;	SUB.opcode = `RCC; 	SUB.rs2 = rs2; 	SUB.rs1 = rs1; 	SUB.rd = rd;
	SLT.funct7		= 0; SLT.funct3		= 2;	SLT.opcode = `RCC; 	SLT.rs2 = rs2; 	SLT.rs1 = rs1; 	SLT.rd = rd;
	SLTU.funct7		= 0; SLTU.funct3	= 3;	SLTU.opcode = `RCC; SLTU.rs2 = rs2; 	SLTU.rs1 = rs1; 	SLTU.rd = rd;
	AND.funct7		= 0; AND.funct3		= 7;	AND.opcode = `RCC; 	AND.rs2 = rs2; 	AND.rs1 = rs1; 	AND.rd = rd;
	OR.funct7		= 0; OR.funct3		= 6;	OR.opcode = `RCC; 	OR.rs2 = rs2; 	OR.rs1 = rs1; 	OR.rd = rd;
	XOR.funct7		= 0; XOR.funct3		= 4;	XOR.opcode = `RCC; 	XOR.rs2 = rs2; 	XOR.rs1 = rs1; 	XOR.rd = rd;
	SLL.funct7		= 0; SLL.funct3		= 1;	SLL.opcode = `RCC; 	SLL.rs2 = rs2; 	SLL.rs1 = rs1; 	SLL.rd = rd;
	SRL.funct7		= 0; SRL.funct3		= 5;	SRL.opcode = `RCC; 	SRL.rs2 = rs2; 	SRL.rs1 = rs1; 	SRL.rd = rd;
	SRA.funct7		= 32; SRA.funct3	= 5;	SRA.opcode = `RCC; 	SRA.rs2 = rs2; 	SRA.rs1 = rs1; 	SRA.rd = rd;
	

	
	JAL.opcode 		= `JAL;	JAL.imm1 = JOP.imm1; 	JAL.imm2 = JOP.imm2;	JAL.imm3 = JOP.imm3;	JAL.imm4 = JOP.imm4; JAL.rd = rd;
	

	
	BEQ.funct3		= 0; BEQ.opcode		= `BCC; BEQ.imm1 = bimm1; BEQ.imm2 = bimm2; BEQ.rs2 = rs2; BEQ.rs1 = rs1; BEQ.rd = rd; BEQ.imm3 = bimm3;
	BNE.funct3		= 1; BNE.opcode		= `BCC; BNE.imm1 = bimm1; BNE.imm2 = bimm2; BNE.rs2 = rs2; BNE.rs1 = rs1; BNE.rd = rd; BNE.imm3 = bimm3;
	BLT.funct3		= 4; BLT.opcode		= `BCC; BLT.imm1 = bimm1; BLT.imm2 = bimm2; BLT.rs2 = rs2; BLT.rs1 = rs1; BLT.rd = rd; BLT.imm3 = bimm3;
	BLTU.funct3		= 6; BLTU.opcode	= `BCC; BLTU.imm1 = bimm1; BLTU.imm2 = bimm2; BLTU.rs2 = rs2; BLTU.rs1 = rs1; BLTU.rd = rd; BLTU.imm3 = bimm3;
	BGE.funct3		= 5; BGE.opcode		= `BCC; BGE.imm1 = bimm1; BGE.imm2 = bimm2; BGE.rs2 = rs2; BGE.rs1 = rs1; BGE.rd = rd; BGE.imm3 = bimm3;
	BGEU.funct3		= 7; BGEU.opcode	= `BCC; BGEU.imm1 = bimm1; BGEU.imm2 = bimm2; BGEU.rs2 = rs2; BGEU.rs1 = rs1; BGEU.rd = rd; BGEU.imm3 = bimm3;
	
end



always_comb begin 	


	
	IOP = IDATA;
	SOP = IDATA;
	UOP = IDATA;
	ROP = IDATA;
	JOP = IDATA;
	BOP = IDATA;
	


	instr_type = IDATA[6:0] == (`MCC) 				? ITYPE :
				IDATA[6:0] == (`LCC) 				? ITYPE :
				IDATA[6:0] == (`JALR) 				? ITYPE :
				IDATA[6:0] == (`SCC)				? STYPE :
				IDATA[6:0] == (`LUI)				? UTYPE :
				IDATA[6:0] == (`AUIPC) 				? UTYPE :
				IDATA[6:0] == (`RCC)				? RTYPE :
				IDATA[6:0] == (`JAL)				? JTYPE :
				IDATA[6:0] == (`BCC)				? BTYPE : INSTR_ERR;
	

	
	unique case (instr_type)
		ITYPE : begin
					if(IDATA[6:0] == `MCC) 
						op_type = 	(IOP.funct3 == 0) ? ADDI_OP :
									IOP.funct3 == 1 ? SLLI_OP :
									IOP.funct3 == 2 ? SLTI_OP :
									IOP.funct3 == 3 ? SLTIU_OP :
									IOP.funct3 == 4 ? XORI_OP :
									IOP.funct3 == 5 && IOP.imm == 0 ? SRLI_OP :
									IOP.funct3 == 5 && IOP.imm == 32 ? SRAI_OP :
									IOP.funct3 == 6 ? ORI_OP :
									IOP.funct3 == 7 ? ANDI_OP : OP_ERR;
					else if(IDATA[6:0] == `LCC)
						op_type =	IOP.funct3 == 0 ? LB_OP :
									IOP.funct3 == 1 ? LH_OP :
									IOP.funct3 == 2 ? LW_OP :
									IOP.funct3 == 4 ? LBU_OP :
									IOP.funct3 == 5 ? LHU_OP : OP_ERR;
					else if(IDATA[6:0] == `JALR)
						op_type =	IOP.funct3 == 0 ? JALR_OP : OP_ERR;
					else
						op_type = OP_ERR;
				end
				
		STYPE :	op_type = 	SOP.funct3 == 0 ? SB_OP :
							SOP.funct3 == 1	? SH_OP :
							SOP.funct3 == 2 ? SW_OP : OP_ERR;
							
		UTYPE : op_type =	UOP.opcode == `LUI ? LUI_OP :
							UOP.opcode == `AUIPC ? AUIPC_OP : OP_ERR;
							
		RTYPE :	op_type =	ROP.funct7 == 0 && ROP.funct3 == 0 	? ADD_OP :
							ROP.funct7 == 32 && ROP.funct3 == 0 ? SUB_OP :
							ROP.funct7 == 0 && ROP.funct3 == 2 	? SLT_OP :
							ROP.funct7 == 0 && ROP.funct3 == 3 	? SLTU_OP :
							ROP.funct7 == 0 && ROP.funct3 == 7 	? AND_OP :
							ROP.funct7 == 0 && ROP.funct3 == 6 	? OR_OP :
							ROP.funct7 == 0 && ROP.funct3 == 4 	? XOR_OP :
							ROP.funct7 == 0 && ROP.funct3 == 1 	? SLL_OP :
							ROP.funct7 == 0 && ROP.funct3 == 5 	? SRL_OP :
							ROP.funct7 == 32 && ROP.funct3 == 5 ? SRA_OP : OP_ERR;
							
		JTYPE : op_type = 	JOP.opcode == `JAL ? JAL_OP : OP_ERR;
		
		BTYPE : op_type =	BOP.funct3 == 0 ? BEQ_OP :
							BOP.funct3 == 1 ? BNE_OP :
							BOP.funct3 == 4 ? BLT_OP :
							BOP.funct3 == 5 ? BGE_OP :
							BOP.funct3 == 6 ? BLTU_OP :
							BOP.funct3 == 7 ? BGEU_OP : OP_ERR;
	endcase 
	
end



default clocking c0 @(posedge CLK); endclocking







genvar i;
generate for( i = 0; i < `NUM_OPS; i = i + 1) begin: instr_cover
	opcode: cover property(IDATA ==? OPS[i]);
end
endgenerate



cover_wr_en: cover property( darkriscv.WR == 1'b1 );



cover_rd_en: cover property( darkriscv.RD  == 1'b1 );



cover_idle_en: cover property( darkriscv.IDLE == 1'b1 );



assume_valid_idata: assume property( 
	IDATA ==? ADDI || IDATA ==? SLTI || IDATA ==? SLTIU || IDATA ==? ANDI || IDATA ==? ORI || IDATA ==? XORI || IDATA ==? JALR || IDATA ==? LW || IDATA ==? LH || IDATA ==? LHU || IDATA ==? LB || IDATA ==? LBU || IDATA ==? SLLI || IDATA ==? SRLI || IDATA ==? SRAI || IDATA ==? SW || IDATA ==? SH || IDATA ==? SB || IDATA ==? LUI || IDATA ==? AUIPC || IDATA ==? ADD || IDATA ==? SUB || IDATA ==? SLT || IDATA ==? SLTU || IDATA ==? AND || IDATA ==? OR || IDATA ==? XOR || IDATA ==? SLL || IDATA ==? SRL || IDATA ==? SRA || IDATA ==? JAL || IDATA ==? BEQ || IDATA ==? BNE || IDATA ==? BLT || IDATA ==? BLTU || IDATA ==? BGE || IDATA ==? BGEU );
	

assume_imm_nonzero: assume property(
	uimm != 0 &&
	iimm != 0 &&
	simm1 != 0 &&
	bimm2 != 0 &&
	simm2 != 0 &&
	bimm1 != 0 &&
	bimm3 != 0 );
	

assumme_rx_nonzero: assume property(
	rd != 0 &&
	rs1 != 0 &&
	rs2 != 0 );
		


assert_not_rd_and_wr: assert property( !(darkriscv.WR == 1'b1 && darkriscv.RD == 1'b1) );



`ifdef __3STAGE__
	assert_WR_3_after_store: assert property( (IDATA ==? SW) |-> ##3 darkriscv.WR );
`else
	assert_WR_2_after_store: assert property( (IDATA ==? SW) |-> ##2 darkriscv.WR );
`endif


endmodule
module darkriscv_checker_sva(
    input             CLK,
    input             RES,
    input             HLT,

    input      [31:0] IDATA,
    
    input      [31:0] DATAI,
	

	input [19:0] uimm,
	input [11:0] iimm,
	input [6:0] simm1,
	input [5:0] bimm2,
	input [4:0] simm2,
	input bimm1, bimm3,


	input [4:0] rs1, rs2, rd
	
	);

	



typedef enum bit [2:0] {ITYPE, STYPE, UTYPE, RTYPE, JTYPE, BTYPE, INSTR_ERR} INSTR_TYPE;
INSTR_TYPE instr_type;
bit [31:0] instr;


typedef enum bit [5:0] {ADDI_OP, SLTI_OP, SLTIU_OP, ANDI_OP, ORI_OP, XORI_OP, JALR_OP, LW_OP, LH_OP, LHU_OP, LB_OP, LBU_OP, SLLI_OP, SRLI_OP, SRAI_OP, SW_OP, SH_OP, SB_OP, LUI_OP, AUIPC_OP, ADD_OP, SUB_OP, SLT_OP, SLTU_OP, AND_OP, OR_OP, XOR_OP, SLL_OP, SRL_OP, SRA_OP, JAL_OP, BEQ_OP, BNE_OP, BLT_OP, BLTU_OP, BGE_OP, BGEU_OP, OP_ERR} OP_TYPE;
OP_TYPE op_type;

itype IOP, ADDI, SLTI, SLTIU, ANDI, ORI, XORI, JALR, LW, LH, LHU, LB, LBU, SLLI, SRLI, SRAI;
stype SOP, SW, SH, SB;
utype UOP, LUI, AUIPC;
rtype ROP, ADD, SUB, SLT, SLTU, AND, OR, XOR, SLL, SRL, SRA;
jtype JOP, JAL;
btype BOP, BEQ, BNE, BLT, BLTU, BGE, BGEU;



wire [31:0] OPS [`NUM_OPS];
assign OPS = RES ? '{`NUM_OPS{'x}} : {ADDI, SLTI, SLTIU, ANDI, ORI, XORI, JALR, LW, LH, LHU, LB, LBU, SLLI, SRLI, SRAI, SW, SH, SB, LUI, AUIPC, ADD, SUB, SLT, SLTU, AND, OR, XOR, SLL, SRL, SRA, JAL, BEQ, BNE, BLT, BLTU, BGE, BGEU};



always_comb begin
	

	
	ADDI.funct3 = 0; ADDI.opcode 	= `MCC; ADDI.imm = iimm; 	ADDI.rs1 = rs1; 	ADDI.rd = rd;
	SLTI.funct3 = 2; SLTI.opcode 	= `MCC; SLTI.imm = iimm; 	SLTI.rs1 = rs1; 	SLTI.rd = rd;
	SLTIU.funct3 = 3; SLTIU.opcode 	= `MCC; SLTIU.imm = iimm; 	SLTIU.rs1 = rs1; 	SLTIU.rd = rd;
	XORI.funct3 = 4; XORI.opcode 	= `MCC; XORI.imm = iimm; 	XORI.rs1 = rs1; 	XORI.rd = rd;
	ANDI.funct3 = 7; ANDI.opcode 	= `MCC; ANDI.imm = iimm; 	ANDI.rs1 = rs1; 	ANDI.rd = rd;
	ORI.funct3 	= 6; ORI.opcode 	= `MCC; ORI.imm = iimm; 		ORI.rs1 = rs1; 		ORI.rd = rd;
	SLLI.funct3 = 1; SLLI.opcode 	= `MCC;	SLLI.imm = 0; 			SLLI.rs1 = rs1; 	SLLI.rd = rd;
	SRLI.funct3 = 5; SRLI.opcode 	= `MCC; SRLI.imm = 0; 			SRLI.rs1 = rs1; 	SRLI.rd = rd;
	SRAI.funct3 = 5; SRAI.opcode 	= `MCC; SRAI.imm = 32;			SRAI.rs1 = rs1; 	SRAI.rd = rd;
	
	LW.funct3 		= 2; LW.opcode 		= `LCC; LW.imm = iimm; 	LW.rs1 = rs1; 	LW.rd = rs1;
	LH.funct3 		= 1; LH.opcode 		= `LCC; LH.imm = iimm; 	LH.rs1 = rs1; 	LH.rd = rs1;
	LHU.funct3 		= 5; LHU.opcode 	= `LCC; LHU.imm = iimm; 	LHU.rs1 = rs1; 	LHU.rd = rs1;
	LB.funct3 		= 0; LB.opcode 		= `LCC; LB.imm = iimm; 	LB.rs1 = rs1; 	LB.rd = rs1;
	LBU.funct3 		= 4; LBU.opcode 	= `LCC; LBU.imm = iimm; 	LBU.rs1 = rs1; 	LBU.rd = rs1;
	
	JALR.funct3		= 0; JALR.opcode    = `JALR; JALR.imm = iimm; 	JALR.rs1 = rs1; 	JALR.rd = rs1;
	

	
	SW.funct3 		= 2; SW.opcode 		= `SCC; SW.imm1 = simm1; 	SW.rs1 = rs1;	SW.imm2 = simm2; 	SW.rs2 = rs2;
	SH.funct3 		= 1; SH.opcode 		= `SCC;	SH.imm1 = simm1; 	SH.rs1 = rs1;	SH.imm2 = simm2; 	SH.rs2 = rs2;
	SB.funct3 		= 0; SB.opcode 		= `SCC;	SB.imm1 = simm1; 	SB.rs1 = rs1;	SB.imm2 = simm2; 	SB.rs2 = rs2;
	

	
	LUI.opcode 		= `LUI;		LUI.imm = uimm; 	 	LUI.rd = UOP.rd;						
	AUIPC.opcode 	= `AUIPC;	AUIPC.imm = uimm; 	 	AUIPC.rd = UOP.rd;
	

	
	ADD.funct7		= 0; ADD.funct3		= 0;	ADD.opcode = `RCC; 	ADD.rs2 = rs2; 	ADD.rs1 = rs1; 	ADD.rd = rd;
	SUB.funct7		= 32; SUB.funct3	= 0;	SUB.opcode = `RCC; 	SUB.rs2 = rs2; 	SUB.rs1 = rs1; 	SUB.rd = rd;
	SLT.funct7		= 0; SLT.funct3		= 2;	SLT.opcode = `RCC; 	SLT.rs2 = rs2; 	SLT.rs1 = rs1; 	SLT.rd = rd;
	SLTU.funct7		= 0; SLTU.funct3	= 3;	SLTU.opcode = `RCC; SLTU.rs2 = rs2; 	SLTU.rs1 = rs1; 	SLTU.rd = rd;
	AND.funct7		= 0; AND.funct3		= 7;	AND.opcode = `RCC; 	AND.rs2 = rs2; 	AND.rs1 = rs1; 	AND.rd = rd;
	OR.funct7		= 0; OR.funct3		= 6;	OR.opcode = `RCC; 	OR.rs2 = rs2; 	OR.rs1 = rs1; 	OR.rd = rd;
	XOR.funct7		= 0; XOR.funct3		= 4;	XOR.opcode = `RCC; 	XOR.rs2 = rs2; 	XOR.rs1 = rs1; 	XOR.rd = rd;
	SLL.funct7		= 0; SLL.funct3		= 1;	SLL.opcode = `RCC; 	SLL.rs2 = rs2; 	SLL.rs1 = rs1; 	SLL.rd = rd;
	SRL.funct7		= 0; SRL.funct3		= 5;	SRL.opcode = `RCC; 	SRL.rs2 = rs2; 	SRL.rs1 = rs1; 	SRL.rd = rd;
	SRA.funct7		= 32; SRA.funct3	= 5;	SRA.opcode = `RCC; 	SRA.rs2 = rs2; 	SRA.rs1 = rs1; 	SRA.rd = rd;
	

	
	JAL.opcode 		= `JAL;	JAL.imm1 = JOP.imm1; 	JAL.imm2 = JOP.imm2;	JAL.imm3 = JOP.imm3;	JAL.imm4 = JOP.imm4; JAL.rd = rd;
	

	
	BEQ.funct3		= 0; BEQ.opcode		= `BCC; BEQ.imm1 = bimm1; BEQ.imm2 = bimm2; BEQ.rs2 = rs2; BEQ.rs1 = rs1; BEQ.rd = rd; BEQ.imm3 = bimm3;
	BNE.funct3		= 1; BNE.opcode		= `BCC; BNE.imm1 = bimm1; BNE.imm2 = bimm2; BNE.rs2 = rs2; BNE.rs1 = rs1; BNE.rd = rd; BNE.imm3 = bimm3;
	BLT.funct3		= 4; BLT.opcode		= `BCC; BLT.imm1 = bimm1; BLT.imm2 = bimm2; BLT.rs2 = rs2; BLT.rs1 = rs1; BLT.rd = rd; BLT.imm3 = bimm3;
	BLTU.funct3		= 6; BLTU.opcode	= `BCC; BLTU.imm1 = bimm1; BLTU.imm2 = bimm2; BLTU.rs2 = rs2; BLTU.rs1 = rs1; BLTU.rd = rd; BLTU.imm3 = bimm3;
	BGE.funct3		= 5; BGE.opcode		= `BCC; BGE.imm1 = bimm1; BGE.imm2 = bimm2; BGE.rs2 = rs2; BGE.rs1 = rs1; BGE.rd = rd; BGE.imm3 = bimm3;
	BGEU.funct3		= 7; BGEU.opcode	= `BCC; BGEU.imm1 = bimm1; BGEU.imm2 = bimm2; BGEU.rs2 = rs2; BGEU.rs1 = rs1; BGEU.rd = rd; BGEU.imm3 = bimm3;
	
end



always_comb begin 	


	
	IOP = IDATA;
	SOP = IDATA;
	UOP = IDATA;
	ROP = IDATA;
	JOP = IDATA;
	BOP = IDATA;
	


	instr_type = IDATA[6:0] == (`MCC) 				? ITYPE :
				IDATA[6:0] == (`LCC) 				? ITYPE :
				IDATA[6:0] == (`JALR) 				? ITYPE :
				IDATA[6:0] == (`SCC)				? STYPE :
				IDATA[6:0] == (`LUI)				? UTYPE :
				IDATA[6:0] == (`AUIPC) 				? UTYPE :
				IDATA[6:0] == (`RCC)				? RTYPE :
				IDATA[6:0] == (`JAL)				? JTYPE :
				IDATA[6:0] == (`BCC)				? BTYPE : INSTR_ERR;
	

	
	unique case (instr_type)
		ITYPE : begin
					if(IDATA[6:0] == `MCC) 
						op_type = 	(IOP.funct3 == 0) ? ADDI_OP :
									IOP.funct3 == 1 ? SLLI_OP :
									IOP.funct3 == 2 ? SLTI_OP :
									IOP.funct3 == 3 ? SLTIU_OP :
									IOP.funct3 == 4 ? XORI_OP :
									IOP.funct3 == 5 && IOP.imm == 0 ? SRLI_OP :
									IOP.funct3 == 5 && IOP.imm == 32 ? SRAI_OP :
									IOP.funct3 == 6 ? ORI_OP :
									IOP.funct3 == 7 ? ANDI_OP : OP_ERR;
					else if(IDATA[6:0] == `LCC)
						op_type =	IOP.funct3 == 0 ? LB_OP :
									IOP.funct3 == 1 ? LH_OP :
									IOP.funct3 == 2 ? LW_OP :
									IOP.funct3 == 4 ? LBU_OP :
									IOP.funct3 == 5 ? LHU_OP : OP_ERR;
					else if(IDATA[6:0] == `JALR)
						op_type =	IOP.funct3 == 0 ? JALR_OP : OP_ERR;
					else
						op_type = OP_ERR;
				end
				
		STYPE :	op_type = 	SOP.funct3 == 0 ? SB_OP :
							SOP.funct3 == 1	? SH_OP :
							SOP.funct3 == 2 ? SW_OP : OP_ERR;
							
		UTYPE : op_type =	UOP.opcode == `LUI ? LUI_OP :
							UOP.opcode == `AUIPC ? AUIPC_OP : OP_ERR;
							
		RTYPE :	op_type =	ROP.funct7 == 0 && ROP.funct3 == 0 	? ADD_OP :
							ROP.funct7 == 32 && ROP.funct3 == 0 ? SUB_OP :
							ROP.funct7 == 0 && ROP.funct3 == 2 	? SLT_OP :
							ROP.funct7 == 0 && ROP.funct3 == 3 	? SLTU_OP :
							ROP.funct7 == 0 && ROP.funct3 == 7 	? AND_OP :
							ROP.funct7 == 0 && ROP.funct3 == 6 	? OR_OP :
							ROP.funct7 == 0 && ROP.funct3 == 4 	? XOR_OP :
							ROP.funct7 == 0 && ROP.funct3 == 1 	? SLL_OP :
							ROP.funct7 == 0 && ROP.funct3 == 5 	? SRL_OP :
							ROP.funct7 == 32 && ROP.funct3 == 5 ? SRA_OP : OP_ERR;
							
		JTYPE : op_type = 	JOP.opcode == `JAL ? JAL_OP : OP_ERR;
		
		BTYPE : op_type =	BOP.funct3 == 0 ? BEQ_OP :
							BOP.funct3 == 1 ? BNE_OP :
							BOP.funct3 == 4 ? BLT_OP :
							BOP.funct3 == 5 ? BGE_OP :
							BOP.funct3 == 6 ? BLTU_OP :
							BOP.funct3 == 7 ? BGEU_OP : OP_ERR;
	endcase 
	
end



default clocking c0 @(posedge CLK); endclocking







genvar i;
generate for( i = 0; i < `NUM_OPS; i = i + 1) begin: instr_cover
	opcode: cover property(IDATA ==? OPS[i]);
end
endgenerate



cover_wr_en: cover property( darkriscv.WR == 1'b1 );



cover_rd_en: cover property( darkriscv.RD  == 1'b1 );



cover_idle_en: cover property( darkriscv.IDLE == 1'b1 );



assume_valid_idata: assume property( 
	IDATA ==? ADDI || IDATA ==? SLTI || IDATA ==? SLTIU || IDATA ==? ANDI || IDATA ==? ORI || IDATA ==? XORI || IDATA ==? JALR || IDATA ==? LW || IDATA ==? LH || IDATA ==? LHU || IDATA ==? LB || IDATA ==? LBU || IDATA ==? SLLI || IDATA ==? SRLI || IDATA ==? SRAI || IDATA ==? SW || IDATA ==? SH || IDATA ==? SB || IDATA ==? LUI || IDATA ==? AUIPC || IDATA ==? ADD || IDATA ==? SUB || IDATA ==? SLT || IDATA ==? SLTU || IDATA ==? AND || IDATA ==? OR || IDATA ==? XOR || IDATA ==? SLL || IDATA ==? SRL || IDATA ==? SRA || IDATA ==? JAL || IDATA ==? BEQ || IDATA ==? BNE || IDATA ==? BLT || IDATA ==? BLTU || IDATA ==? BGE || IDATA ==? BGEU );
	

assume_imm_nonzero: assume property(
	uimm != 0 &&
	iimm != 0 &&
	simm1 != 0 &&
	bimm2 != 0 &&
	simm2 != 0 &&
	bimm1 != 0 &&
	bimm3 != 0 );
	

assumme_rx_nonzero: assume property(
	rd != 0 &&
	rs1 != 0 &&
	rs2 != 0 );
		


assert_not_rd_and_wr: assert property( !(darkriscv.WR == 1'b1 && darkriscv.RD == 1'b1) );



`ifdef __3STAGE__
	assert_WR_3_after_store: assert property( (IDATA ==? SW) |-> ##3 darkriscv.WR );
`else
	assert_WR_2_after_store: assert property( (IDATA ==? SW) |-> ##2 darkriscv.WR );
`endif


endmodule