| /**************************************************************************** |
| * fwrisc_fetch_formal_seq32_test.sv |
| ****************************************************************************/ |
| `include "fwrisc_fetch_formal_defines.svh" |
| |
| /** |
| * Module: fwrisc_fetch_formal_seq_test |
| * |
| * TODO: Add module documentation |
| */ |
| module fwrisc_fetch_formal_seqmix_test( |
| input clock, |
| input reset, |
| output reg[31:0] next_pc, |
| output reg next_pc_seq, |
| input[31:0] iaddr, |
| output reg[31:0] idata, |
| input ivalid, |
| output iready, |
| input fetch_valid, |
| output decode_complete, |
| input[31:0] instr, |
| input instr_c |
| ); |
| |
| // 00 - 32-bit instruction at aligned address |
| // 01 - 32-bit instruction at unaligned address |
| // 10 - 16-bit instruction at aligned address |
| // 11 - 16-bit instruction at unaligned address |
| `ifdef FORMAL |
| wire [2:0] data_type = `anyconst; |
| // reg [2:0] data_type; |
| `else |
| reg [1:0] data_type; |
| `endif |
| // reg [1:0] data_type; |
| |
| |
| |
| // Instruction-memory unit |
| // 'h63010000 |
| // 'h00376301 |
| // 'h00000037 |
| // 'h6301 |
| always @* begin |
| case (data_type) |
| 2'b00: idata = 'h63010003; // aligned 32-bit instruction |
| 2'b01: idata = 'h00030000; // unaligned 32-bit instruction |
| 2'b10: idata = 'h00000000; // aligned 16-bit instruction |
| default /*2'b11*/: idata = 'h00000003; // unaligned 16-bit instruction |
| endcase |
| |
| case (data_type) |
| 2'b00: next_pc = 'h8000_0000; |
| 2'b01: next_pc = 'h8000_0002; |
| 2'b10: next_pc = 'h8000_0000; |
| default /*2'b11*/: next_pc = 'h8000_0002; |
| endcase |
| end |
| |
| reg[3:0] fetch_count; |
| reg iready_r; |
| assign iready = iready_r; |
| always @(posedge clock) begin |
| if (reset) begin |
| fetch_count <= 0; |
| iready_r <= 0; |
| end else begin |
| if (ivalid) begin |
| iready_r <= ~iready_r; |
| end |
| if (iready && ivalid) begin |
| fetch_count <= fetch_count + 1; |
| end |
| // `cover(fetch_count == 3); |
| end |
| end |
| |
| // Decode unit |
| reg[1:0] decode_state = 0; |
| reg[3:0] instr_count = 0; |
| reg in_reset; |
| // decode_ready signals that the instruction is complete |
| assign decode_complete = (decode_state == 2'b11); |
| always @(posedge clock) begin |
| if (reset) begin |
| next_pc_seq <= 1; |
| decode_state <= 0; |
| instr_count <= 0; |
| in_reset <= 1; |
| end else begin |
| if (in_reset) begin |
| in_reset <= 0; |
| `ifdef FORMAL |
| // data_type <= data_type_w; |
| `else |
| data_type <= `anyconst; |
| `endif |
| end |
| case (decode_state) |
| 2'b00: begin // wait for fetch to complete |
| if (fetch_valid) begin |
| decode_state <= 2'b01; |
| end |
| end |
| 2'b01: begin // instruction executing |
| decode_state <= 2'b10; |
| end |
| |
| 2'b10: begin // instruction executing |
| decode_state <= 2'b11; |
| end |
| |
| 2'b11: begin // ready for next instruction |
| next_pc_seq <= 1; |
| instr_count <= instr_count + 1; |
| `cover(data_type == 2'b00); |
| `cover(data_type == 2'b01); |
| `cover(data_type == 2'b10); |
| // Formal tool really doesn't like to cover this case for some reason |
| // `cover(data_type == 2'b11); |
| // data_type <= data_type + 1; |
| decode_state <= 2'b00; |
| end |
| endcase |
| // `cover (instr_count == 3); |
| end |
| end |
| |
| endmodule |
| |
| |