Subversion Repositories zipcpu

////////////////////////////////////////////////////////////////////////////////

//

// Filename:    prefetch.v

//

// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core

//

// Purpose:     This is a very simple instruction fetch approach.  It gets

//              one instruction at a time.  Future versions should pipeline

//      fetches and perhaps even cache results--this doesn't do that.  It

//      should, however, be simple enough to get things running.

//

//      The interface is fascinating.  The 'i_pc' input wire is just a

//      suggestion of what to load.  Other wires may be loaded instead. i_pc

//      is what must be output, not necessarily input.

//

//   20150919 -- Added support for the WB error signal.  When reading an

//      instruction results in this signal being raised, the pipefetch module

//      will set an illegal instruction flag to be returned to the CPU together

//      with the instruction.  Hence, the ZipCPU can trap on it if necessary.

//

//   20171020 -- Added a formal proof to prove that the module works.  This

//      also involved adding a req_addr register, and the logic associated

//      with it.

//

//   20171113 -- Removed the req_addr register, replacing it with a bus abort

//      capability.

//

// Creator:     Dan Gisselquist, Ph.D.

//              Gisselquist Technology, LLC

//

////////////////////////////////////////////////////////////////////////////////

//

// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC

//

// This program is free software (firmware): you can redistribute it and/or

// modify it under the terms of  the GNU General Public License as published

// by the Free Software Foundation, either version 3 of the License, or (at

// your option) any later version.

//

// This program is distributed in the hope that it will be useful, but WITHOUT

// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or

// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License

// for more details.

//

// You should have received a copy of the GNU General Public License along

// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no

// target there if the PDF file isn't present.)  If not, see

// <http://www.gnu.org/licenses/> for a copy.

//

// License:     GPL, v3, as defined and found on www.gnu.org,

//              http://www.gnu.org/licenses/gpl.html

//

//

////////////////////////////////////////////////////////////////////////////////

//

//

`default_nettype        none

//

//

module  prefetch(i_clk, i_reset, i_new_pc, i_clear_cache, i_stalled_n, i_pc,

                        o_insn, o_pc, o_valid, o_illegal,

                o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,

                        i_wb_ack, i_wb_stall, i_wb_err, i_wb_data);

        parameter               ADDRESS_WIDTH=30, DATA_WIDTH=32;

        localparam              AW=ADDRESS_WIDTH,

                                DW=DATA_WIDTH;

        input   wire                    i_clk, i_reset;

        // CPU interaction wires

        input   wire                    i_new_pc, i_clear_cache, i_stalled_n;

        // We ignore i_pc unless i_new_pc is true as well

        input   wire    [(AW+1):0]       i_pc;

        output  reg     [(DW-1):0]       o_insn; // Instruction read from WB

        output  wire    [(AW+1):0]       o_pc;   // Address of that instruction

        output  reg                     o_valid; // If the output is valid

        output  reg                     o_illegal; // Result is from a bus err

        // Wishbone outputs

        output  reg                     o_wb_cyc, o_wb_stb;

        output  wire                    o_wb_we;

        output  reg     [(AW-1):0]       o_wb_addr;

        output  wire    [(DW-1):0]       o_wb_data;

        // And return inputs

        input   wire                    i_wb_ack, i_wb_stall, i_wb_err;

        input   wire    [(DW-1):0]       i_wb_data;

        // Declare local variables

        reg                     invalid;

        // These are kind of obligatory outputs when dealing with a bus, that

        // we'll set them here.  Nothing's going to pay attention to these,

        // though, this is primarily for form.

        assign  o_wb_we = 1'b0;

        assign  o_wb_data = 32'h0000;

        // Let's build it simple and upgrade later: For each instruction

        // we do one bus cycle to get the instruction.  Later we should

        // pipeline this, but for now let's just do one at a time.

        initial o_wb_cyc = 1'b0;

        initial o_wb_stb = 1'b0;

        always @(posedge i_clk)

        if ((i_reset)||((o_wb_cyc)&&((i_wb_ack)||(i_wb_err))))

        begin

                // End any bus cycle on a reset, or a return ACK

                // or error.

                o_wb_cyc <= 1'b0;

                o_wb_stb <= 1'b0;

        end else if ((!o_wb_cyc)&&(

                        // Start if the last instruction output was

                        // accepted, *and* it wasn't a bus error

                        // response

                        ((i_stalled_n)&&(!o_illegal))

                        // Start if the last bus result ended up

                        // invalid

                        ||(invalid)

                        // Start on any request for a new address

                        ||(i_new_pc)))

        begin

                // Initiate a bus transaction

                o_wb_cyc <= 1'b1;

                o_wb_stb <= 1'b1;

        end else if (o_wb_cyc)

        begin

                // If our request has been accepted, then drop the

                // strobe line

                if (!i_wb_stall)

                        o_wb_stb <= 1'b0;

                // Abort on new-pc

                // ... clear_cache  is identical, save that it will

                // immediately be followed by a new PC, so we don't

                // need to worry about that other than to drop

                // CYC and STB here.

                if (i_new_pc)

                begin

                        o_wb_cyc <= 1'b0;

                        o_wb_stb <= 1'b0;

                end

        end

        //

        // If during the current bus request, a command came in from the CPU

        // that will invalidate the results of that request, then we need to

        // keep track of an "invalid" flag to remember that and so squash

        // the result.

        //

        initial invalid = 1'b0;

        always @(posedge i_clk)

        if ((i_reset)||(!o_wb_cyc))

                invalid <= 1'b0;

        else if (i_new_pc)

                invalid <= 1'b1;

        // The wishbone request address, o_wb_addr

        //

        // The rule regarding this address is that it can *only* be changed

        // when no bus request is active.  Further, since the CPU is depending

        // upon this value to know what "PC" is associated with the instruction

        // it is processing, we can't change until either the CPU has accepted

        // our result, or it is requesting a new PC (and hence not using the

        // output).

        //

        initial o_wb_addr= 0;

        always @(posedge i_clk)

        if (i_new_pc)

                o_wb_addr  <= i_pc[AW+1:2];

        else if ((o_valid)&&(i_stalled_n)&&(!o_illegal))

                o_wb_addr  <= o_wb_addr + 1'b1;

        // The instruction returned is given by the data returned from the bus.

        always @(posedge i_clk)

        if ((o_wb_cyc)&&(i_wb_ack))

                o_insn <= i_wb_data;

        //

        // Finally, the flags associated with the prefetch.  The rule is that

        // if the output represents a return from the bus, then o_valid needs

        // to be true.  o_illegal will be true any time the last bus request

        // resulted in an error.  o_illegal is only relevant to the CPU when

        // o_valid is also true, hence o_valid will be true even in the case

        // of a bus error in our request.

        //

        initial o_valid   = 1'b0;

        initial o_illegal = 1'b0;

        always @(posedge i_clk)

        if ((i_reset)||(i_new_pc)||(i_clear_cache))

        begin

                // On any reset, request for a new PC (i.e. a branch),

                // or a request to clear our cache (i.e. the data

                // in memory may have changed), we invalidate any

                // output.

                o_valid   <= 1'b0;

                o_illegal <= 1'b0;

        end else if ((o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))

        begin

                // Otherwise, at the end of our bus cycle, the

                // answer will be valid.  Well, not quite.  If the

                // user requested something mid-cycle (i_new_pc)

                // or (i_clear_cache), then we'll have to redo the

                // bus request, so we aren't valid.

                //

                o_valid   <= 1'b1;

                o_illegal <= ( i_wb_err);

        end else if (i_stalled_n)

        begin

                // Once the CPU accepts any result we produce, clear

                // the valid flag, lest we send two identical

                // instructions to the CPU.

                //

                o_valid <= 1'b0;

                //

                // o_illegal doesn't change ... that way we don't

                // access the bus again until a new address request

                // is given to us, via i_new_pc, or we are asked

                //  to check again via i_clear_cache

                //

                // o_illegal <= (!i_stalled_n);

        end

        // The o_pc output shares its value with the (last) wishbone address

        assign  o_pc = { o_wb_addr, 2'b00 };

        // Make verilator happy

        // verilator lint_off UNUSED

        wire    [1:0]    unused;

        assign  unused = i_pc[1:0];

        // verilator lint_on  UNUSED

`ifdef  FORMAL

        localparam      F_LGDEPTH=2;

        reg     f_past_valid;

        wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks,

                                        f_outstanding;

        reg     [(AW-1):0]       f_last_pc;

        reg                     f_last_pc_valid;

        reg     [(AW-1):0]       f_req_addr;

//

//

// Generic setup

//

//

`ifdef  PREFETCH

`define ASSUME  assume

`else

`define ASSUME  assert

`endif

        // Assume a clock

        // Keep track of a flag telling us whether or not $past()

        // will return valid results

        initial f_past_valid = 1'b0;

        always @(posedge i_clk)

                f_past_valid = 1'b1;

        /////////////////////////////////////////////////

        //

        //

        // Assumptions about our inputs

        //

        //

        /////////////////////////////////////////////////

        // Assume we start from a reset condition

        initial `ASSUME(i_reset);

        always @(*)

        if (!f_past_valid)

                `ASSUME(i_reset);

        // Some things to know from the CPU ... there will always be a

        // i_new_pc request following any reset

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(i_reset)))

                `ASSUME(i_new_pc);

        // There will also be a i_new_pc request following any request to clear

        // the cache.

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(i_clear_cache)))

                `ASSUME(i_new_pc);

        //

        //

        // Let's make some assumptions about how long it takes our

        // phantom bus and phantom CPU to respond.

        //

        // These delays need to be long enough to flush out any potential

        // errors, yet still short enough that the formal method doesn't

        // take forever to solve.

        //

        localparam      F_CPU_DELAY = 4;

        reg     [4:0]    f_cpu_delay;

        // First, let's assume that any response from the bus comes back

        // within F_WB_DELAY clocks

                // Here's our delay assumption: We'll assume that the

        // wishbone will always respond within F_WB_DELAY clock ticks

        // of the beginning of any cycle.

        //

        // This includes both dropping the stall line, as well as

        // acknowledging any request.  While this may not be

        // a reasonable assumption for a piped master, it should

        // work here for us.

        // Count the number of clocks it takes the CPU to respond to our

        // instruction.

        always @(posedge i_clk)

        // If no instruction is ready, then keep our counter at zero

        if ((i_reset)||(!o_valid)||(i_stalled_n))

                f_cpu_delay <= 0;

        else

                // Otherwise, count the clocks the CPU takes to respond

                f_cpu_delay <= f_cpu_delay + 1'b1;

`ifdef  PREFETCH

        // Only *assume* that we are less than F_CPU_DELAY if we are not

        // integrated into the CPU

        always @(posedge i_clk)

                assume(f_cpu_delay < F_CPU_DELAY);

`endif

        fwb_master #(.AW(AW), .DW(DW),.F_LGDEPTH(F_LGDEPTH),

                        .F_MAX_REQUESTS(1), .F_OPT_SOURCE(1),

                        .F_OPT_RMW_BUS_OPTION(0),

                        .F_OPT_DISCONTINUOUS(0))

                f_wbm(i_clk, i_reset,

                        o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, 4'h0,

                        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,

                        f_nreqs, f_nacks, f_outstanding);

        /////////////////////////////////////////////////

        //

        //

        // Assertions about our outputs

        //

        //

        /////////////////////////////////////////////////

        //

        // Assertions about our wishbone control outputs first

        // Prefetches don't write

        always @(posedge i_clk)

        if (o_wb_stb)

                assert(!o_wb_we);

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(f_past_valid))

                        &&($past(i_clear_cache,2))

                        &&($past(o_wb_cyc,2)))

                // Make sure any clear-cache transaction is aborted,

                // *and* that no valid instructions get sent to the

                // CPU

                assert((!$past(o_wb_cyc))||(!o_wb_cyc));

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_valid))&&(o_valid))

                assert(o_wb_addr == $past(o_wb_addr));

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(!i_reset))&&($past(invalid)))

                assert(o_wb_cyc);

        // Any time the CPU accepts an instruction, assert that on the

        // valid line will be low on the next clock

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_valid))&&($past(i_stalled_n)))

                assert(!o_valid);

        // Since we only change our output on a response from the bus, we

        // need to insist that the item has been read by the CPU before

        // we go looking/asking for a next value.

        //

        // This routine should never be requesting a new instruction when

        // one is valid--lest the CPU never accept the old instruction and we

        // have nothing to do with the data when the bus request returns.

        always @(*)

        if (o_wb_cyc)

                assert(!o_valid);

        // If we just got a valid instruction from the wishbone, assert that

        // the instruction is listed as valid on the next instruction cycle

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(i_reset))

                &&($past(o_wb_cyc))

                &&($past(!i_clear_cache))

                &&($past(i_wb_ack))&&(!$past(i_wb_err)))

        begin

                if (!invalid)

                        assert(o_valid);

        end

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(i_clear_cache)))

                assert(!o_valid);

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(f_past_valid))

                        &&($past(i_clear_cache,2))

                        &&($past(o_wb_cyc,2)))

                // Make sure any clear-cache transaction is aborted,

                // *and* that no valid instructions get sent to the

                // CPU

                assert(!o_valid);

        //

        // Assertions about our return responses

        //

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(i_reset))

                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))

                        &&($past(o_valid))&&(!$past(i_stalled_n)))

                assert(o_valid == $past(o_valid));

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_valid))&&(o_valid))

        begin

                assert($stable(o_pc));

                assert($stable(o_insn));

                assert($stable(o_illegal));

        end

        //

        // The o_illegal line is the one we use to remind us not to go

        // back and retry the last value if it returned a bus error.  Hence,

        // let's assert that this line stays constant any time o_wb_cyc

        // is low, and we haven't received any new requests.

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(i_reset))

                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))

                        &&($past(!o_wb_cyc)))

                assert(o_illegal == $past(o_illegal));

        //

        //

        // Let's examine whether or not we "walk" though PC addresses one

        // at a time like we expect.

        //

        initial f_last_pc_valid = 1'b0;

        always @(posedge i_clk)

        if ((i_reset)||(i_clear_cache)||(i_new_pc)||(invalid))

                f_last_pc_valid <= 1'b0;

        else if (o_valid)

                f_last_pc_valid <= (!o_illegal);

        // initial      f_last_pc = 0;

        always @(posedge i_clk)

        if (o_valid)

                f_last_pc  <= o_pc[AW+1:2];

        else if (f_last_pc_valid)

                assert(o_pc[AW+1:2] == f_last_pc + 1'b1);

        always @(*)

                assert(o_pc[1:0] == 2'b00);

        // If we are producing a new result, and no new-pc or clear cache

        // has come through (i.e. f_last_pc_valid is true), then the resulting

        // PC should be one more than the last time.

        //

        // The o_valid && !$past(o_valid) is necessary because f_last_pc_valid

        // will be different by the second o_valid.

        always @(posedge i_clk)

        if ((f_past_valid)&&(o_valid)

                        &&(!$past(o_valid))&&(f_last_pc_valid))

                assert(o_pc[AW+1:2] == (f_last_pc + 1'b1));

        // Let's also keep track of the address the CPU wants us to return.

        // Any time the CPU branches to a new_pc, we'll record that request.

        // Likewise, any time an instruction is returned from the bus,

        // we'll increment this address so as to automatically walk through

        // memory.

        //

        always @(*)

                assume(i_pc[1:0] == 2'b00);

        initial f_req_addr = 0;

        always @(posedge i_clk)

        if (i_new_pc)

                f_req_addr <= i_pc[AW+1:2];

        else if ((!invalid)&&(o_wb_cyc)&&(i_wb_ack)&&(!i_wb_err))

                f_req_addr <= f_req_addr + 1'b1;

        // Let's also keep the formal methods on track.  Any time we are

        // requesting a value, it should either be from the req_addr, or if

        // not a new value should've come in rendering this one invalid.

        always @(posedge i_clk)

        if (o_wb_cyc)

                assert((invalid)||(f_req_addr == o_wb_addr));

        // This isn't good enough for induction, so we'll need to

        // constrain this further

        else if ((!o_valid)&&(!i_new_pc)&&(!i_reset))

                assert(f_req_addr == o_wb_addr);

        // In this version, invalid should only ever be high for one cycle.

        // CYC should be high on the cycle following--if ever.

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(invalid)))

                assert(!invalid);

        (* anyconst *) reg      [AW:0]           const_addr;

        (* anyconst *) reg      [DW-1:0] const_insn;

        wire    f_this_addr, f_this_pc, f_this_req, f_this_data;

        assign  f_this_addr = (o_wb_addr ==   const_addr[AW-1:0]);

        assign  f_this_pc   = (o_pc      == { const_addr[AW-1:0], 2'b00 });

        assign  f_this_req  = (i_pc      == { const_addr[AW-1:0], 2'b00 });

        assign  f_this_data = (i_wb_data ==   const_insn);

        reg     f_addr_pending;

        initial f_addr_pending = 1'b0;

        always @(posedge i_clk)

        if (i_reset)

                f_addr_pending <= 1'b0;

        else if (!o_wb_cyc)

                f_addr_pending <= 1'b0;

        else if ((o_wb_stb)&&(f_this_addr))

        begin

                if ((!i_wb_ack)&&(!i_wb_err))

                        f_addr_pending <= 1'b1;

        end

        always @(*)

        if ((o_wb_stb)&&(f_this_addr)&&(!i_wb_stall))

        begin

                if (!const_addr[AW])

                        assume(!i_wb_err);

                else

                        assume(!i_wb_ack);

                if (i_wb_ack)

                        assume(f_this_data);

        end else if ((o_wb_cyc)&&(f_addr_pending))

        begin

                if (!const_addr[AW])

                        assume(!i_wb_err);

                else

                        assume(!i_wb_ack);

                if (i_wb_ack)

                        assume(f_this_data);

        end

        always @(*)

        if ((o_valid)&&(f_this_pc)&&(!o_illegal))

                assert(o_insn == const_insn);

        always @(*)

        if ((o_valid)&&(f_this_pc))

                assert(o_illegal == const_addr[AW]);

        reg     f_insn_pending;

        initial f_insn_pending = 1'b0;

        always @(posedge i_clk)

        if (i_reset)

                f_insn_pending <= 1'b0;

        else if (i_clear_cache)

                f_insn_pending <= 1'b0;

        else if ((i_new_pc)&&(f_this_req))

                f_insn_pending <= 1'b1;

        else if ((o_valid)||(i_new_pc))

                f_insn_pending <= 1'b0;

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc)&&(f_insn_pending))

                assert(f_this_pc);

        always @(posedge i_clk)

        if (((f_past_valid)&&($past(o_wb_cyc))&&($past(f_insn_pending)))

                &&(!$past(i_reset))&&(!$past(i_clear_cache))

                &&(!$past(i_new_pc)))

        begin

                if(!o_wb_cyc)

                        assert((o_valid)&&(f_this_pc));

        end

        always @(posedge i_clk)

        if ((f_past_valid)&&(!$past(o_wb_cyc))&&(!o_wb_cyc))

                assert(!f_insn_pending);

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc)&&(f_this_addr))

                assert(f_addr_pending);

        always @(posedge i_clk)

        if ((f_past_valid)&&($past(o_wb_cyc))&&(f_insn_pending))

                assert(f_this_addr);

`endif

endmodule

//

// Usage:       (this)  (mid)   (past)

//    Cells     167     230     175

//      FDRE     67      97      69

//      LUT1      1       1       1

//      LUT2      1       3       3

//      LUT3     31      63      33

//      LUT4      5       3       3

//      LUT5      1       3       3

//      LUT6      2       1       3

//      MUXCY    29      29      31

//      XORCY    30      30      32