| `include "fwrisc_exec_formal_defines.svh" |
| |
| |
| module fwrisc_exec_formal_arith_checker( |
| input clock, |
| input reset, |
| input decode_valid, |
| input instr_complete, |
| |
| // Indicates whether the instruction is compressed |
| input instr_c, |
| |
| input[4:0] op_type, |
| |
| input[31:0] op_a, |
| input[31:0] op_b, |
| input[5:0] op, |
| input[31:0] op_c, |
| input[5:0] rd, |
| |
| input[5:0] rd_waddr, |
| input[31:0] rd_wdata, |
| input rd_wen, |
| |
| input[31:1] pc, |
| // Indicates that the PC is sequential to the last PC |
| input pc_seq, |
| input[31:0] mtvec, |
| input[31:0] daddr, |
| input dvalid, |
| input dwrite, |
| input[31:0] dwdata, |
| input[3:0] dwstb, |
| input[31:0] drdata, |
| input dready |
| ); |
| `include "fwrisc_op_type.svh" |
| `include "fwrisc_alu_op.svh" |
| |
| reg[7:0] count = 0; |
| reg[31:0] wr_data; |
| reg[1:0] rd_wr_count; |
| reg[31:0] rd_wr_data; |
| reg[5:0] rd_wr; |
| reg[2:0] instr_count; |
| |
| always @(posedge clock) begin |
| if (reset) begin |
| count <= 0; |
| wr_data <= 0; |
| rd_wr_count <= 0; |
| instr_count <= 0; |
| end else begin |
| if (rd_wen) begin |
| rd_wr_count <= rd_wr_count + 1; |
| rd_wr_data <= rd_wdata; |
| rd_wr <= rd_waddr; |
| end |
| |
| if (instr_complete) begin |
| `assert(rd_wr_count == 1); |
| `assert(rd_wr == rd); |
| rd_wr_count <= 0; |
| instr_count <= instr_count + 1; |
| case (op_type) |
| OP_TYPE_ARITH: begin |
| `cover(op==OP_ADD); |
| `cover(op==OP_SUB); |
| `cover(op==OP_AND); |
| `cover(op==OP_OR); |
| `cover(op==OP_CLR); |
| `cover(op==OP_EQ); |
| `cover(op==OP_LT); |
| `cover(op==OP_LTU); |
| `cover(op==OP_XOR); |
| `cover(op==OP_OPA); |
| `cover(op==OP_OPB); |
| `assert(op == OP_ADD || op == OP_SUB || op == OP_AND || |
| op == OP_OR || op == OP_CLR || op == OP_EQ || |
| op == OP_LT || op == OP_LTU || op == OP_XOR || |
| op == OP_OPA || op == OP_OPB); |
| case (op) |
| OP_ADD: begin |
| `assert(rd_wr_data == (op_a + op_b)); |
| end |
| OP_SUB: begin |
| `assert(rd_wr_data == (op_a - op_b)); |
| end |
| OP_AND: begin |
| `assert(rd_wr_data == (op_a & op_b)); |
| end |
| OP_OR: begin |
| `assert(rd_wr_data == (op_a | op_b)); |
| end |
| OP_CLR: begin |
| `assert(rd_wr_data == (op_b ^ (op_a & op_b))); |
| end |
| OP_EQ: begin |
| `assert(rd_wr_data == (op_a == op_b)); |
| end |
| OP_LT: begin |
| `assert(rd_wr_data == ($signed(op_a) < $signed(op_b))); |
| end |
| OP_LTU: begin |
| `assert(rd_wr_data == (op_a < op_b)); |
| end |
| OP_XOR: begin |
| `assert(rd_wr_data == (op_a ^ op_b)); |
| end |
| OP_OPA: begin |
| `assert(rd_wr_data == op_a); |
| end |
| OP_OPB: begin |
| `assert(rd_wr_data == op_b); |
| end |
| default: begin |
| `assert(0); |
| end |
| endcase |
| end |
| default: begin |
| `assert(0); |
| end |
| endcase |
| end |
| `cover(instr_count == 2); |
| end |
| end |
| |
| endmodule |
| |