| /**************************************************************************** |
| * fwrisc_formal_arith_checker.sv |
| ****************************************************************************/ |
| |
| `include "fwrisc_formal_opcode_defines.svh" |
| /** |
| * Module: fwrisc_formal_jump_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 |
| ); |
| 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[31:0] in_regs[63:0]; |
| reg[31:0] out_regs[63:0]; |
| reg out_regs_w[63:0]; |
| 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; |
| reg[1:0] state = 0; |
| reg[5:0] rd, rs1; |
| reg[6:0] opcode; |
| reg[31:0] imm_jal; |
| reg[31:0] imm_jalr; |
| reg[31:0] pc_curr; |
| reg[31:0] pc_target; |
| always @(posedge clock) begin |
| if (reset == 1) begin |
| ivalid_r <= 0; |
| state <= 0; |
| end else begin |
| ivalid_r <= ivalid; |
| |
| case (state) |
| 0: begin |
| // Capture at the end of the first EXECUTE |
| if (ivalid) begin |
| rd <= `rd(instr); |
| rs1 <= `rs1(instr); |
| opcode <= `opcode(instr); |
| imm_jal <= `imm_jtype(instr); |
| imm_jalr <= $signed(instr[31:20]); |
| pc_curr <= pc; |
| end |
| |
| if (ivalid_r) begin |
| // Calculate the expected jump target |
| case (`opcode(instr)) |
| 7'b1101111: pc_target <= pc_curr + imm_jal; |
| 7'b1100111: pc_target <= in_regs[`rs1(instr)] + imm_jalr; |
| endcase |
| state <= 1; |
| end |
| end |
| |
| 1: begin |
| // End of the second EXECUTE |
| if (ivalid) begin |
| pc_curr <= pc; |
| case (opcode) |
| 7'b1101111,7'b1100111: begin |
| if (pc_target[1] == 0) begin |
| assert(pc[31:1] == pc_target[31:1]); |
| assert (rd == 0 || out_regs[rd] == (pc_curr+4)); |
| assert (rd == 0 || out_regs_w[rd] == 1); |
| end else begin |
| assert(pc == {in_regs['h25][31:2], 2'b0}); // MTVEC |
| assert (out_regs['h29] == pc_curr); // MEPC |
| assert (out_regs_w['h29] == 1); // MEPC |
| assert (out_regs_w['h2A] == 1); // MCAUSE |
| assert (out_regs_w[rd] == 0); |
| end |
| end |
| |
| // Unknown opcode |
| default: begin |
| assert(0); |
| end |
| endcase |
| |
| state <= 2; |
| end |
| end |
| |
| 2: begin |
| // Idle |
| end |
| endcase |
| end |
| end |
| |
| |
| endmodule |
| |
| |