OpenCores
URL https://opencores.org/ocsvn/zipcpu/zipcpu/trunk

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [core/] [dblfetch.v] - Diff between revs 205 and 209

Show entire file | Details | Blame | View Log

Rev 205 Rev 209
Line 4... Line 4...
//
//
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
//
//
// Purpose:     This is one step beyond the simplest instruction fetch,
// Purpose:     This is one step beyond the simplest instruction fetch,
//              prefetch.v.  dblfetch.v uses memory pipelining to fetch two
//              prefetch.v.  dblfetch.v uses memory pipelining to fetch two
//      instruction words in one cycle, figuring that the unpipelined CPU can't
//      (or more) instruction words in one bus cycle.  If the CPU consumes
//      go through both at once, but yet recycles itself fast enough for the
//      either of these before the bus cycle completes, a new request will be
//      next instruction that would follow.  It is designed to be a touch
//      made of the bus.  In this way, we can keep the CPU filled in spite
//      faster than the single instruction prefetch, although not as fast as
//      of a (potentially) slow memory operation.  The bus request will end
//      the prefetch and cache found elsewhere.
//      when both requests have been sent and both result locations are empty.
//
//
//      There are some gotcha's in this logic, however.  For example, it's 
//      This routine is designed to be a touch faster than the single
//      illegal to switch devices mid-transaction, since the second device
//      instruction prefetch (prefetch.v), although not as fast as the
//      might have different timing.  I.e. the first device might take 8
//      prefetch and cache approach found elsewhere (pfcache.v).
//      clocks to create an ACK, and the second device might take 2 clocks, the
 
//      acks might therefore come on top of each other, or even out of order.
 
//      But ... in order to keep logic down, we keep track of the PC in the
 
//      o_wb_addr register.  Hence, this register gets changed on any i_new_pc.
 
//      The i_pc value associated with i_new_pc will only be valid for one
 
//      clock, hence we can't wait to change.  To keep from violating the WB
 
//      rule, therefore, we *must* immediately stop requesting any transaction,
 
//      and then terminate the bus request as soon as possible.
 
//
 
//      This has consequences in terms of logic used, leaving this routine
 
//      anything but simple--even though the number of wires affected by
 
//      this is small (o_wb_cyc, o_wb_stb, and last_ack).
 
//
//
 
//      20180222: Completely rebuilt.
//
//
// Creator:     Dan Gisselquist, Ph.D.
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//              Gisselquist Technology, LLC
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
// Copyright (C) 2017, Gisselquist Technology, LLC
// Copyright (C) 2017-2019, Gisselquist Technology, LLC
//
//
// This program is free software (firmware): you can redistribute it and/or
// 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
// 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// your option) any later version.
Line 56... Line 45...
//
//
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
//
//
module  dblfetch(i_clk, i_rst, i_new_pc, i_clear_cache,
`default_nettype        none
                        i_stall_n, i_pc, o_i, o_pc, o_v,
//
 
module  dblfetch(i_clk, i_reset, i_new_pc, i_clear_cache,
 
                        i_stall_n, i_pc, o_insn, o_pc, o_valid,
                o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
                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,
                        i_wb_ack, i_wb_stall, i_wb_err, i_wb_data,
                o_illegal);
                o_illegal);
        parameter               ADDRESS_WIDTH=32, AUX_WIDTH = 1;
        parameter               ADDRESS_WIDTH=30, AUX_WIDTH = 1;
        localparam              AW=ADDRESS_WIDTH;
        localparam              AW=ADDRESS_WIDTH, DW = 32;
        input                           i_clk, i_rst, i_new_pc, i_clear_cache,
        input   wire                    i_clk, i_reset, i_new_pc, i_clear_cache,
                                                i_stall_n;
                                                i_stall_n;
        input           [(AW-1):0]       i_pc;
        input   wire    [(AW+1):0]       i_pc;
        output  reg     [31:0]           o_i;
        output  reg     [(DW-1):0]       o_insn;
        output  reg     [(AW-1):0]       o_pc;
        output  reg     [(AW+1):0]       o_pc;
        output  wire                    o_v;
        output  reg                     o_valid;
        // Wishbone outputs
        // Wishbone outputs
        output  reg                     o_wb_cyc, o_wb_stb;
        output  reg                     o_wb_cyc, o_wb_stb;
        output  wire                    o_wb_we;
        output  wire                    o_wb_we;
        output  reg     [(AW-1):0]       o_wb_addr;
        output  reg     [(AW-1):0]       o_wb_addr;
        output  wire    [31:0]           o_wb_data;
        output  wire    [(DW-1):0]       o_wb_data;
        // And return inputs
        // And return inputs
        input                   i_wb_ack, i_wb_stall, i_wb_err;
        input   wire                    i_wb_ack, i_wb_stall, i_wb_err;
        input           [31:0]   i_wb_data;
        input   wire    [(DW-1):0]       i_wb_data;
        // And ... the result if we got an error
        // And ... the result if we got an error
        output  reg             o_illegal;
        output  reg             o_illegal;
 
 
        assign  o_wb_we = 1'b0;
        assign  o_wb_we = 1'b0;
        assign  o_wb_data = 32'h0000;
        assign  o_wb_data = 32'h0000;
 
 
        reg     last_ack, last_stb, invalid_bus_cycle;
        reg     last_stb, invalid_bus_cycle;
 
 
        reg     [31:0]           cache   [0:1];
        reg     [(DW-1):0]       cache_word;
        reg     cache_read_addr, cache_write_addr;
        reg                     cache_valid;
        reg     [1:0]            cache_valid;
        reg     [1:0]            inflight;
 
        reg                     cache_illegal;
 
 
        initial o_wb_cyc = 1'b0;
        initial o_wb_cyc = 1'b0;
        initial o_wb_stb = 1'b0;
        initial o_wb_stb = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((i_rst)||(i_wb_err))
                if ((i_reset)||((o_wb_cyc)&&(i_wb_err)))
                begin
                begin
                        o_wb_cyc <= 1'b0;
                        o_wb_cyc <= 1'b0;
                        o_wb_stb <= 1'b0;
                        o_wb_stb <= 1'b0;
                        // last_stb <= 1'b0;
 
                        // last_ack <= 1'b0;
 
                end else if (o_wb_cyc)
                end else if (o_wb_cyc)
                begin
                begin
                        if ((o_wb_stb)&&(!i_wb_stall))
                        if ((!o_wb_stb)||(!i_wb_stall))
                        begin
                                o_wb_stb <= (!last_stb);
                                // last_stb <= 1'b1;
 
                                o_wb_stb <= !last_stb;
 
                        end
 
                        // if (i_wb_ack)
 
                        //      last_ack <= 1'b1;
 
                        if ((i_new_pc)||(invalid_bus_cycle))
 
                                o_wb_stb <= 1'b0;
 
 
 
                        if ((i_wb_ack)&&(
 
                                // Relase the bus on the second ack
                                // Relase the bus on the second ack
                                (last_ack)
                        if (((i_wb_ack)&&(!o_wb_stb)&&(inflight<=1))
                                // Or on the first ACK, if we've been told
                                ||((!o_wb_stb)&&(inflight == 0))
                                // we have an invalid bus cycle
                                // Or any new transaction request
                                ||((o_wb_stb)&&(i_wb_stall)&&(last_stb)&&(
                                ||((i_new_pc)||(i_clear_cache)))
                                        (i_new_pc)||(invalid_bus_cycle)))
 
                                ))
 
                        begin
                        begin
                                o_wb_cyc <= 1'b0;
                                o_wb_cyc <= 1'b0;
                                o_wb_stb <= 1'b0;
                                o_wb_stb <= 1'b0;
                        end
                        end
 
 
                        if ((!last_stb)&&(i_wb_stall)&&((i_new_pc)||(invalid_bus_cycle)))
                end else if ((i_new_pc)||(invalid_bus_cycle)
                                // Also release the bus with no acks, if we
                        ||((o_valid)&&(i_stall_n)&&(!o_illegal)))
                                // haven't made any requests
 
                        begin
 
                                o_wb_cyc <= 1'b0;
 
                                o_wb_stb <= 1'b0;
 
                        end
 
                end else if ((invalid_bus_cycle)
 
                        ||((o_v)&&(i_stall_n)&&(cache_read_addr))) // Initiate a bus cycle
 
                begin
                begin
 
                        // Initiate a bus cycle if ... the last bus cycle was
 
                        // aborted (bus error or new_pc), we've been given a
 
                        // new PC to go get, or we just exhausted our one
 
                        // instruction cache
                        o_wb_cyc <= 1'b1;
                        o_wb_cyc <= 1'b1;
                        o_wb_stb <= 1'b1;
                        o_wb_stb <= 1'b1;
                        // last_stb <= 1'b0;
 
                        // last_ack <= 1'b0;
 
                end
                end
 
 
        initial last_stb = 1'b0;
        initial inflight = 2'b00;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((o_wb_cyc)&&(o_wb_stb)&&(!i_wb_stall))
        if (!o_wb_cyc)
                        last_stb <= 1'b1;
                inflight <= 2'b00;
                else if (!o_wb_cyc)
        else begin
                        last_stb <= 1'b0;
                case({ ((o_wb_stb)&&(!i_wb_stall)), i_wb_ack })
 
                2'b01:  inflight <= inflight - 1'b1;
 
                2'b10:  inflight <= inflight + 1'b1;
 
                // If neither ack nor request, then no change.  Likewise
 
                // if we have both an ack and a request, there's no change
 
                // in the number of requests in flight.
 
                default: begin end
 
                endcase
 
        end
 
 
        initial last_ack = 1'b0;
        always @(*)
        always @(posedge i_clk)
                last_stb = (inflight != 2'b00)||((o_valid)&&(!i_stall_n));
                if ((o_wb_cyc)&&(i_wb_ack))
 
                        last_ack <= 1'b1;
 
                else if ((o_wb_cyc)&&(o_wb_stb)&&(i_wb_stall)&&(
 
                                (i_new_pc)||(invalid_bus_cycle)))
 
                        last_ack <= 1'b1;
 
                else if ((o_wb_cyc)&&(o_wb_stb)&&(!i_wb_stall)&&(!last_stb)&&(
 
                                (i_new_pc)||(invalid_bus_cycle)))
 
                        last_ack <= 1'b1;
 
                else if (!o_wb_cyc)
 
                        last_ack <= 1'b0;
 
 
 
        initial invalid_bus_cycle = 1'b0;
        initial invalid_bus_cycle = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_rst)
                if ((o_wb_cyc)&&(i_new_pc))
                        invalid_bus_cycle <= 1'b0;
 
                else if ((i_new_pc)||(i_clear_cache))
 
                        invalid_bus_cycle <= 1'b1;
                        invalid_bus_cycle <= 1'b1;
                else if (!o_wb_cyc)
                else if (!o_wb_cyc)
                        invalid_bus_cycle <= 1'b0;
                        invalid_bus_cycle <= 1'b0;
 
 
        initial o_wb_addr = {(AW){1'b1}};
        initial o_wb_addr = {(AW){1'b1}};
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_new_pc)
                if (i_new_pc)
                        o_wb_addr <= i_pc;
                        o_wb_addr <= i_pc[AW+1:2];
                else if ((o_wb_stb)&&(!i_wb_stall)&&(!invalid_bus_cycle))
                else if ((o_wb_stb)&&(!i_wb_stall))
                        o_wb_addr <= o_wb_addr + 1'b1;
                        o_wb_addr <= o_wb_addr + 1'b1;
 
 
        initial cache_write_addr = 1'b0;
        //////////////////
 
        //
 
        // Now for the immediate output word to the CPU
 
        //
 
        //////////////////
 
 
 
        initial o_valid = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (!o_wb_cyc)
                if ((i_reset)||(i_new_pc)||(i_clear_cache))
                        cache_write_addr <= 1'b0;
                        o_valid <= 1'b0;
                else if ((o_wb_cyc)&&(i_wb_ack))
                else if ((o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
                        cache_write_addr <= cache_write_addr + 1'b1;
                        o_valid <= 1'b1;
 
                else if (i_stall_n)
 
                        o_valid <= cache_valid;
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((o_wb_cyc)&&(i_wb_ack))
        if ((!o_valid)||(i_stall_n))
                        cache[cache_write_addr] <= i_wb_data;
        begin
 
                if (cache_valid)
 
                        o_insn <= cache_word;
 
                else
 
                        o_insn <= i_wb_data;
 
        end
 
 
        initial cache_read_addr = 1'b0;
        initial o_pc[1:0] = 2'b00;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((i_new_pc)||(invalid_bus_cycle)
        if (i_new_pc)
                                ||((o_v)&&(cache_read_addr)&&(i_stall_n)))
                o_pc <= i_pc;
                        cache_read_addr <= 1'b0;
        else if ((o_valid)&&(i_stall_n))
                else if ((o_v)&&(i_stall_n))
                o_pc[AW+1:2] <= o_pc[AW+1:2] + 1'b1;
                        cache_read_addr <= 1'b1;
 
 
 
 
        initial o_illegal = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((i_new_pc)||(invalid_bus_cycle))
                if ((i_reset)||(i_new_pc)||(i_clear_cache))
                        cache_valid <= 2'b00;
                        o_illegal <= 1'b0;
 
                else if ((!o_valid)||(i_stall_n))
 
                begin
 
                        if (cache_valid)
 
                                o_illegal <= (o_illegal)||(cache_illegal);
 
                        else if ((o_wb_cyc)&&(i_wb_err))
 
                                o_illegal <= 1'b1;
 
                end
 
 
 
 
 
        //////////////////
 
        //
 
        // Now for the output/cached word
 
        //
 
        //////////////////
 
 
 
        initial cache_valid = 1'b0;
 
        always @(posedge i_clk)
 
                if ((i_reset)||(i_new_pc)||(i_clear_cache))
 
                        cache_valid <= 1'b0;
                else begin
                else begin
                        if ((o_v)&&(i_stall_n))
                        if ((o_valid)&&(o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
                                cache_valid[cache_read_addr] <= 1'b0;
                                cache_valid <= (!i_stall_n)||(cache_valid);
 
                        else if (i_stall_n)
 
                                cache_valid <= 1'b0;
 
                end
 
 
 
        always @(posedge i_clk)
                        if ((o_wb_cyc)&&(i_wb_ack))
                        if ((o_wb_cyc)&&(i_wb_ack))
                                cache_valid[cache_write_addr] <= 1'b1;
                        cache_word <= i_wb_data;
 
 
 
        initial cache_illegal = 1'b0;
 
        always @(posedge i_clk)
 
        if ((i_reset)||(i_clear_cache)||(i_new_pc))
 
                cache_illegal <= 1'b0;
 
        else if ((o_wb_cyc)&&(i_wb_err)&&(o_valid)&&(!i_stall_n))
 
                cache_illegal <= 1'b1;
 
//
 
// Some of these properties can be done in yosys-smtbmc, *or* Verilator
 
//
 
// Ver1lator is different from yosys, however, in that Verilator doesn't support
 
// the $past() directive.  Further, any `assume`'s turn into `assert()`s
 
// within Verilator.  We can use this to help prove that the properties
 
// of interest truly hold, and that any contracts we create or assumptions we
 
// make truly hold in practice (i.e. in simulation).
 
//
 
`ifdef  FORMAL
 
`define VERILATOR_FORMAL
 
`else
 
`ifdef  VERILATOR
 
//
 
// Define VERILATOR_FORMAL here to have Verilator check your formal properties
 
// during simulation.  assert() and assume() statements will both have the
 
// same effect within VERILATOR of causing your simulation to suddenly end.
 
//
 
// I have this property commented because it only works on the newest versions
 
// of Verilator (3.9 something and later), and I tend to still use Verilator
 
// 3.874.
 
//
 
// `define      VERILATOR_FORMAL
 
`endif
 
`endif
 
 
 
`ifdef  VERILATOR_FORMAL
 
        // Keep track of a flag telling us whether or not $past()
 
        // will return valid results
 
        reg     f_past_valid;
 
        initial f_past_valid = 1'b0;
 
        always @(posedge i_clk)
 
                f_past_valid = 1'b1;
 
 
 
        // Keep track of some alternatives to $past that can still be used
 
        // in a VERILATOR environment
 
        reg     f_past_reset, f_past_clear_cache, f_past_o_valid,
 
                f_past_stall_n;
 
 
 
        initial f_past_reset = 1'b1;
 
        initial f_past_clear_cache = 1'b0;
 
        initial f_past_o_valid = 1'b0;
 
        initial f_past_stall_n = 1'b1;
 
        always @(posedge i_clk)
 
        begin
 
                f_past_reset       <= i_reset;
 
                f_past_clear_cache <= i_clear_cache;
 
                f_past_o_valid     <= o_valid;
 
                f_past_stall_n     <= i_stall_n;
                end
                end
 
`endif
 
 
        initial o_i = {(32){1'b1}};
`ifdef  FORMAL
 
//
 
//
 
// Generic setup
 
//
 
//
 
`ifdef  DBLFETCH
 
`define ASSUME  assume
 
`else
 
`define ASSUME  assert
 
`endif
 
 
 
        /////////////////////////////////////////////////
 
        //
 
        //
 
        // Assumptions about our inputs
 
        //
 
        //
 
        /////////////////////////////////////////////////
 
 
 
        always @(*)
 
        if (!f_past_valid)
 
                `ASSUME(i_reset);
 
 
 
        //
 
        // Assume that resets, new-pc commands, and clear-cache commands
 
        // are never more than pulses--one clock wide at most.
 
        //
 
        // It may be that the CPU treats us differently.  We'll only restrict
 
        // our solver to this here.
 
/*
 
        always @(posedge i_clk)
 
        if (f_past_valid)
 
        begin
 
                if (f_past_reset)
 
                        restrict(!i_reset);
 
                if ($past(i_new_pc))
 
                        restrict(!i_new_pc);
 
        end
 
*/
 
 
 
        //
 
        // Assume we start from a reset condition
 
        initial assume(i_reset);
 
 
 
        /////////////////////////////////////////////////
 
        //
 
        //
 
        // Wishbone bus properties
 
        //
 
        //
 
        /////////////////////////////////////////////////
 
 
 
        localparam      F_LGDEPTH=2;
 
        wire    [(F_LGDEPTH-1):0]        f_nreqs, f_nacks, f_outstanding;
 
 
 
        //
 
        // Add a bunch of wishbone-based asserts
 
        fwb_master #(.AW(AW), .DW(DW), .F_LGDEPTH(F_LGDEPTH),
 
                                .F_MAX_STALL(2),
 
                                .F_MAX_REQUESTS(0), .F_OPT_SOURCE(1),
 
                                .F_OPT_RMW_BUS_OPTION(1),
 
                                .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);
 
 
 
`endif
 
 
 
//
 
// Now, apply the following to Verilator *or* yosys-smtbmc
 
//
 
`ifdef  VERILATOR_FORMAL
 
        /////////////////////////////////////////////////
 
        //
 
        //
 
        // Assumptions about our interaction with the CPU
 
        //
 
        //
 
        /////////////////////////////////////////////////
 
 
 
        // Assume that any reset is either accompanied by a new address,
 
        // or a new address immediately follows it.
 
        always @(posedge i_clk)
 
                if ((f_past_valid)&&(f_past_reset))
 
                        assume(i_new_pc);
 
 
 
        always @(posedge i_clk)
 
        if (f_past_clear_cache)
 
                assume(!i_clear_cache);
 
 
 
        //
 
        //
 
        // The bottom two bits of the PC address register are always zero.
 
        // They are there to make examining traces easier, but I expect
 
        // the synthesis tool to remove them.
 
        //
 
        always @(*)
 
                assume(i_pc[1:0] == 2'b00);
 
 
 
        // 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)&&(f_past_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)&&(f_past_clear_cache))
 
                        assume(i_new_pc);
 
 
 
        always @(posedge i_clk)
 
        if (f_past_clear_cache)
 
                assume(!i_clear_cache);
 
 
 
        always @(*)
 
                assume(i_pc[1:0] == 2'b00);
 
`endif
 
 
 
`ifdef  FORMAL
 
        //
 
        // Let's make some assumptions about how long it takes our phantom
 
        // (i.e. assumed) CPU to respond.
 
        //
 
        // This delay needs to be long enough to flush out any potential
 
        // errors, yet still short enough that the formal method doesn't
 
        // take forever to solve.
 
        //
 
`ifdef  DBLFETCH
 
        localparam      F_CPU_DELAY = 4;
 
        reg     [4:0]    f_cpu_delay;
 
 
 
        // Now, let's look at the delay the CPU takes to accept an instruction.
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((i_stall_n)&&(o_wb_cyc)&&(i_wb_ack))
                // If no instruction is ready, then keep our counter at zero
                        o_i <= i_wb_data;
                if ((!o_valid)||(i_stall_n))
 
                        f_cpu_delay <= 0;
                else
                else
                        o_i <= cache[cache_read_addr];
                        // Otherwise, count the clocks the CPU takes to respond
 
                        f_cpu_delay <= f_cpu_delay + 1'b1;
 
 
        initial o_pc = 0;
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_new_pc)
                assume(f_cpu_delay < F_CPU_DELAY);
                        o_pc <= i_pc;
`endif
                else if ((o_v)&&(i_stall_n))
 
                        o_pc <= o_pc + 1'b1;
 
 
 
        assign  o_v = cache_valid[cache_read_addr];
 
 
 
        initial o_illegal = 1'b0;
 
 
        /////////////////////////////////////////////////
 
        //
 
        //
 
        // Assertions about our outputs
 
        //
 
        //
 
        /////////////////////////////////////////////////
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((o_wb_cyc)&&(i_wb_err))
        if ((f_past_valid)&&($past(o_wb_stb))&&(!$past(i_wb_stall))
                        o_illegal <= 1'b1;
                        &&(!$past(i_new_pc)))
                else if ((!o_wb_cyc)&&((i_new_pc)||(invalid_bus_cycle)))
                assert(o_wb_addr <= $past(o_wb_addr)+1'b1);
                        o_illegal <= 1'b0;
 
 
 
 
        //
 
        // Assertions about our return responses to the CPU
 
        //
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))
 
                        &&($past(o_valid))&&(!$past(i_stall_n)))
 
        begin
 
                assert($stable(o_pc));
 
                assert($stable(o_insn));
 
                assert($stable(o_valid));
 
                assert($stable(o_illegal));
 
        end
 
 
 
        // The same is true of the cache as well.
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))
 
                        &&($past(o_valid))&&(!$past(i_stall_n))
 
                        &&($past(cache_valid)))
 
        begin
 
                assert($stable(cache_valid));
 
                assert($stable(cache_word));
 
                assert($stable(cache_illegal));
 
        end
 
 
 
        // Consider it invalid to present the CPU with the same instruction
 
        // twice in a row.  Any effort to present the CPU with the same
 
        // instruction twice in a row must go through i_new_pc, and thus a
 
        // new bus cycle--hence the assertion below makes sense.
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_new_pc))
 
                        &&($past(o_valid))&&($past(i_stall_n)))
 
                assert(o_pc[AW+1:2] == $past(o_pc[AW+1:2])+1'b1);
 
 
 
 
 
        //
 
        // As with i_pc[1:0], the bottom two bits of the address are unused.
 
        // Let's assert here that they remain zero.
 
        always @(*)
 
                assert(o_pc[1:0] == 2'b00);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                        &&(!$past(i_new_pc))
 
                        &&(!$past(i_clear_cache))
 
                        &&($past(o_wb_cyc))&&($past(i_wb_err)))
 
                assert( ((o_valid)&&(o_illegal))
 
                        ||((cache_valid)&&(cache_illegal)) );
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(o_illegal))&&(o_illegal))
 
                assert(o_valid);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(cache_illegal))&&(!cache_valid))
 
                assert(!cache_illegal);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_new_pc)))
 
                assert(!o_valid);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_clear_cache))
 
                        &&($past(o_valid))&&(!o_valid)&&(!o_illegal))
 
                assert((o_wb_cyc)||(invalid_bus_cycle));
 
 
 
        /////////////////////////////////////////////////
 
        //
 
        //
 
        // Our "contract" with the CPU
 
        //
 
        //
 
        /////////////////////////////////////////////////
 
        //
 
        // For any particular address, that address is associated with an
 
        // instruction and a flag regarding whether or not it is illegal.
 
        //
 
        // Any attempt to return to the CPU a value from this address,
 
        // must return the value and the illegal flag.
 
        //
 
        (* anyconst *) reg      [AW-1:0] f_const_addr;
 
        (* anyconst *) reg      [DW-1:0] f_const_insn;
 
        (* anyconst *) reg                      f_const_illegal;
 
 
 
        //
 
        // While these wires may seem like overkill, and while they make the
 
        // following logic perhaps a bit more obscure, these predicates make
 
        // it easier to follow the complex logic on a scope.  They don't
 
        // affect anything synthesized.
 
        //
 
        wire    f_this_addr, f_this_pc, f_this_req, f_this_data,
 
                f_this_insn;
 
 
 
        assign  f_this_addr = (o_wb_addr ==   f_const_addr);
 
        assign  f_this_pc   = (o_pc      == { f_const_addr, 2'b00 });
 
        assign  f_this_req  = (i_pc      == { f_const_addr, 2'b00 });
 
        assign  f_this_data = (i_wb_data ==   f_const_insn);
 
        assign  f_this_insn = (o_insn    ==   f_const_insn);
 
 
 
 
 
        //
 
        //
 
        // Here's our contract:
 
        //
 
        // Any time we return a value for the address above, it *must* be
 
        // the "right" value.
 
        //
 
        always @(*)
 
        if ((o_valid)&&(f_this_pc))
 
        begin
 
                if (f_const_illegal)
 
                        assert(o_illegal);
 
                if (!o_illegal)
 
                        assert(f_this_insn);
 
        end
 
 
 
        //
 
        // The contract will only work if we assume the return from the
 
        // bus at this address will be the right return.
 
        wire    f_this_return;
 
        assign  f_this_return = (o_wb_addr - f_outstanding == f_const_addr);
 
        always @(*)
 
        if ((o_wb_cyc)&&(f_this_return))
 
        begin
 
                if (i_wb_ack)
 
                        assume(i_wb_data == f_const_insn);
 
 
 
                if (f_const_illegal)
 
                        assume(!i_wb_ack);
 
                else
 
                        assume(!i_wb_err);
 
        end
 
 
 
        //
 
        // Here is a corrollary to our contract.  Anything in the one-word
 
        // cache must also match the contract as well.
 
        //
 
        always @(*)
 
        if ((o_pc[AW+1:2] + 1'b1 == f_const_addr)&&(cache_valid))
 
        begin
 
                if (!cache_illegal)
 
                        assert(cache_word == f_const_insn);
 
 
 
                if (f_const_illegal)
 
                        assert(cache_illegal);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(cache_illegal))&&(!cache_valid))
 
                assert(!cache_illegal);
 
 
 
        ////////////////////////////////////////////////////////
 
        //
 
        //
 
        // Additional assertions necessary to pass induction
 
        //
 
        //
 
        ////////////////////////////////////////////////////////
 
        //
 
        // We have only a one word cache.  Hence, we shouldn't be asking
 
        // for more data any time we have nowhere to put it.
 
        always @(*)
 
        if (o_wb_stb)
 
                assert((!cache_valid)||(i_stall_n));
 
 
 
        always @(*)
 
        if ((o_valid)&&(cache_valid))
 
                assert((f_outstanding == 0)&&(!o_wb_stb));
 
 
 
        always @(*)
 
        if ((o_valid)&&(!i_stall_n))
 
                assert(f_outstanding < 2);
 
 
 
        always @(*)
 
        if ((!o_valid)||(i_stall_n))
 
                assert(f_outstanding <= 2);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_wb_cyc))&&(!$past(o_wb_stb))
 
                        &&(o_wb_cyc))
 
                assert(inflight != 0);
 
 
 
        always @(*)
 
        if ((o_wb_cyc)&&(i_wb_ack))
 
                assert(!cache_valid);
 
 
 
        always @(posedge i_clk)
 
        if (o_wb_cyc)
 
                assert(inflight == f_outstanding);
 
 
 
        wire    [AW-1:0] this_return_address,
 
                                next_pc_address;
 
        assign  this_return_address = o_wb_addr - f_outstanding;
 
        assign  next_pc_address = o_pc[AW+1:2] + 1'b1;
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_wb_cyc))
 
                        &&(!$past(i_reset))
 
                        &&(!$past(i_new_pc))
 
                        &&(!$past(i_clear_cache))
 
                        &&(!$past(invalid_bus_cycle))
 
                        &&(($past(i_wb_ack))||($past(i_wb_err)))
 
                        &&((!$past(o_valid))||($past(i_stall_n)))
 
                        &&(!$past(cache_valid)))
 
                assert(o_pc[AW+1:2] == $past(this_return_address));
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_wb_cyc))&&(!o_valid)&&(!$past(i_new_pc))
 
                        &&(o_wb_cyc))
 
                assert(o_pc[AW+1:2] == this_return_address);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_wb_cyc))
 
                        &&(!$past(cache_valid))&&(cache_valid))
 
                assert(next_pc_address == $past(this_return_address));
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc))
 
        begin
 
                if ((o_valid)&&(!cache_valid))
 
                        assert(this_return_address == next_pc_address);
 
                else if (!o_valid)
 
                        assert(this_return_address == o_pc[AW+1:2]);
 
        end else if ((f_past_valid)&&(!invalid_bus_cycle)
 
                        &&(!o_wb_cyc)&&(o_valid)&&(!o_illegal)
 
                        &&(!cache_valid))
 
                assert(o_wb_addr == next_pc_address);
 
 
 
 
 
        always @(*)
 
        if (invalid_bus_cycle)
 
                assert(!o_wb_cyc);
 
        always @(*)
 
        if (cache_valid)
 
                assert(o_valid);
 
 
 
        /////////////////////////////////////////////////////
 
        //
 
        //
 
        // Cover statements
 
        //
 
        //
 
        /////////////////////////////////////////////////////
 
 
 
        always @(posedge i_clk)
 
        cover((f_past_valid)&&($past(f_nacks)==3)
 
                &&($past(i_wb_ack))&&($past(o_wb_cyc)));
 
 
 
 
 
        /////////////////////////////////////////////////////
 
        //
 
        //
 
        // Temporary simplifications
 
        //
 
        //
 
        /////////////////////////////////////////////////////
 
 
 
//      always @(*)
 
//              assume((!i_wb_err)&&(!f_const_illegal));
 
 
 
 
 
`endif  // FORMAL
endmodule
endmodule
 
//
 
// Usage:               (this)  (prior) (old)  (S6)
 
//    Cells             374     387     585     459
 
//      FDRE            135     108     203     171
 
//      LUT1              2       3       2
 
//      LUT2              9       3       4       5
 
//      LUT3             98      76     104      71
 
//      LUT4              2       0       2       2
 
//      LUT5              3      35      35       3
 
//      LUT6              6       5      10      43
 
//      MUXCY            58      62      93      62
 
//      MUXF7             1       0       2       3
 
//      MUXF8             0       1       1
 
//      RAM64X1D          0      32      32      32
 
//      XORCY            60      64      96      64
 
//
 
 
 No newline at end of file
 No newline at end of file

powered by: WebSVN 2.1.0

© copyright 1999-2021 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.