| |
| `include "fwrisc_fetch_formal_defines.svh" |
| |
| |
| module fwrisc_fetch_formal_seqmix_checker( |
| input clock, |
| input reset, |
| input[31:0] next_pc, |
| input next_pc_seq, |
| input[31:0] iaddr, |
| input[31:0] idata, |
| input ivalid, |
| input iready, |
| input fetch_valid, |
| input decode_complete, |
| input[31:0] instr, |
| input instr_c |
| ); |
| |
| reg[7:0] instr_in_count = 0; |
| reg[7:0] instr_out_count = 0; |
| reg[31:0] last_pc; |
| |
| // Track stream of fetched instructions |
| // against what is delivered |
| reg[1:0] num_fetch; |
| reg[31:0] idata0; |
| reg[31:0] idata1; |
| reg state; |
| |
| always @(posedge clock) begin |
| if (reset) begin |
| instr_in_count <= 0; |
| instr_out_count <= 0; |
| num_fetch <= 0; |
| state <= 0; |
| end else begin |
| if (ivalid && iready) begin |
| if (num_fetch == 0) begin |
| idata0 <= idata; |
| end else if (num_fetch == 1) begin |
| idata1 <= idata; |
| end else begin |
| `assert(0); |
| end |
| num_fetch <= num_fetch + 1; |
| end |
| |
| case (state) |
| 0: begin // Wait for an instruction to be fetched |
| if (fetch_valid) begin |
| `assert(num_fetch == 1 || num_fetch == 2); |
| `cover({next_pc[1], instr_c} == 2'b00); |
| `cover({next_pc[1], instr_c} == 2'b01); |
| `cover({next_pc[1], instr_c} == 2'b10); |
| // Formal tool really doesn't like to cover this case for some reason... |
| // `cover({next_pc[1], instr_c} == 2'b11); |
| case ({next_pc[1], instr_c}) |
| 2'b00: `assert(num_fetch == 1); |
| 2'b01: `assert(num_fetch == 1); |
| 2'b10: `assert(num_fetch == 2); |
| 2'b11: `assert(num_fetch == 1); |
| endcase |
| num_fetch <= 0; |
| state <= 1; |
| end |
| end |
| 1: begin // |
| if (decode_complete) begin |
| instr_out_count <= instr_out_count + 1; |
| // `cover(instr_out_count == 2); |
| state <= 0; |
| end else begin |
| end |
| end |
| endcase |
| end |
| end |
| |
| endmodule |
| |