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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [core/] [dcache.v] - Diff between revs 201 and 209

Show entire file | Details | Blame | View Log

Rev 201 Rev 209
Line 46... Line 46...
// Creator:     Dan Gisselquist, Ph.D.
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//              Gisselquist Technology, LLC
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
// Copyright (C) 2016, Gisselquist Technology, LLC
// Copyright (C) 2016-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 65... Line 65...
//
//
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
//
//
module  dcache(i_clk, i_rst, i_pipe_stb, i_lock,
`default_nettype        none
 
//
 
//
 
`ifdef  FORMAL
 
`define ASSERT  assert
 
 
 
`ifdef DCACHE
 
`define ASSUME  assume
 
`else
 
`define ASSUME  assert
 
`endif
 
`endif
 
 
 
module  dcache(i_clk, i_reset, i_pipe_stb, i_lock,
                i_op, i_addr, i_data, i_oreg,
                i_op, i_addr, i_data, i_oreg,
                        o_busy, o_pipe_stalled, o_valid, o_err, o_wreg,o_data,
                        o_busy, o_pipe_stalled, o_valid, o_err, o_wreg,o_data,
                o_wb_cyc_gbl, o_wb_cyc_lcl, o_wb_stb_gbl, o_wb_stb_lcl,
                o_wb_cyc_gbl, o_wb_cyc_lcl, o_wb_stb_gbl, o_wb_stb_lcl,
                        o_wb_we, o_wb_addr, o_wb_data,
                        o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data);
                i_wb_ack, i_wb_stall, i_wb_err, i_wb_data
 
`ifdef  FORMAL
 
                , f_nreqs, f_nacks, f_outstanding, f_pc
 
`endif
 
        );
        parameter       LGCACHELEN = 8,
        parameter       LGCACHELEN = 8,
                        ADDRESS_WIDTH=32,
                        ADDRESS_WIDTH=30,
                        LGNLINES=5, // Log of the number of separate cache lines
                        LGNLINES=(LGCACHELEN-3), // Log of the number of separate cache lines
                        IMPLEMENT_LOCK=0,
 
                        NAUX=5; // # of aux d-wires to keep aligned w/memops
                        NAUX=5; // # of aux d-wires to keep aligned w/memops
        localparam      SDRAM_BIT = 26;
        parameter [0:0]   OPT_LOCAL_BUS=1'b1;
        localparam      FLASH_BIT = 22;
        parameter [0:0]   OPT_PIPE=1'b1;
        localparam      BLKRAM_BIT= 15;
        parameter [0:0]   OPT_LOCK=1'b1;
 
        parameter [0:0]   OPT_DUAL_READ_PORT=1'b1;
 
        parameter       OPT_FIFO_DEPTH = 4;
        localparam      AW = ADDRESS_WIDTH; // Just for ease of notation below
        localparam      AW = ADDRESS_WIDTH; // Just for ease of notation below
        localparam      CS = LGCACHELEN; // Number of bits in a cache address
        localparam      CS = LGCACHELEN; // Number of bits in a cache address
        localparam      LS = CS-LGNLINES; // Bits to spec position w/in cline
        localparam      LS = CS-LGNLINES; // Bits to spec position w/in cline
 
        parameter       F_LGDEPTH=1 + (((!OPT_PIPE)||(LS > OPT_FIFO_DEPTH))
 
                                        ? LS : OPT_FIFO_DEPTH);
        localparam      LGAUX = 3; // log_2 of the maximum number of piped data 
        localparam      LGAUX = 3; // log_2 of the maximum number of piped data 
        input                   i_clk, i_rst;
        localparam      DW = 32; // Bus data width
 
        localparam      DP = OPT_FIFO_DEPTH;
 
        //
 
        localparam [1:0] DC_IDLE  = 2'b00; // Bus is idle
 
        localparam [1:0] DC_WRITE = 2'b01; // Write
 
        localparam [1:0] DC_READS = 2'b10; // Read a single value(!cachd)
 
        localparam [1:0] DC_READC = 2'b11; // Read a whole cache line
 
        //
 
        input   wire            i_clk, i_reset;
        // Interface from the CPU
        // Interface from the CPU
        input                   i_pipe_stb, i_lock;
        input   wire            i_pipe_stb, i_lock;
        input                   i_op;
        input   wire [2:0]               i_op;
        input   [31:0]           i_addr;
        input   wire [(DW-1):0]  i_addr;
        input   [31:0]           i_data;
        input   wire [(DW-1):0]  i_data;
        input   [(NAUX-1):0]     i_oreg; // Aux data, such as reg to write to
        input   wire [(NAUX-1):0] i_oreg; // Aux data, such as reg to write to
        // Outputs, going back to the CPU
        // Outputs, going back to the CPU
        output  wire            o_busy, o_pipe_stalled, o_valid, o_err;
        output  reg             o_busy;
 
        output  reg             o_pipe_stalled;
 
        output  reg             o_valid, o_err;
        output reg [(NAUX-1):0]  o_wreg;
        output reg [(NAUX-1):0]  o_wreg;
        output  reg     [31:0]   o_data;
        output  reg [(DW-1):0]   o_data;
        // Wishbone bus master outputs
        // Wishbone bus master outputs
        output  wire            o_wb_cyc_gbl, o_wb_cyc_lcl;
        output  wire            o_wb_cyc_gbl, o_wb_cyc_lcl;
        output  reg             o_wb_stb_gbl, o_wb_stb_lcl;
        output  reg             o_wb_stb_gbl, o_wb_stb_lcl;
        output  reg             o_wb_we;
        output  reg             o_wb_we;
        output  reg     [(AW-1):0]       o_wb_addr;
        output  reg     [(AW-1):0]       o_wb_addr;
        output  reg     [31:0]           o_wb_data;
        output  reg [(DW-1):0]   o_wb_data;
 
        output  wire [(DW/8-1):0] o_wb_sel;
        // Wishbone bus slave response inputs
        // Wishbone bus slave response 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;
 
`ifdef FORMAL
 
        output  wire [(F_LGDEPTH-1):0]   f_nreqs, f_nacks, f_outstanding;
 
        output  wire                    f_pc;
 
 
 
        reg     f_past_valid;
 
`endif
 
        //
 
        // output       reg     [31:0]          o_debug;
 
 
 
 
        reg     cyc, stb, last_ack, end_of_line, last_line_stb;
        reg     cyc, stb, last_ack, end_of_line, last_line_stb;
 
        reg     r_wb_cyc_gbl, r_wb_cyc_lcl;
 
        // npending is the number of pending non-cached operations, counted
 
        // from the i_pipe_stb to the o_wb_ack
 
        reg     [DP:0]   npending;
 
 
 
 
        reg     [((1<<LGNLINES)-1):0] c_v;       // One bit per cache line, is it valid?
        reg     [((1<<LGNLINES)-1):0] c_v;       // One bit per cache line, is it valid?
        reg     [(AW-LS-1):0]    c_vtags [0:((1<<LGNLINES)-1)];
        reg     [(AW-LS-1):0]    c_vtags [0:((1<<LGNLINES)-1)];
        reg     [31:0]           c_mem   [0:((1<<CS)-1)];
        reg     [(DW-1):0]       c_mem   [0:((1<<CS)-1)];
        // reg  [((1<<LGNLINES)-1):0]   c_wr; // Is the cache line writable?
        reg                     set_vflag;
        // reg  c_wdata;
        reg     [1:0]            state;
        // reg  c_waddr;
        reg     [(CS-1):0]       wr_addr;
 
        reg     [(DW-1):0]       cached_idata, cached_rdata;
 
        reg     [DW-1:0] pre_data;
 
        reg                     lock_gbl, lock_lcl;
 
 
 
 
        // To simplify writing to the cache, and the job of the synthesizer to
        // To simplify writing to the cache, and the job of the synthesizer to
        // recognize that a cache write needs to take place, we'll take an extra
        // recognize that a cache write needs to take place, we'll take an extra
        // clock to get there, and use these c_w... registers to capture the
        // clock to get there, and use these c_w... registers to capture the
        // data in the meantime.
        // data in the meantime.
        reg                     c_wr;
        reg                     c_wr;
        reg     [31:0]           c_wdata;
        reg     [(DW-1):0]       c_wdata;
 
        reg     [(DW/8-1):0]     c_wsel;
        reg     [(CS-1):0]       c_waddr;
        reg     [(CS-1):0]       c_waddr;
 
 
        reg     [(AW-LS-1):0]    last_tag;
        reg     [(AW-LS-1):0]    last_tag;
 
        reg                     last_tag_valid;
 
 
 
 
        wire    [(LGNLINES-1):0] i_cline;
        wire    [(LGNLINES-1):0] i_cline;
        wire    [(CS-1):0]       i_caddr;
        wire    [(CS-1):0]       i_caddr;
        wire    [(AW-LS-1):0]    i_ctag;
 
 
 
        assign  i_cline = i_addr[(CS-1):LS];
`ifdef  FORMAL
        assign  i_caddr = i_addr[(CS-1):0];
        reg     [F_LGDEPTH-1:0]  f_fill;
        assign  i_ctag  = i_addr[(AW-1):LS];
        reg     [AW:0]           f_return_address;
 
        reg     [AW:0]           f_pending_addr;
 
`endif
 
 
 
        assign  i_cline = i_addr[(CS+1):LS+2];
 
        assign  i_caddr = i_addr[(CS+1):2];
 
 
        wire    cache_miss_inow, w_cachable;
        wire    cache_miss_inow, w_cachable;
        assign  cache_miss_inow = (last_tag != i_addr[31:LS])||(!c_v[i_cline]);
        assign  cache_miss_inow = (!last_tag_valid)
        assign  w_cachable = (i_addr[31:30]!=2'b11)&&(!i_lock)&&(
                                        ||(last_tag != i_addr[(AW+1):LS+2])
                                ((SDRAM_BIT>0)&&(i_addr[SDRAM_BIT]))
                                        ||(!c_v[i_cline]);
                                ||((FLASH_BIT>0)&&(i_addr[FLASH_BIT]))
 
                                ||((BLKRAM_BIT>0)&&(i_addr[BLKRAM_BIT])));
 
 
 
        reg     r_cachable, r_svalid, r_dvalid, r_rd, r_cache_miss, r_rvalid;
        wire    raw_cachable_address;
 
 
 
        iscachable chkaddress(i_addr[AW+1:2], raw_cachable_address);
 
 
 
        assign  w_cachable = ((!OPT_LOCAL_BUS)||(i_addr[(DW-1):(DW-8)]!=8'hff))
 
                &&((!i_lock)||(!OPT_LOCK))&&(raw_cachable_address);
 
 
 
        reg     r_cachable, r_svalid, r_dvalid, r_rd, r_cache_miss,
 
                r_rd_pending;
        reg     [(AW-1):0]       r_addr;
        reg     [(AW-1):0]       r_addr;
        reg     [31:0]           r_idata, r_ddata, r_rdata;
 
        wire    [(LGNLINES-1):0] r_cline;
        wire    [(LGNLINES-1):0] r_cline;
        wire    [(CS-1):0]       r_caddr;
        wire    [(CS-1):0]       r_caddr;
        wire    [(AW-LS-1):0]    r_ctag;
        wire    [(AW-LS-1):0]    r_ctag;
 
 
        assign  r_cline = r_addr[(CS-1):LS];
        assign  r_cline = r_addr[(CS-1):LS];
        assign  r_caddr = r_addr[(CS-1):0];
        assign  r_caddr = r_addr[(CS-1):0];
        assign  r_ctag  = r_addr[(AW-1):LS];
        assign  r_ctag  = r_addr[(AW-1):LS];
 
 
 
 
        reg     wr_cstb, r_iv, pipeable_op, non_pipeable_op, in_cache;
        reg     wr_cstb, r_iv, in_cache;
        reg     [(AW-LS-1):0]    r_itag;
        reg     [(AW-LS-1):0]    r_itag;
 
        reg     [DW/8-1:0]       r_sel;
 
        reg     [(NAUX+4-1):0]   req_data;
 
        reg                     gie;
 
 
 
 
 
 
        //
        //
        // The one-clock delayed read values from the cache.
        // The one-clock delayed read values from the cache.
        //
        //
        initial r_rd = 1'b0;
        initial r_rd = 1'b0;
        initial r_cachable = 1'b0;
        initial r_cachable = 1'b0;
        initial r_svalid = 1'b0;
        initial r_svalid = 1'b0;
        initial r_dvalid = 1'b0;
        initial r_dvalid = 1'b0;
 
        initial r_cache_miss = 1'b0;
 
        initial r_addr = 0;
 
        initial last_tag_valid = 0;
 
        initial r_rd_pending = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
        begin
        begin
 
                r_rd <= 1'b0;
 
                r_cachable <= 1'b0;
 
                r_svalid <= 1'b0;
 
                r_dvalid <= 1'b0;
 
                r_cache_miss <= 1'b0;
 
                r_addr <= 0;
 
                r_rd_pending <= 0;
 
                last_tag_valid <= 0;
 
        end else begin
                // The single clock path
                // The single clock path
                r_idata <= c_mem[i_addr[(CS-1):0]];
 
                // The valid for the single clock path
                // The valid for the single clock path
                //      Only ... we need to wait if we are currently writing
                //      Only ... we need to wait if we are currently writing
                //      to our cache.
                //      to our cache.
                r_svalid<= (!i_op)&&(!cache_miss_inow)&&(w_cachable)
                r_svalid<= (i_pipe_stb)&&(!i_op[0])&&(w_cachable)
                                &&(i_pipe_stb)&&(!c_wr)&&(!wr_cstb);
                                &&(!cache_miss_inow)&&(!c_wr)&&(!wr_cstb);
 
 
                //
                //
                // The two clock in-cache path
                // The two clock in-cache path
                //
                //
                // Some preliminaries that needed to be calculated on the first
                // Some preliminaries that needed to be calculated on the first
                // clock
                // clock
                if (!o_busy)
                if ((!o_pipe_stalled)&&(!r_rd_pending))
 
                        r_addr <= i_addr[(AW+1):2];
 
                if ((!o_pipe_stalled)&&(!r_rd_pending))
                begin
                begin
                        r_iv   <= c_v[i_cline];
                        r_iv   <= c_v[i_cline];
                        r_itag <= c_vtags[i_cline];
                        r_itag <= c_vtags[i_cline];
                        r_addr <= i_addr;
                        r_cachable <= (!i_op[0])&&(w_cachable)&&(i_pipe_stb);
                        r_cachable <= (!i_op)&&(w_cachable)&&(i_pipe_stb);
                        r_rd_pending <= (i_pipe_stb)&&(!i_op[0])&&(w_cachable)
 
                                &&((cache_miss_inow)||(c_wr)||(wr_cstb));
 
                                // &&((!c_wr)||(!wr_cstb));
                end else begin
                end else begin
                        r_iv   <= c_v[r_cline];
                        r_iv   <= c_v[r_cline];
                        r_itag <= c_vtags[r_cline];
                        r_itag <= c_vtags[r_cline];
 
                        r_rd_pending <= (r_rd_pending)
 
                                &&((!cyc)||(!i_wb_err))
 
                                &&((r_itag != r_ctag)||(!r_iv));
                end
                end
                // r_idata still contains the right answer
                r_rd <= (i_pipe_stb)&&(!i_op[0]);
                r_rd <= (i_pipe_stb)&&(!i_op);
 
                r_ddata  <= r_idata;
 
                // r_itag contains the tag we didn't have available to us on the
                // r_itag contains the tag we didn't have available to us on the
                // last clock, r_ctag is a bit select from r_addr containing a
                // last clock, r_ctag is a bit select from r_addr containing a
                // one clock delayed address.
                // one clock delayed address.
                r_dvalid <= (r_itag == r_ctag)&&(r_iv)&&(r_cachable);
                r_dvalid <= (!r_svalid)&&(!r_dvalid)&&(r_itag == r_ctag)&&(r_iv)
                if ((r_itag == r_ctag)&&(r_iv)&&(r_cachable))
                                                &&(r_cachable)&&(r_rd_pending);
 
                if ((r_itag == r_ctag)&&(r_iv)&&(r_cachable)&&(r_rd_pending))
 
                begin
 
                        last_tag_valid <= 1'b1;
                        last_tag <= r_ctag;
                        last_tag <= r_ctag;
 
                end else if ((state == DC_READC)
 
                                &&(last_tag[CS-LS-1:0]==o_wb_addr[CS-1:LS])
 
                                &&((i_wb_ack)||(i_wb_err)))
 
                        last_tag_valid <= 1'b0;
 
 
                // r_cache miss takes a clock cycle.  It is only ever true for
                // r_cache miss takes a clock cycle.  It is only ever true for
                // something that should be cachable, but isn't in the cache.
                // something that should be cachable, but isn't in the cache.
                // A cache miss is only true _if_
                // A cache miss is only true _if_
                // 1. A read was requested
                // 1. A read was requested
Line 212... Line 300...
                                // One clock path -- miss
                                // One clock path -- miss
                                &&(!r_svalid)
                                &&(!r_svalid)
                                // Two clock path -- misses as well
                                // Two clock path -- misses as well
                                &&(r_rd)&&(!r_svalid)
                                &&(r_rd)&&(!r_svalid)
                                &&((r_itag != r_ctag)||(!r_iv));
                                &&((r_itag != r_ctag)||(!r_iv));
 
        end
 
 
                r_rdata <= c_mem[r_addr[(CS-1):0]];
        initial r_sel = 4'hf;
                r_rvalid<= ((i_wb_ack)&&(last_ack));
        always @(posedge i_clk)
 
        if (i_reset)
 
                r_sel <= 4'hf;
 
        else if (!o_pipe_stalled)
 
        begin
 
                casez({i_op[2:1], i_addr[1:0]})
 
                4'b0???: r_sel <= 4'b1111;
 
                4'b100?: r_sel <= 4'b1100;
 
                4'b101?: r_sel <= 4'b0011;
 
                4'b1100: r_sel <= 4'b1000;
 
                4'b1101: r_sel <= 4'b0100;
 
                4'b1110: r_sel <= 4'b0010;
 
                4'b1111: r_sel <= 4'b0001;
 
                endcase
        end
        end
 
 
`define DC_IDLE         2'b00
        assign  o_wb_sel = (state == DC_READC) ? 4'hf : r_sel;
`define DC_WRITE        2'b01
 
`define DC_READS        2'b10
 
`define DC_READC        2'b11
 
        reg     [1:0]    state;
 
 
 
        reg     [(AW-LS-1):0]    wr_wtag, wr_vtag;
        initial o_wb_data = 0;
        reg     [31:0]           wr_data;
        always @(posedge i_clk)
        reg     [(CS-1):0]       wr_addr;
        if (i_reset)
 
                o_wb_data <= 0;
 
        else if ((!o_busy)||((stb)&&(!i_wb_stall)))
 
        begin
 
                casez(i_op[2:1])
 
                2'b0?: o_wb_data <= i_data;
 
                2'b10: o_wb_data <= { (2){i_data[15:0]} };
 
                2'b11: o_wb_data <= { (4){i_data[ 7:0]} };
 
                endcase
 
        end
 
 
 
        generate if (OPT_PIPE)
 
        begin : OPT_PIPE_FIFO
 
                reg     [NAUX+4-2:0]     fifo_data [0:((1<<OPT_FIFO_DEPTH)-1)];
 
 
 
                reg     [DP:0]           wraddr, rdaddr;
 
 
 
                always @(posedge i_clk)
 
                if (i_pipe_stb)
 
                        fifo_data[wraddr[DP-1:0]]
 
                                <= { i_oreg[NAUX-2:0], i_op[2:1], i_addr[1:0] };
 
 
 
                always @(posedge i_clk)
 
                if (i_pipe_stb)
 
                        gie <= i_oreg[NAUX-1];
 
 
 
`ifdef  NO_BKRAM
 
                reg     [NAUX+4-2:0]     r_req_data, r_last_data;
 
                reg                     single_write;
 
 
 
                always @(posedge i_clk)
 
                        r_req_data <= fifo_data[rdaddr[DP-1:0]];
 
 
 
                always @(posedge i_clk)
 
                        single_write <= (rdaddr == wraddr)&&(i_pipe_stb);
 
 
 
                always @(posedge i_clk)
 
                if (i_pipe_stb)
 
                        r_last_data <= { i_oreg[NAUX-2:0],
 
                                                i_op[2:1], i_addr[1:0] };
 
 
 
                always @(*)
 
                begin
 
                        req_data[NAUX+4-1] = gie;
 
                        // if ((r_svalid)||(state == DC_READ))
 
                        if (single_write)
 
                                req_data[NAUX+4-2:0] = r_last_data;
 
                        else
 
                                req_data[NAUX+4-2:0] = r_req_data;
 
                end
 
 
 
                always @(*)
 
                        `ASSERT(req_data == fifo_data[rdaddr[DP-1:0]]);
 
`else
 
                always @(*)
 
                        req_data[NAUX+4-2:0] = fifo_data[rdaddr[DP-1:0]];
 
                always @(*)
 
                        req_data[NAUX+4-1] = gie;
 
`endif
 
 
 
                initial wraddr = 0;
 
                always @(posedge i_clk)
 
                if ((i_reset)||((cyc)&&(i_wb_err)))
 
                        wraddr <= 0;
 
                else if (i_pipe_stb)
 
                        wraddr <= wraddr + 1'b1;
 
 
 
                initial rdaddr = 0;
 
                always @(posedge i_clk)
 
                if ((i_reset)||((cyc)&&(i_wb_err)))
 
                        rdaddr <= 0;
 
                else if ((r_dvalid)||(r_svalid))
 
                        rdaddr <= rdaddr + 1'b1;
 
                else if ((state == DC_WRITE)&&(i_wb_ack))
 
                        rdaddr <= rdaddr + 1'b1;
 
                else if ((state == DC_READS)&&(i_wb_ack))
 
                        rdaddr <= rdaddr + 1'b1;
 
 
 
`ifdef  FORMAL
 
                reg     [AW-1:0] f_fifo_addr [0:((1<<OPT_FIFO_DEPTH)-1)];
 
                reg     [F_LGDEPTH-1:0]  f_last_wraddr;
 
                reg     f_pc_pending;
 
 
 
                always @(*)
 
                begin
 
                        f_fill = 0;
 
                        f_fill[DP:0] = wraddr - rdaddr;
 
                end
 
 
 
                always @(*)
 
                        `ASSERT(f_fill <= { 1'b1, {(DP){1'b0}} });
 
 
 
                always @(*)
 
                if ((r_dvalid)||(r_svalid))
 
                begin
 
                        if (r_svalid)
 
                                `ASSERT(f_fill == 1);
 
                        else if (r_dvalid)
 
                                `ASSERT(f_fill == 1);
 
                        else
 
                                `ASSERT(f_fill == 0);
 
                end else if (r_rd_pending)
 
                        `ASSERT(f_fill == 1);
 
                else
 
                        `ASSERT(f_fill == npending);
 
 
 
 
 
                initial f_pc_pending = 0;
 
                always @(posedge i_clk)
 
                if (i_reset)
 
                        f_pc_pending <= 1'b0;
 
                else if (i_pipe_stb)
 
                        f_pc_pending <= (!i_op[0])&&(i_oreg[3:1] == 3'h7);
 
                else if (f_fill == 0)
 
                        f_pc_pending <= 1'b0;
 
                //else if ((o_valid)&&(o_wreg[3:1] == 3'h7)&&(f_fill == 0))
 
                //      f_pc_pending <= 1'b0;
 
 
 
                always @(posedge i_clk)
 
                if (f_pc_pending)
 
                        `ASSUME(!i_pipe_stb);
 
 
 
                always @(posedge i_clk)
 
                if (state == DC_WRITE)
 
                        `ASSERT(!f_pc_pending);
 
 
 
                always @(*)
 
                begin
 
                        f_last_wraddr = 0;
 
                        f_last_wraddr[DP:0] = wraddr - 1'b1;
 
                end
 
 
 
                always @(posedge i_clk)
 
                if (r_rd_pending)
 
                        `ASSERT(f_pc_pending == (fifo_data[f_last_wraddr][7:5] == 3'h7));
 
 
 
`define INSPECT_FIFO
 
                reg     [((1<<(DP+1))-1):0]      f_valid_fifo_entry;
 
 
 
                genvar  k;
 
                for(k=0; k<(1<<(DP+1)); k=k+1)
 
                begin
 
 
 
                        always @(*)
 
                        begin
 
                        f_valid_fifo_entry[k] = 1'b0;
 
                        /*
 
                        if ((rdaddr[DP] != wraddr[DP])
 
                                        &&(rdaddr[DP-1:0] == wraddr[DP-1:0]))
 
                                f_valid_fifo_entry[k] = 1'b1;
 
                        else */
 
                        if ((rdaddr < wraddr)&&(k < wraddr)
 
                                        &&(k >= rdaddr))
 
                                f_valid_fifo_entry[k] = 1'b1;
 
                        else if ((rdaddr > wraddr)&&(k >= rdaddr))
 
                                f_valid_fifo_entry[k] = 1'b1;
 
                        else if ((rdaddr > wraddr)&&(k <  wraddr))
 
                                f_valid_fifo_entry[k] = 1'b1;
 
                        end
 
 
 
`ifdef  INSPECT_FIFO
 
                        wire    [NAUX+4-2:0]     fifo_data_k;
 
 
 
                        assign  fifo_data_k = fifo_data[k[DP-1:0]];
 
                        always @(*)
 
                        if (f_valid_fifo_entry[k])
 
                        begin
 
                                if (!f_pc_pending)
 
                                        `ASSERT((o_wb_we)||(fifo_data_k[7:5] != 3'h7));
 
                                else if (k != f_last_wraddr)
 
                                        `ASSERT(fifo_data_k[7:5] != 3'h7);
 
                        end
 
`endif // INSPECT_FIFO
 
 
 
                end
 
 
 
`ifndef INSPECT_FIFO
 
                always @(posedge i_clk)
 
                if ((r_rd_pending)&&(rdaddr[DP:0] != f_last_wraddr[DP-1]))
 
                        assume(fifo_data[rdaddr][7:5] != 3'h7);
 
`endif // INSPECT_FIFO
 
 
 
                assign  f_pc = f_pc_pending;
 
 
 
                //
 
                //
 
                //
 
                always @(*)
 
                        f_pending_addr = f_fifo_addr[rdaddr];
 
 
 
                //
 
                //
 
                //
 
                always @(posedge i_clk)
 
                if (i_pipe_stb)
 
                        f_fifo_addr[wraddr[DP-1:0]] <= i_addr[AW+1:2];
 
 
 
                always @(*)
 
                begin
 
                        f_return_address[AW] = (o_wb_cyc_lcl);
 
                        f_return_address[AW-1:0] = f_fifo_addr[rdaddr];
 
                        if (state == DC_READC)
 
                                f_return_address[LS-1:0]
 
                                = (o_wb_addr[LS-1:0] - f_outstanding[LS-1:0]);
 
                end
 
 
 
`define TWIN_WRITE_TEST
 
`ifdef  TWIN_WRITE_TEST
 
                (* anyconst *)  reg     [DP:0]           f_twin_base;
 
                                reg     [DP:0]           f_twin_next;
 
                (* anyconst *)  reg     [AW+NAUX+4-2-1:0]        f_twin_first,
 
                                                        f_twin_second;
 
                // reg  [AW-1:0]        f_fifo_addr [0:((1<<OPT_FIFO_DEPTH)-1)];
 
                // reg  [NAUX+4-2:0]    fifo_data [0:((1<<OPT_FIFO_DEPTH)-1)];
 
 
 
                always @(*)     f_twin_next = f_twin_base+1;
 
 
 
                reg     f_twin_none, f_twin_single, f_twin_double, f_twin_last;
 
                reg     f_twin_valid_one, f_twin_valid_two;
 
                always @(*)
 
                begin
 
                        f_twin_valid_one = ((f_valid_fifo_entry[f_twin_base])
 
                                &&(f_twin_first == { f_fifo_addr[f_twin_base],
 
                                                fifo_data[f_twin_base] }));
 
                        f_twin_valid_two = ((f_valid_fifo_entry[f_twin_next])
 
                                &&(f_twin_second == { f_fifo_addr[f_twin_next],
 
                                                fifo_data[f_twin_next] }));
 
                end
 
 
 
                always @(*)
 
                begin
 
                        f_twin_none   =(!f_twin_valid_one)&&(!f_twin_valid_two);
 
                        f_twin_single =( f_twin_valid_one)&&(!f_twin_valid_two);
 
                        f_twin_double =( f_twin_valid_one)&&( f_twin_valid_two);
 
                        f_twin_last   =(!f_twin_valid_one)&&( f_twin_valid_two);
 
                end
 
 
 
                always @(posedge i_clk)
 
                if ((!f_past_valid)||($past(i_reset))||($past(cyc && i_wb_err)))
 
                        `ASSERT(f_twin_none);
 
                else if ($past(f_twin_none))
 
                        `ASSERT(f_twin_none || f_twin_single || f_twin_last);
 
                else if ($past(f_twin_single))
 
                        `ASSERT(f_twin_none || f_twin_single || f_twin_double || f_twin_last);
 
                else if ($past(f_twin_double))
 
                        `ASSERT(f_twin_double || f_twin_last);
 
                else if ($past(f_twin_last))
 
                        `ASSERT(f_twin_none || f_twin_single || f_twin_last);
 
 
 
`endif // TWIN_WRITE_TEST
 
 
 
                always @(*)
 
                        `ASSERT(req_data == { gie, fifo_data[rdaddr[DP-1:0]] });
 
 
 
                always @(posedge i_clk)
 
                if (r_svalid||r_dvalid || r_rd_pending)
 
                        `ASSERT(f_fill == 1);
 
                else if (f_fill > 0)
 
                        `ASSERT(cyc);
 
 
 
                always @(posedge i_clk)
 
                if (state != 0)
 
                        `ASSERT(f_fill > 0);
 
                else if (!r_svalid && !r_dvalid && !r_rd_pending)
 
                        `ASSERT(f_fill == 0);
 
 
 
`endif // FORMAL
 
 
 
                always @(posedge i_clk)
 
                        o_wreg <= req_data[(NAUX+4-1):4];
 
 
 
                /*
 
                reg     fifo_err;
 
                always @(posedge i_clk)
 
                begin
 
                        fifo_err <= 1'b0;
 
                        if ((!o_busy)&&(rdaddr != wraddr))
 
                                fifo_err <= 1'b1;
 
                        if ((!r_dvalid)&&(!r_svalid)&&(!r_rd_pending))
 
                                fifo_err <= (npending != (wraddr-rdaddr));
 
                end
 
 
 
                always @(*)
 
                o_debug = { i_pipe_stb, state, cyc, stb,        //  5b
 
                                fifo_err, i_oreg[3:0], o_wreg,          // 10b
 
                                rdaddr, wraddr,                 // 10b
 
                                i_wb_ack, i_wb_err, o_pipe_stalled, o_busy,//4b
 
                                r_svalid, r_dvalid, r_rd_pending };
 
                */
 
        end else begin : NO_FIFO
 
 
 
                always @(posedge i_clk)
 
                if (i_pipe_stb)
 
                        req_data <= { i_oreg, i_op[2:1], i_addr[1:0] };
 
 
 
                always @(*)
 
                        o_wreg = req_data[(NAUX+4-1):4];
 
 
 
                always @(*)
 
                        gie = i_oreg[NAUX-1];
 
 
 
`ifdef  FORMAL
 
                assign  f_pc = ((r_rd_pending)||(o_valid))&&(o_wreg[3:1] == 3'h7);
 
 
 
                //
 
                //
 
                //
 
                initial f_pending_addr = 0;
 
                always @(posedge i_clk)
 
                if (i_reset)
 
                        f_pending_addr <= 0;
 
                else if (i_pipe_stb)
 
                begin
 
                        f_pending_addr <= { (OPT_LOCAL_BUS)&&(&i_addr[DW-1:DW-8]),
 
                                                i_addr[(AW+1):2] };
 
                end
 
 
 
                //
 
                //
 
                always @(*)
 
                begin
 
                        f_return_address[AW]      = o_wb_cyc_lcl;
 
                        f_return_address[AW-1:LS] = o_wb_addr[AW-1:LS];
 
                end
 
                always @(*)
 
                if (state == DC_READS)
 
                        f_return_address[LS-1:0] = o_wb_addr[LS-1:0];
 
                else
 
                        f_return_address[LS-1:0]
 
                                = (o_wb_addr[LS-1:0] - f_outstanding[LS-1:0]);
 
 
 
`endif
 
                /*
 
                always @(*)
 
                o_debug = { i_pipe_stb, state, cyc, stb,        //  5b
 
                                i_oreg, o_wreg,                 // 10b
 
                                10'hb,                          // 10b
 
                                i_wb_ack, i_wb_err, o_pipe_stalled, o_busy,//4b
 
                                r_svalid, r_dvalid, r_rd_pending };
 
                */
 
 
 
                // verilator lint_off UNUSED
 
                wire    unused_no_fifo;
 
                assign  unused_no_fifo = gie;
 
                // verilator lint_on  UNUSED
 
        end endgenerate
 
 
 
 
 
        initial r_wb_cyc_gbl = 0;
 
        initial r_wb_cyc_lcl = 0;
 
        initial o_wb_stb_gbl = 0;
 
        initial o_wb_stb_lcl = 0;
 
        initial c_v = 0;
 
        initial cyc = 0;
 
        initial stb = 0;
 
        initial c_wr = 0;
 
        initial wr_cstb = 0;
 
        initial state = DC_IDLE;
 
        initial set_vflag = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
        begin
        begin
 
                c_v <= 0;
 
                c_wr   <= 1'b0;
 
                c_wsel <= 4'hf;
 
                r_wb_cyc_gbl <= 1'b0;
 
                r_wb_cyc_lcl <= 1'b0;
 
                o_wb_stb_gbl <= 0;
 
                o_wb_stb_lcl <= 0;
 
                wr_cstb <= 1'b0;
 
                last_line_stb <= 1'b0;
 
                end_of_line <= 1'b0;
 
                state <= DC_IDLE;
 
                cyc <= 1'b0;
 
                stb <= 1'b0;
 
                state <= DC_IDLE;
 
                set_vflag <= 1'b0;
 
        end else begin
                // By default, update the cache from the write 1-clock ago
                // By default, update the cache from the write 1-clock ago
                c_wr <= (wr_cstb)&&(wr_wtag == wr_vtag);
                // c_wr <= (wr_cstb)&&(wr_wtag == wr_vtag);
                c_wdata <= wr_data;
                // c_waddr <= wr_addr[(CS-1):0];
                c_waddr <= wr_addr[(CS-1):0];
                c_wr <= 0;
 
 
 
                set_vflag <= 1'b0;
 
                if ((!cyc)&&(set_vflag))
 
                        c_v[c_waddr[(CS-1):LS]] <= 1'b1;
 
 
                wr_cstb <= 1'b0;
                wr_cstb <= 1'b0;
                wr_vtag <= c_vtags[o_wb_addr[(CS-LS-1):0]];
 
                wr_wtag <= o_wb_addr[(AW-LS-1):0];
 
                wr_data <= o_wb_data;
 
                wr_addr <= o_wb_addr[(CS-1):0];
 
 
 
 
                if (!cyc)
 
                        wr_addr <= r_addr[(CS-1):0];
 
                else if (i_wb_ack)
 
                        wr_addr <= wr_addr + 1'b1;
 
                else
 
                        wr_addr <= wr_addr;
 
 
                if (LS <= 1)
                if (LS <= 0)
                        end_of_line <= 1'b1;
                        end_of_line <= 1'b1;
 
                else if (!cyc)
 
                        end_of_line <= 1'b0;
 
                else if (!end_of_line)
 
                begin
 
                        if (i_wb_ack)
 
                                end_of_line
 
                                <= (c_waddr[(LS-1):0] == {{(LS-2){1'b1}},2'b01});
                else
                else
                        end_of_line<=(cyc)&&((c_waddr[(LS-1):1]=={(LS-1){1'b1}})
                                end_of_line
                                ||((i_wb_ack)
                                <= (c_waddr[(LS-1):0]=={{(LS-1){1'b1}}, 1'b0});
                                &&(c_waddr[(LS-1):0]=={{(LS-2){1'b1}},2'b01})));
                end
 
 
                if (LS <= 1)
                if (!cyc)
 
                        last_line_stb <= (LS <= 0);
 
                else if ((stb)&&(!i_wb_stall)&&(LS <= 1))
                        last_line_stb <= 1'b1;
                        last_line_stb <= 1'b1;
                else
                else if ((stb)&&(!i_wb_stall))
                        last_line_stb <= (stb)&&
                        last_line_stb <= (o_wb_addr[(LS-1):1]=={(LS-1){1'b1}});
                                ((o_wb_addr[(LS-1):1]=={(LS-1){1'b1}})
                else if (stb)
                                ||((!i_wb_stall)
                        last_line_stb <= (o_wb_addr[(LS-1):0]=={(LS){1'b1}});
                                        &&(o_wb_addr[(LS-1):0]
 
                                                =={{(LS-2){1'b1}},2'b01})));
 
 
 
                //
                //
                if (state == `DC_IDLE)
                //
                        pipeable_op <= 1'b0;
                if (state == DC_IDLE)
                if (state == `DC_IDLE)
 
                        non_pipeable_op <= 1'b0;
 
 
 
 
 
                if (state == `DC_IDLE)
 
                begin
                begin
                        o_wb_we <= 1'b0;
                        o_wb_we <= 1'b0;
                        o_wb_data <= i_data;
 
                        pipeable_op <= 1'b0;
 
                        non_pipeable_op <= 1'b1;
 
 
 
                        cyc <= 1'b0;
                        cyc <= 1'b0;
                        stb <= 1'b0;
                        stb <= 1'b0;
 
 
                        r_wb_cyc_gbl <= 1'b0;
                        r_wb_cyc_gbl <= 1'b0;
                        r_wb_cyc_lcl <= 1'b0;
                        r_wb_cyc_lcl <= 1'b0;
                        o_wb_stb_gbl <= 1'b0;
                        o_wb_stb_gbl <= 1'b0;
                        o_wb_stb_lcl <= 1'b0;
                        o_wb_stb_lcl <= 1'b0;
 
 
                        in_cache <= (i_op)&&(w_cachable);
                        in_cache <= (i_op[0])&&(w_cachable);
                        if ((i_pipe_stb)&&(i_op))
                        if ((i_pipe_stb)&&(i_op[0]))
                        begin // Write  operation
                        begin // Write  operation
                                state <= `DC_WRITE;
                                state <= DC_WRITE;
                                o_wb_addr <= i_addr;
                                o_wb_addr <= i_addr[(AW+1):2];
                                o_wb_we <= 1'b1;
                                o_wb_we <= 1'b1;
                                pipeable_op <= 1'b1;
 
 
 
                                cyc <= 1'b1;
                                cyc <= 1'b1;
                                stb <= 1'b1;
                                stb <= 1'b1;
 
 
                                r_wb_cyc_gbl <= (i_addr[31:30]!=2'b11);
                                if (OPT_LOCAL_BUS)
                                r_wb_cyc_lcl <= (i_addr[31:30]==2'b11);
                                begin
                                o_wb_stb_gbl <= (i_addr[31:30]!=2'b11);
                                r_wb_cyc_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
                                o_wb_stb_lcl <= (i_addr[31:30]==2'b11);
                                r_wb_cyc_lcl <= (i_addr[DW-1:DW-8]==8'hff);
 
                                o_wb_stb_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
 
                                o_wb_stb_lcl <= (i_addr[DW-1:DW-8]==8'hff);
 
                                end else begin
 
                                        r_wb_cyc_gbl <= 1'b1;
 
                                        o_wb_stb_gbl <= 1'b1;
 
                                end
 
 
                        end else if (r_cache_miss)
                        end else if (r_cache_miss)
                        begin
                        begin
                                state <= `DC_READC;
                                state <= DC_READC;
                                o_wb_addr <= { i_ctag, {(LS){1'b0}} };
                                o_wb_addr <= { r_ctag, {(LS){1'b0}} };
                                non_pipeable_op <= 1'b1;
 
 
 
 
                                c_waddr <= { r_ctag[CS-LS-1:0], {(LS){1'b0}} }-1'b1;
                                cyc <= 1'b1;
                                cyc <= 1'b1;
                                stb <= 1'b1;
                                stb <= 1'b1;
                                r_wb_cyc_gbl <= 1'b1;
                                r_wb_cyc_gbl <= 1'b1;
                                o_wb_stb_gbl <= 1'b1;
                                o_wb_stb_gbl <= 1'b1;
 
                                wr_addr[LS-1:0] <= 0;
                        end else if ((i_pipe_stb)&&(!w_cachable))
                        end else if ((i_pipe_stb)&&(!w_cachable))
                        begin // Read non-cachable memory area
                        begin // Read non-cachable memory area
                                state <= `DC_READS;
                                state <= DC_READS;
                                o_wb_addr <= i_addr;
                                o_wb_addr <= i_addr[(AW+1):2];
                                pipeable_op <= 1'b1;
 
 
 
                                cyc <= 1'b1;
                                cyc <= 1'b1;
                                stb <= 1'b1;
                                stb <= 1'b1;
                                r_wb_cyc_gbl <= (i_addr[31:30]!=2'b11);
                                if (OPT_LOCAL_BUS)
                                r_wb_cyc_lcl <= (i_addr[31:30]==2'b11);
                                begin
                                o_wb_stb_gbl <= (i_addr[31:30]!=2'b11);
                                r_wb_cyc_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
                                o_wb_stb_lcl <= (i_addr[31:30]==2'b11);
                                r_wb_cyc_lcl <= (i_addr[DW-1:DW-8]==8'hff);
 
                                o_wb_stb_gbl <= (i_addr[DW-1:DW-8]!=8'hff);
 
                                o_wb_stb_lcl <= (i_addr[DW-1:DW-8]==8'hff);
 
                                end else begin
 
                                r_wb_cyc_gbl <= 1'b1;
 
                                o_wb_stb_gbl <= 1'b1;
 
                                end
                        end // else we stay idle
                        end // else we stay idle
 
 
                end else if (state == `DC_READC)
                end else if (state == DC_READC)
                begin
                begin
                        // We enter here once we have committed to reading
                        // We enter here once we have committed to reading
                        // data into a cache line.
                        // data into a cache line.
                        if ((stb)&&(!i_wb_stall))
                        if ((stb)&&(!i_wb_stall))
                        begin
                        begin
                                stb <= (!last_line_stb);
                                stb <= (!last_line_stb);
                                o_wb_stb_gbl <= (!last_line_stb);
                                o_wb_stb_gbl <= (!last_line_stb);
                                o_wb_addr[(LS-1):0] <= o_wb_addr[(LS-1):0]+1'b1;
                                o_wb_addr[(LS-1):0] <= o_wb_addr[(LS-1):0]+1'b1;
                        end
                        end
 
 
                        if(stb)
                        if ((i_wb_ack)&&(!end_of_line))
                                c_v[o_wb_addr[(CS-LS-1):0]] <= 1'b0;
                                c_v[o_wb_addr[(CS-1):LS]] <= 1'b0;
 
 
                        c_wr <= (i_wb_ack);
                        c_wr <= (i_wb_ack);
                        c_wdata <= o_wb_data;
                        c_wdata <= i_wb_data;
                        c_waddr <= ((c_wr)?(c_waddr+1'b1):c_waddr);
                        c_waddr <= ((i_wb_ack)?(c_waddr+1'b1):c_waddr);
 
                        c_wsel  <= 4'hf;
                        c_vtags[o_wb_addr[(CS-LS-1):0]]<= o_wb_addr[(AW-LS-1):0];
 
 
                        set_vflag <= !i_wb_err;
 
                        if (i_wb_ack)
 
                                c_vtags[r_addr[(CS-1):LS]]
 
                                                <= r_addr[(AW-1):LS];
 
 
                        if (((i_wb_ack)&&(end_of_line))||(i_wb_err))
                        if (((i_wb_ack)&&(end_of_line))||(i_wb_err))
                        begin
                        begin
                                state           <= `DC_IDLE;
                                state          <= DC_IDLE;
                                non_pipeable_op <= 1'b0;
 
                                cyc <= 1'b0;
                                cyc <= 1'b0;
 
                                stb <= 1'b0;
                                r_wb_cyc_gbl <= 1'b0;
                                r_wb_cyc_gbl <= 1'b0;
                                r_wb_cyc_lcl <= 1'b0;
                                r_wb_cyc_lcl <= 1'b0;
 
                                o_wb_stb_gbl <= 1'b0;
 
                                o_wb_stb_lcl <= 1'b0;
                                //
                                //
                                c_v[o_wb_addr[(CS-LS-1):0]] <= i_wb_ack;
 
                        end
                        end
                end else if (state == `DC_READS)
                end else if (state == DC_READS)
                begin
                begin
                        // We enter here once we have committed to reading
                        // We enter here once we have committed to reading
                        // data that cannot go into a cache line
                        // data that cannot go into a cache line
                        if ((!i_wb_stall)&&(!i_pipe_stb))
                        if ((!i_wb_stall)&&(!i_pipe_stb))
                        begin
                        begin
                                stb <= 1'b0;
                                stb <= 1'b0;
                                o_wb_stb_gbl <= 1'b0;
                                o_wb_stb_gbl <= 1'b0;
                                o_wb_stb_lcl <= 1'b0;
                                o_wb_stb_lcl <= 1'b0;
                                pipeable_op <= 1'b0;
 
                        end
                        end
 
 
                        if ((!i_wb_stall)&&(i_pipe_stb))
                        if ((!i_wb_stall)&&(i_pipe_stb))
                                o_wb_addr <= i_data;
                                o_wb_addr <= i_addr[(AW+1):2];
 
 
                        c_wr <= 1'b0;
                        c_wr <= 1'b0;
 
 
                        if (((i_wb_ack)&&(last_ack))||(i_wb_err))
                        if (((i_wb_ack)&&(last_ack))||(i_wb_err))
                        begin
                        begin
                                state        <= `DC_IDLE;
                                state        <= DC_IDLE;
                                cyc          <= 1'b0;
                                cyc          <= 1'b0;
 
                                stb          <= 1'b0;
                                r_wb_cyc_gbl <= 1'b0;
                                r_wb_cyc_gbl <= 1'b0;
                                r_wb_cyc_lcl <= 1'b0;
                                r_wb_cyc_lcl <= 1'b0;
 
                                o_wb_stb_gbl <= 1'b0;
 
                                o_wb_stb_lcl <= 1'b0;
                        end
                        end
                end else if (state == `DC_WRITE)
                end else if (state == DC_WRITE)
                begin
                begin
                        // c_wr    <= (c_v[])&&(c_tag[])&&(in_cache)&&(stb);
                        c_wr    <= (stb)&&(c_v[o_wb_addr[CS-1:LS]])
 
                                &&(c_vtags[o_wb_addr[CS-1:LS]]==o_wb_addr[AW-1:LS])
 
                                &&(stb);
                        c_wdata <= o_wb_data;
                        c_wdata <= o_wb_data;
                        c_waddr <= (state == `DC_IDLE)?i_caddr
                        c_waddr <= r_addr[CS-1:0];
                                : ((c_wr)?(c_waddr+1'b1):c_waddr);
                        c_wsel  <= o_wb_sel;
 
 
                        if ((!i_wb_stall)&&(!i_pipe_stb))
                        if ((!i_wb_stall)&&(!i_pipe_stb))
                        begin
                        begin
                                stb          <= 1'b0;
                                stb          <= 1'b0;
                                o_wb_stb_gbl <= 1'b0;
                                o_wb_stb_gbl <= 1'b0;
                                o_wb_stb_lcl <= 1'b0;
                                o_wb_stb_lcl <= 1'b0;
                                pipeable_op  <= 1'b0;
 
                        end
                        end
 
 
                        wr_cstb  <= (stb)&&(!i_wb_stall)&&(in_cache);
                        wr_cstb  <= (stb)&&(!i_wb_stall)&&(in_cache);
 
 
                        if ((stb)&&(!i_wb_stall)&&(i_pipe_stb))
                        if ((stb)&&(!i_wb_stall))
                                o_wb_addr <= i_addr;
                                o_wb_addr <= i_addr[(AW+1):2];
                        if ((stb)&&(!i_wb_stall)&&(i_pipe_stb))
 
                                o_wb_data <= i_data;
 
 
 
                        if (((i_wb_ack)&&(last_ack))||(i_wb_err))
                        if (((i_wb_ack)&&(last_ack)
 
                                                &&((!OPT_PIPE)||(!i_pipe_stb)))
 
                                ||(i_wb_err))
                        begin
                        begin
                                state        <= `DC_IDLE;
                                state        <= DC_IDLE;
                                cyc          <= 1'b0;
                                cyc          <= 1'b0;
 
                                stb          <= 1'b0;
                                r_wb_cyc_gbl <= 1'b0;
                                r_wb_cyc_gbl <= 1'b0;
                                r_wb_cyc_lcl <= 1'b0;
                                r_wb_cyc_lcl <= 1'b0;
 
                                o_wb_stb_gbl <= 1'b0;
 
                                o_wb_stb_lcl <= 1'b0;
                        end
                        end
                end
                end
        end
        end
 
 
        //
        //
 
        // npending is the number of outstanding (non-cached) read or write
 
        // requests
 
        initial npending = 0;
 
        always @(posedge i_clk)
 
        if ((i_reset)||(!OPT_PIPE)
 
                        ||((cyc)&&(i_wb_err))
 
                        ||((!cyc)&&(!i_pipe_stb))
 
                        ||(state == DC_READC))
 
                npending <= 0;
 
        else if (r_svalid)
 
                npending <= (i_pipe_stb) ? 1:0;
 
        else case({ (i_pipe_stb), (cyc)&&(i_wb_ack) })
 
        2'b01: npending <= npending - 1'b1;
 
        2'b10: npending <= npending + 1'b1;
 
        default: begin end
 
        endcase
 
 
 
        initial last_ack = 1'b0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                last_ack <= 1'b0;
 
        else if (state == DC_IDLE)
 
        begin
 
                last_ack <= 1'b0;
 
                if ((i_pipe_stb)&&(i_op[0]))
 
                        last_ack <= 1'b1;
 
                else if (r_cache_miss)
 
                        last_ack <= (LS == 0);
 
                else if ((i_pipe_stb)&&(!w_cachable))
 
                        last_ack <= 1'b1;
 
        end else if (state == DC_READC)
 
        begin
 
                if (i_wb_ack)
 
                        last_ack <= last_ack || (&wr_addr[LS-1:1]);
 
                else
 
                        last_ack <= last_ack || (&wr_addr[LS-1:0]);
 
        end else case({ (i_pipe_stb), (i_wb_ack) })
 
        2'b01: last_ack <= (npending <= 2);
 
        2'b10: last_ack <= (!cyc)||(npending == 0);
 
        default: begin end
 
        endcase
 
 
 
`ifdef  FORMAL
 
always @(*)
 
`ASSERT(npending <= { 1'b1, {(DP){1'b0}} });
 
 
 
`endif
 
 
 
 
 
        //
        // Writes to the cache
        // Writes to the cache
        //
        //
        // These have been made as simple as possible.  Note that the c_wr
        // These have been made as simple as possible.  Note that the c_wr
        // line has already been determined, as have the write value and address
        // line has already been determined, as have the write value and address
        // on the last clock.  Further, this structure is defined to match the
        // on the last clock.  Further, this structure is defined to match the
        // block RAM design of as many architectures as possible.
        // block RAM design of as many architectures as possible.
        // 
        // 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (c_wr)
                if (c_wr)
                        c_mem[c_waddr] <= c_wdata;
        begin
 
                if (c_wsel[0])
 
                        c_mem[c_waddr][7:0] <= c_wdata[7:0];
 
                if (c_wsel[1])
 
                        c_mem[c_waddr][15:8] <= c_wdata[15:8];
 
                if (c_wsel[2])
 
                        c_mem[c_waddr][23:16] <= c_wdata[23:16];
 
                if (c_wsel[3])
 
                        c_mem[c_waddr][31:24] <= c_wdata[31:24];
 
        end
 
 
        //
        //
        // Reads from the cache
        // Reads from the cache
        //
        //
        // Some architectures require that all reads be registered.  We
        // Some architectures require that all reads be registered.  We
        // accomplish that here.  Whether or not the result of this read is
        // accomplish that here.  Whether or not the result of this read is
        // going to be our output will need to be determined with combinatorial
        // going to be our output will need to be determined with combinatorial
        // logic on the output.
        // logic on the output.
        //
        //
        reg     [31:0]   cached_idata, cached_rdata;
        generate if (OPT_DUAL_READ_PORT)
 
        begin
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                cached_idata <= c_mem[i_caddr];
                cached_idata <= c_mem[i_caddr];
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                cached_rdata <= c_mem[r_caddr];
                cached_rdata <= c_mem[r_caddr];
 
 
 
        end else begin
 
 
 
                always @(posedge i_clk)
 
                        cached_rdata <= c_mem[(o_busy) ? r_caddr : i_caddr];
 
 
 
                always @(*)
 
                        cached_idata = cached_rdata;
 
 
 
        end endgenerate
 
 
// o_data can come from one of three places:
// o_data can come from one of three places:
// 1. The cache, assuming the data was in the last cache line
// 1. The cache, assuming the data was in the last cache line
// 2. The cache, second clock, assuming the data was in the cache at all
// 2. The cache, second clock, assuming the data was in the cache at all
// 3. The cache, after filling the cache
// 3. The cache, after filling the cache
// 4. The wishbone state machine, upon reading the value desired.
// 4. The wishbone state machine, upon reading the value desired.
        always @(posedge i_clk)
        always @(*)
                if (r_svalid)
                if (r_svalid)
                        o_data <= cached_idata;
                        pre_data = cached_idata;
                else if ((i_wb_ack)&&(pipeable_op))
                else if (state == DC_READS)
                        o_data <= i_wb_data;
                        pre_data = i_wb_data;
                else
                else
                        o_data <= cached_rdata;
                        pre_data = cached_rdata;
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                o_valid <= (r_svalid)||((i_wb_ack)&&(pipeable_op))
        casez(req_data[3:0])
                                ||(r_dvalid)||(r_rvalid);
        4'b100?: o_data <= { 16'h0, pre_data[31:16] };
 
        4'b101?: o_data <= { 16'h0, pre_data[15: 0] };
 
        4'b1100: o_data <= { 24'h0, pre_data[31:24] };
 
        4'b1101: o_data <= { 24'h0, pre_data[23:16] };
 
        4'b1110: o_data <= { 24'h0, pre_data[15: 8] };
 
        4'b1111: o_data <= { 24'h0, pre_data[ 7: 0] };
 
        default o_data <= pre_data;
 
        endcase
 
 
 
        initial o_valid = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                o_err <= (cyc)&&(i_wb_err);
        if (i_reset)
 
                o_valid <= 1'b0;
 
        else if (state == DC_READS)
 
                o_valid <= i_wb_ack;
 
        else
 
                o_valid <= (r_svalid)||(r_dvalid);
 
 
        assign  o_busy = (state != `DC_IDLE);
        initial o_err = 1'b0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                o_err <= 1'b0;
 
        else
 
                o_err <= (cyc)&&(i_wb_err);
 
 
 
        initial o_busy = 0;
 
        always @(posedge i_clk)
 
        if ((i_reset)||((cyc)&&(i_wb_err)))
 
                o_busy <= 1'b0;
 
        else if (i_pipe_stb)
 
                o_busy <= 1'b1;
 
        else if ((state == DC_READS)&&(i_wb_ack))
 
                o_busy <= 1'b0;
 
        else if ((r_rd_pending)&&(!r_dvalid))
 
                o_busy <= 1'b1;
 
        else if ((state == DC_WRITE)
 
                        &&(i_wb_ack)&&(last_ack)&&(!i_pipe_stb))
 
                o_busy <= 1'b0;
 
        else if (cyc)
 
                o_busy <= 1'b1;
 
        else // if ((r_dvalid)||(r_svalid))
 
                o_busy <= 1'b0;
 
 
        //
        //
        // Handle our auxilliary data lines.
        // We can use our FIFO addresses to pre-calculate when an ACK is going
 
        // to be the last_noncachable_ack.
 
 
 
 
 
        always @(*)
 
        if (OPT_PIPE)
 
                o_pipe_stalled = (cyc)&&((!o_wb_we)||(i_wb_stall)||(!stb))
 
                                ||(r_rd_pending)||(npending[DP]);
 
        else
 
                o_pipe_stalled = o_busy;
 
 
 
        initial lock_gbl = 0;
 
        initial lock_lcl = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
        begin
 
                lock_gbl <= 1'b0;
 
                lock_lcl<= 1'b0;
 
        end else begin
 
                lock_gbl <= (OPT_LOCK)&&(i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
 
                lock_lcl <= (OPT_LOCK)&&(i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
 
        end
 
 
 
        assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
 
        assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
 
 
 
        generate if (AW+2 < DW)
 
        begin : UNUSED_BITS
 
 
 
                // Verilator lint_off UNUSED
 
                wire    [DW-AW-2:0]      unused;
 
                assign  unused = i_addr[DW-1:AW+1];
 
                // Verilator lint_on  UNUSED
 
        end endgenerate
 
 
 
`ifdef  FORMAL
 
 
 
        initial f_past_valid = 1'b0;
 
        always @(posedge i_clk)
 
                f_past_valid <= 1'b1;
 
 
 
        ////////////////////////////////////////////////
        //
        //
        // These just go into a FIFO upon request, and then get fed back out
        // Reset properties
        // upon completion of an OP.
 
        //
        //
        // These are currently designed for handling bursts of writes or
        ////////////////////////////////////////////////
        // non-cachable  reads.
 
        //
        //
        // A very similar structure will be used once we switch to using an
 
        // MMU, in order to make certain memory operations are synchronous
 
        // enough to deal with bus errors.
 
        //
        //
        reg     [(LGAUX-1):0]    aux_head, aux_tail;
        always @(*)
        reg     [(NAUX-1):0]     aux_fifo [0:((1<<LGAUX)-1)];
        if(!f_past_valid)
        initial aux_head = 0;
                `ASSUME(i_reset);
        initial aux_tail = 0;
 
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if ((!f_past_valid)||($past(i_reset)))
        begin
        begin
                if ((i_rst)||(i_wb_err))
                // Insist on initial statements matching reset values
                        aux_head <= 0;
                `ASSERT(r_rd == 1'b0);
                else if ((i_pipe_stb)&&(!o_busy))
                `ASSERT(r_cachable == 1'b0);
                        aux_head <= aux_head + 1'b1;
                `ASSERT(r_svalid == 1'b0);
                aux_fifo[aux_head] <= i_oreg;
                `ASSERT(r_dvalid == 1'b0);
 
                `ASSERT(r_cache_miss == 1'b0);
 
                `ASSERT(r_addr == 0);
 
                //
 
                `ASSERT(c_wr == 0);
 
                `ASSERT(c_v  == 0);
 
                //
 
                // assert(aux_head == 0);
 
                // assert(aux_tail == 0);
 
                //
 
                `ASSERT(lock_gbl == 0);
 
                `ASSERT(lock_lcl == 0);
        end
        end
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        // Assumptions about our inputs
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        always @(*)
 
        if (o_pipe_stalled)
 
                `ASSUME(!i_pipe_stb);
 
 
 
        always @(*)
 
        if (!f_past_valid)
 
                `ASSUME(!i_pipe_stb);
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                &&($past(i_pipe_stb))&&($past(o_pipe_stalled)))
        begin
        begin
                if ((i_rst)||(i_wb_err))
                `ASSUME($stable(i_pipe_stb));
                        aux_tail <= 0;
                `ASSUME($stable(i_op[0]));
                else if (o_valid) // ||(aux_tail[WBIT])&&(no-mmu-error)
                `ASSUME($stable(i_addr));
                        aux_tail <= aux_tail + 1'b1;
                if (i_op[0])
                o_wreg <= aux_fifo[aux_tail];
                        `ASSUME($stable(i_data));
        end
        end
 
 
 
        always @(posedge i_clk)
 
        if (o_err)
 
                `ASSUME(!i_pipe_stb);
 
 
 
        ////////////////////////////////////////////////
        //
        //
        // We can use our FIFO addresses to pre-calculate when an ACK is going
        // Wishbone properties
        // to be the last_noncachable_ack.
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        wire    f_cyc, f_stb;
 
 
 
        assign  f_cyc = (o_wb_cyc_gbl)|(o_wb_cyc_lcl);
 
        assign  f_stb = (o_wb_stb_gbl)|(o_wb_stb_lcl);
 
 
 
        always @(*)
 
        begin
 
                // Only one interface can be active at once
 
                `ASSERT((!o_wb_cyc_gbl)||(!o_wb_cyc_lcl));
 
                // Strobe may only be active on the active interface
 
                `ASSERT((r_wb_cyc_gbl)||(!o_wb_stb_gbl));
 
                `ASSERT((r_wb_cyc_lcl)||(!o_wb_stb_lcl));
 
                if (o_wb_stb_lcl)
 
                begin
 
                        if (o_wb_we)
 
                                assert(state == DC_WRITE);
 
                        else
 
                                assert(state == DC_READS);
 
                end
 
 
 
                if (cyc)
 
                        assert(o_wb_we == (state == DC_WRITE));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(cyc)&&($past(cyc)))
 
        begin
 
                `ASSERT($stable(r_wb_cyc_gbl));
 
                `ASSERT($stable(r_wb_cyc_lcl));
 
        end
 
 
 
 
        assign o_pipe_stalled=((pipeable_op)&&(i_wb_stall))||(non_pipeable_op);
`ifdef  DCACHE
        // pipeable_op must become zero when stb goes low
`define FWB_MASTER      fwb_master
 
`else
 
`define FWB_MASTER      fwb_counter
 
`endif
 
 
 
        `FWB_MASTER #(
 
                .AW(AW), .DW(DW),
 
                        .F_MAX_STALL(2),
 
                        .F_MAX_ACK_DELAY(3),
 
                        // If you need the proof to run faster, use these
 
                        // lines instead of the two that follow
 
                        // .F_MAX_STALL(1),
 
                        // .F_MAX_ACK_DELAY(1),
 
                        .F_LGDEPTH(F_LGDEPTH),
 
                        .F_MAX_REQUESTS((OPT_PIPE) ? 0 : (1<<LS)),
 
`ifdef  DCACHE
 
                        .F_OPT_SOURCE(1'b1),
 
`endif
 
                        .F_OPT_DISCONTINUOUS(0)
 
                ) fwb(i_clk, i_reset,
 
                        cyc, f_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
 
                                i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
 
                f_nreqs, f_nacks, f_outstanding);
 
 
 
`ifdef  DCACHE  // Arbitrary access is specific to local dcache implementation
 
        ////////////////////////////////////////////////
 
        //
 
        // Arbitrary address properties
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        (* anyconst *)  reg     [AW:0]           f_const_addr;
 
        (* anyconst *)  reg                     f_const_buserr;
 
        wire    [AW-LS-1:0]      f_const_tag, f_ctag_here, f_wb_tag;
 
        wire    [CS-LS-1:0]      f_const_tag_addr;
 
        reg     [DW-1:0] f_const_data;
 
        wire    [DW-1:0] f_cmem_here;
 
        reg                     f_pending_rd;
 
        wire                    f_cval_in_cache;
 
 
 
        assign  f_const_tag    = f_const_addr[AW-1:LS];
 
        assign  f_const_tag_addr = f_const_addr[CS-1:LS];
 
        assign  f_cmem_here    = c_mem[f_const_addr[CS-1:0]];
 
        assign  f_ctag_here    = c_vtags[f_const_addr[CS-1:LS]];
 
        assign  f_wb_tag       = o_wb_addr[AW-1:LS];
 
 
 
        assign  f_cval_in_cache= (c_v[f_const_addr[CS-1:LS]])
 
                                        &&(f_ctag_here == f_const_tag);
 
 
 
        generate if ((AW > DW - 8)&&(OPT_LOCAL_BUS))
 
        begin : UPPER_CONST_ADDR_BITS
 
 
 
                always @(*)
 
                if (f_const_addr[AW])
 
                        assume(&f_const_addr[(AW-1):(DW-8)]);
 
                else
 
                        assume(!(&f_const_addr[(AW-1):(DW-8)]));
 
        end endgenerate
 
 
 
        wire    [AW-1:0] wb_start;
 
        assign  wb_start = (f_stb) ? (o_wb_addr - f_nreqs) : o_wb_addr;
 
 
 
        // Data changes upon request
        always @(posedge i_clk)
        always @(posedge i_clk)
        begin
        begin
                lock_gbl <= (i_lock)&&((r_wb_cyc_gbl)||(lock_gbl));
                if ((i_pipe_stb)&&(i_addr[(AW+1):2] == f_const_addr[AW-1:0])
                lock_lcl <= (i_lock)&&((r_wb_cyc_lcl)||(lock_lcl));
                        &&(f_const_addr[AW] == ((OPT_LOCAL_BUS)
 
                                                &&(&i_addr[(DW-1):(DW-8)])))
 
                        &&(i_op[0]))
 
                begin
 
                        casez({ i_op[2:1], i_addr[1:0] })
 
                        4'b0???: f_const_data <= i_data;
 
                        4'b100?: f_const_data[31:16] <= i_data[15:0];
 
                        4'b101?: f_const_data[15: 0] <= i_data[15:0];
 
                        4'b1100: f_const_data[31:24] <= i_data[ 7:0];
 
                        4'b1101: f_const_data[23:16] <= i_data[ 7:0];
 
                        4'b1110: f_const_data[15: 8] <= i_data[ 7:0];
 
                        4'b1111: f_const_data[ 7: 0] <= i_data[ 7:0];
 
                        endcase
        end
        end
 
 
        assign  o_wb_cyc_gbl = (r_wb_cyc_gbl)||(lock_gbl);
                if (f_cval_in_cache)
        assign  o_wb_cyc_lcl = (r_wb_cyc_lcl)||(lock_lcl);
                        assume((!i_wb_err)
 
                                ||(!i_pipe_stb)
 
                                ||(f_const_addr[AW-1:0] != i_addr[AW+1:2]));
 
        end
 
 
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!i_reset)&&(!f_const_buserr))
 
        begin
 
                if ((cyc)&&(o_wb_we)&&(f_stb)
 
                                &&(o_wb_addr[AW-1:0] == f_const_addr[AW-1:0])
 
                                &&( o_wb_stb_lcl == f_const_addr[AW]))
 
                begin
 
 
 
                        //
 
                        // Changing our data
 
                        //
 
                        if (o_wb_sel[0])
 
                                `ASSERT(o_wb_data[ 7: 0]==f_const_data[ 7: 0]);
 
                        if (o_wb_sel[1])
 
                                `ASSERT(o_wb_data[15: 8]==f_const_data[15: 8]);
 
                        if (o_wb_sel[2])
 
                                `ASSERT(o_wb_data[23:16]==f_const_data[23:16]);
 
                        if (o_wb_sel[3])
 
                                `ASSERT(o_wb_data[31:24]==f_const_data[31:24]);
 
 
 
                        // Check the data in the cache
 
                        if ((!f_const_addr[AW])&&(c_v[f_const_tag_addr])
 
                                &&(f_ctag_here == o_wb_addr[AW-1:LS]))
 
                        begin
 
                        if ((!c_wsel[0])&&(!o_wb_sel[0]))
 
                                `ASSERT(f_cmem_here[ 7: 0]==f_const_data[ 7: 0]);
 
                        if ((!c_wsel[1])&&(!o_wb_sel[1]))
 
                                `ASSERT(f_cmem_here[15: 8]==f_const_data[15: 8]);
 
                        if ((!c_wsel[2])&&(!o_wb_sel[2]))
 
                                `ASSERT(f_cmem_here[23:16]==f_const_data[23:16]);
 
                        if ((!c_wsel[3])&&(!o_wb_sel[3]))
 
                                `ASSERT(f_cmem_here[31:24]==f_const_data[31:24]);
 
 
 
                        end
 
                end else if ((!f_const_addr[AW])&&(c_v[f_const_tag_addr])
 
                        &&(f_ctag_here ==f_const_addr[AW-1:LS]))
 
                begin
 
                        // If ...
 
                        //   1. Our magic address is cachable
 
                        //   2. Our magic address is associated with a valid
 
                        //              cache line
 
                        //   3. The cache tag matches our magic address
 
 
 
 
 
                        // if ($past(cyc && i_wb_err))
 
                        // begin
 
                                // Ignore what happens on an error, the result
 
                                // becomes undefined anyway
 
                        // end else
 
                        if ((c_wr)
 
                                &&(c_waddr[CS-1:0] == f_const_addr[CS-1:0]))
 
                        begin
 
                                //
 
                                // If we are writing to this valid cache line
 
                                //
 
                                if (c_wsel[3])
 
                                        `ASSERT(c_wdata[31:24]
 
                                                        == f_const_data[31:24]);
 
                                else
 
                                        `ASSERT(f_cmem_here[31:24]
 
                                                        == f_const_data[31:24]);
 
                                if (c_wsel[2])
 
                                        `ASSERT(c_wdata[23:16]
 
                                                        == f_const_data[23:16]);
 
                                else
 
                                        `ASSERT(f_cmem_here[23:16] == f_const_data[23:16]);
 
                                if (c_wsel[1])
 
                                        `ASSERT(c_wdata[15:8]
 
                                                        == f_const_data[15:8]);
 
                                else
 
                                        `ASSERT(f_cmem_here[15:8] == f_const_data[15:8]);
 
                                if (c_wsel[0])
 
                                        `ASSERT(c_wdata[7:0]
 
                                                        == f_const_data[7:0]);
 
                                else
 
                                        `ASSERT(f_cmem_here[7:0] == f_const_data[7:0]);
 
                        end else
 
                                `ASSERT(f_cmem_here == f_const_data);
 
                end
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(state == DC_READC))
 
        begin
 
                `ASSERT(f_wb_tag == r_ctag);
 
                if ((wb_start[AW-1:LS] == f_const_tag)
 
                        &&(!c_v[f_const_tag_addr])
 
                        &&(f_const_addr[AW] == r_wb_cyc_lcl)
 
                        &&(f_nacks > f_const_addr[LS-1:0]))
 
                begin
 
                        // We are reading the cache line containing our
 
                        // constant address f_const_addr.  Make sure the data
 
                        // is correct.
 
                        if ((c_wr)&&(c_waddr[CS-1:0] == f_const_addr[CS-1:0]))
 
                                `ASSERT(c_wdata == f_const_data);
 
                        else
 
                                `ASSERT(f_cmem_here == f_const_data);
 
                end
 
 
 
                if (f_nacks > 0)
 
                        `ASSERT(!c_v[wb_start[CS-1:LS]]);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((state == DC_READC)&&(f_nacks > 0))
 
        begin
 
                `ASSERT(c_vtags[wb_start[(CS-1):LS]] <= wb_start[(AW-1):LS]);
 
                `ASSERT(c_vtags[wb_start[(CS-1):LS]] <= r_addr[AW-1:LS]);
 
        end
 
 
 
        reg     [AW-1:0] f_cache_waddr;
 
        wire                    f_this_cache_waddr;
 
 
 
        always @(*)
 
        begin
 
                // f_cache_waddr[AW-1:LS] = c_vtags[c_waddr[CS-1:CS-LS]];
 
                f_cache_waddr[AW-1:LS] = wb_start[AW-1:LS];
 
                f_cache_waddr[CS-1: 0] = c_waddr[CS-1:0];
 
        end
 
 
 
        assign  f_this_cache_waddr = (!f_const_addr[AW])
 
                                &&(f_cache_waddr == f_const_addr[AW-1:0]);
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(state == DC_READC))
 
        begin
 
                if ((c_wr)&&(c_waddr[LS-1:0] != 0)&&(f_this_cache_waddr))
 
                        `ASSERT(c_wdata == f_const_data);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((OPT_PIPE)&&(o_busy)&&(i_pipe_stb))
 
        begin
 
                `ASSUME(i_op[0] == o_wb_we);
 
                if (o_wb_cyc_lcl)
 
                        assume(&i_addr[DW-1:DW-8]);
 
                else
 
                        assume(!(&i_addr[DW-1:DW-8]));
 
        end
 
 
 
        initial f_pending_rd = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                f_pending_rd <= 0;
 
        else if (i_pipe_stb)
 
                f_pending_rd <= (!i_op[0]);
 
        else if ((o_valid)&&((!OPT_PIPE)
 
                ||((state != DC_READS)&&(!r_svalid)&&(!$past(i_pipe_stb)))))
 
                f_pending_rd <= 1'b0;
 
 
 
        always @(*)
 
        if ((state == DC_READC)&&(!f_stb))
 
                `ASSERT(f_nreqs == (1<<LS));
 
 
 
        always @(*)
 
        if ((state == DC_READC)&&(f_stb))
 
                `ASSERT(f_nreqs == { 1'b0, o_wb_addr[LS-1:0] });
 
 
 
        always @(posedge i_clk)
 
        if (state == DC_READC)
 
        begin
 
                if (($past(i_wb_ack))&&(!$past(f_stb)))
 
                        `ASSERT(f_nacks-1 == { 1'b0, c_waddr[LS-1:0] });
 
                else if (f_nacks > 0)
 
                begin
 
                        `ASSERT(f_nacks-1 == { 1'b0, c_waddr[LS-1:0] });
 
                        `ASSERT(c_waddr[CS-1:LS] == o_wb_addr[CS-1:LS]);
 
                end else begin
 
                        `ASSERT(c_waddr[CS-1:LS] == o_wb_addr[CS-1:LS]-1'b1);
 
                        `ASSERT(&c_waddr[LS-1:0]);
 
                end
 
        end
 
 
 
        always @(*)
 
        if (r_rd_pending)
 
                `ASSERT(r_addr == f_pending_addr[AW-1:0]);
 
 
 
        always @(*)
 
        if (f_pending_addr[AW])
 
        begin
 
                `ASSERT(state != DC_READC);
 
                `ASSERT((!o_wb_we)||(!o_wb_cyc_gbl));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(o_valid)&&($past(f_pending_addr) == f_const_addr))
 
        begin
 
                if (f_const_buserr)
 
                        `ASSERT(o_err);
 
                else if (f_pending_rd)
 
                begin
 
                        casez($past(req_data[3:0]))
 
                        4'b0???: `ASSERT(o_data ==f_const_data);
 
                        4'b101?: `ASSERT(o_data =={16'h00,f_const_data[15: 0]});
 
                        4'b100?: `ASSERT(o_data =={16'h00,f_const_data[31:16]});
 
                        4'b1100: `ASSERT(o_data =={24'h00,f_const_data[31:24]});
 
                        4'b1101: `ASSERT(o_data =={24'h00,f_const_data[23:16]});
 
                        4'b1110: `ASSERT(o_data =={24'h00,f_const_data[15: 8]});
 
                        4'b1111: `ASSERT(o_data =={24'h00,f_const_data[ 7: 0]});
 
                        endcase
 
                end
 
        end
 
 
 
        wire                    f_this_return;
 
 
 
        assign  f_this_return = (f_return_address == f_const_addr);
 
        always @(*)
 
        if ((f_cyc)&&(
 
                ((state == DC_READC)
 
                        &&(f_return_address[AW-1:LS] == f_const_addr[AW-1:LS]))
 
                ||(f_this_return))&&(f_cyc))
 
        begin
 
                if (f_const_buserr)
 
                        assume(!i_wb_ack);
 
                else begin
 
                        assume(!i_wb_err);
 
                        assume(i_wb_data == f_const_data);
 
                end
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(last_tag == f_const_tag)&&(f_const_buserr)
 
                        &&(!f_const_addr[AW]))
 
                `ASSERT(!last_tag_valid);
 
 
 
        always @(*)
 
        if (f_const_buserr)
 
        begin
 
                `ASSERT((!c_v[f_const_tag_addr])||(f_const_addr[AW])
 
                        ||(f_ctag_here != f_const_tag));
 
 
 
                if ((state == DC_READC)&&(wb_start[AW-1:LS] == f_const_tag))
 
                begin
 
                        `ASSERT(f_nacks <= f_const_tag[LS-1:0]);
 
                        if (f_nacks == f_const_tag[LS-1:0])
 
                                assume(!i_wb_ack);
 
                end
 
        end
 
 
 
`endif  // DCACHE
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        // Checking the lock
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
 
 
        always @(*)
 
                `ASSERT((!lock_gbl)||(!lock_lcl));
 
        always @(*)
 
        if (!OPT_LOCK)
 
                `ASSERT((!lock_gbl)&&(!lock_lcl));
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        // State based properties
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        reg     [F_LGDEPTH-1:0]  f_rdpending;
 
 
 
        initial f_rdpending = 0;
 
        always @(posedge i_clk)
 
        if ((i_reset)||(o_err))
 
                f_rdpending <= 0;
 
        else case({ (i_pipe_stb)&&(!i_op[0]), o_valid })
 
        2'b01: f_rdpending <= f_rdpending - 1'b1;
 
        2'b10: f_rdpending <= f_rdpending + 1'b1;
 
        default: begin end
 
        endcase
 
 
 
        wire    f_wb_cachable;
 
        iscachable #(.ADDRESS_WIDTH(AW))
 
                f_chkwb_addr(o_wb_addr, f_wb_cachable);
 
 
 
 
 
        always @(*)
 
        if (state == DC_IDLE)
 
        begin
 
                `ASSERT(!r_wb_cyc_gbl);
 
                `ASSERT(!r_wb_cyc_lcl);
 
 
 
                `ASSERT(!cyc);
 
 
 
                if ((r_rd_pending)||(r_dvalid)||(r_svalid))
 
                        `ASSERT(o_busy);
 
 
 
                if (!OPT_PIPE)
 
                begin
 
                        if (r_rd_pending)
 
                                `ASSERT(o_busy);
 
                        else if (r_svalid)
 
                                `ASSERT(o_busy);
 
                        else if (o_valid)
 
                                `ASSERT(!o_busy);
 
                        else if (o_err)
 
                                `ASSERT(!o_busy);
 
                end
 
        end else begin
 
                `ASSERT(o_busy);
 
                `ASSERT(cyc);
 
        end
 
 
 
 
 
 
 
        always @(posedge i_clk)
 
        if (state == DC_IDLE)
 
        begin
 
                if (r_svalid)
 
                begin
 
                        `ASSERT(!r_dvalid);
 
                        `ASSERT(!r_rd_pending);
 
                        if (!OPT_PIPE)
 
                                `ASSERT(!o_valid);
 
                        else if (o_valid)
 
                                `ASSERT(f_rdpending == 2);
 
                end
 
 
 
                if (r_dvalid)
 
                begin
 
                        `ASSERT(!r_rd_pending);
 
                        `ASSERT(npending == 0);
 
                        `ASSERT(f_rdpending == 1);
 
                end
 
 
 
                if (r_rd_pending)
 
                begin
 
                        if ((OPT_PIPE)&&(o_valid))
 
                                `ASSERT(f_rdpending <= 2);
 
                        else
 
                                `ASSERT(f_rdpending == 1);
 
 
 
                end else if ((OPT_PIPE)&&(o_valid)&&($past(r_dvalid|r_svalid)))
 
                                `ASSERT(f_rdpending <= 2);
 
                else
 
                        `ASSERT(f_rdpending <= 1);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if (state == DC_READC)
 
        begin
 
                `ASSERT( o_wb_cyc_gbl);
 
                `ASSERT(!o_wb_cyc_lcl);
 
                `ASSERT(!o_wb_we);
 
                `ASSERT(f_wb_cachable);
 
 
 
                `ASSERT(r_rd_pending);
 
                `ASSERT(r_cachable);
 
                if (($past(cyc))&&(!$past(o_wb_stb_gbl)))
 
                        `ASSERT(!o_wb_stb_gbl);
 
 
 
                if ((OPT_PIPE)&&(o_valid))
 
                        `ASSERT(f_rdpending == 2);
 
                else
 
                        `ASSERT(f_rdpending == 1);
 
        end
 
 
 
        always @(*)
 
        if (state == DC_READS)
 
        begin
 
                `ASSERT(!o_wb_we);
 
 
 
                if (OPT_PIPE)
 
                begin
 
                        if (o_valid)
 
                                `ASSERT((f_rdpending == npending + 1)
 
                                        ||(f_rdpending == npending));
 
                        else
 
                                `ASSERT(f_rdpending == npending);
 
                end
 
        end else if (state == DC_WRITE)
 
                `ASSERT(o_wb_we);
 
 
 
        always @(posedge i_clk)
 
        if ((state == DC_READS)||(state == DC_WRITE))
 
        begin
 
                `ASSERT(o_wb_we == (state == DC_WRITE));
 
                `ASSERT(!r_rd_pending);
 
                if (o_wb_we)
 
                        `ASSERT(f_rdpending == 0);
 
 
 
                if (OPT_PIPE)
 
                begin
 
                        casez({ $past(i_pipe_stb), f_stb })
 
                        2'b00: `ASSERT(npending == f_outstanding);
 
                        2'b1?: `ASSERT(npending == f_outstanding + 1);
 
                        2'b01: `ASSERT(npending == f_outstanding + 1);
 
                        endcase
 
 
 
                        if (state == DC_WRITE)
 
                                `ASSERT(!o_valid);
 
                end else
 
                        `ASSERT(f_outstanding <= 1);
 
        end
 
 
 
        always @(*)
 
        if (OPT_PIPE)
 
                `ASSERT(f_rdpending <= 2);
 
        else
 
                `ASSERT(f_rdpending <= 1);
 
 
 
        always @(posedge i_clk)
 
        if ((!OPT_PIPE)&&(o_valid))
 
                `ASSERT(f_rdpending == 1);
 
        else if (o_valid)
 
                `ASSERT(f_rdpending >= 1);
 
 
 
 
 
        always @(*)
 
        if ((!o_busy)&&(!o_err)&&(!o_valid))
 
                `ASSERT(f_rdpending == 0);
 
 
 
        always @(*)
 
                `ASSERT(cyc == ((r_wb_cyc_gbl)||(r_wb_cyc_lcl)));
 
 
 
        always @(*)
 
        if ((!i_reset)&&(f_nreqs == f_nacks)&&(!f_stb))
 
                `ASSERT(!cyc);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_err)))
 
                `ASSUME(!i_lock);
 
        else if ((f_past_valid)&&(OPT_LOCK)&&($past(i_lock))
 
                        &&((!$past(o_valid)) || ($past(i_pipe_stb))))
 
                `ASSUME($stable(i_lock));
 
 
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        // Ad-hoc properties
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        always @(*)
 
        if ((OPT_PIPE)&&(state == DC_WRITE)&&(!i_wb_stall)&&(stb)
 
                        &&(!npending[DP]))
 
                `ASSERT(!o_pipe_stalled);
 
 
 
        always @(posedge i_clk)
 
        if (state == DC_WRITE)
 
                `ASSERT(o_wb_we);
 
        else if ((state == DC_READS)||(state == DC_READC))
 
                `ASSERT(!o_wb_we);
 
 
 
        always @(*)
 
        if (cyc)
 
                `ASSERT(f_cyc);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(cyc))&&(!c_wr)&&(last_tag_valid)
 
                        &&(!r_rd_pending))
 
                `ASSERT((c_v[last_tag[(CS-LS-1):0]])
 
                        &&(c_vtags[last_tag[(CS-LS-1):0]] == last_tag));
 
 
 
        always @(*)
 
        if (!OPT_LOCAL_BUS)
 
        begin
 
                `ASSERT(r_wb_cyc_lcl == 1'b0);
 
                `ASSERT(o_wb_stb_lcl == 1'b0);
 
                `ASSERT(lock_lcl == 1'b0);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((state == DC_READC)&&(!stb))
 
        begin
 
                `ASSERT(o_wb_addr[LS-1:0] == 0);
 
                `ASSERT(o_wb_addr[AW-1:CS] == r_addr[AW-1:CS]);
 
        end else if ((state == DC_READC)&&(stb))
 
        begin
 
                `ASSERT(o_wb_addr[AW-1:CS] == r_addr[AW-1:CS]);
 
                `ASSERT(o_wb_addr[LS-1:0] == f_nreqs[LS-1:0]);
 
        end
 
 
 
        wire    [CS-1:0] f_expected_caddr;
 
        assign  f_expected_caddr = { r_ctag[CS-LS-1:0], {(LS){1'b0}} }-1
 
                                        + f_nacks;
 
        always @(posedge i_clk)
 
        if (state == DC_READC)
 
        begin
 
                if (LS == 0)
 
                        `ASSERT(end_of_line);
 
                else if (f_nacks < (1<<LS)-1)
 
                        `ASSERT(!end_of_line);
 
                else if (f_nacks == (1<<LS)-1)
 
                        `ASSERT(end_of_line);
 
                `ASSERT(f_nacks <= (1<<LS));
 
                `ASSERT(f_nreqs <= (1<<LS));
 
                if (f_nreqs < (1<<LS))
 
                begin
 
                        `ASSERT(o_wb_stb_gbl);
 
                        `ASSERT(o_wb_addr[(LS-1):0] == f_nreqs[LS-1:0]);
 
                end else
 
                        `ASSERT(!f_stb);
 
                `ASSERT((f_nreqs == 0)||(f_nacks <= f_nreqs));
 
                `ASSERT(c_waddr == f_expected_caddr);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(r_rd)&&(!$past(i_reset)))
 
        begin
 
                `ASSERT((o_busy)||(r_svalid));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if (!$past(o_busy))
 
                `ASSERT(!r_dvalid);
 
 
 
        always @(posedge i_clk)
 
        if ((state == DC_READC)&&(c_wr))
 
                `ASSERT(c_wsel == 4'hf);
 
 
 
        always @(*)
 
        if (c_wr)
 
                `ASSERT((c_wsel == 4'hf)
 
                        ||(c_wsel == 4'hc)
 
                        ||(c_wsel == 4'h3)
 
                        ||(c_wsel == 4'h8)
 
                        ||(c_wsel == 4'h4)
 
                        ||(c_wsel == 4'h2)
 
                        ||(c_wsel == 4'h1));
 
 
 
        always @(*)
 
        if (!OPT_PIPE)
 
                `ASSERT(o_pipe_stalled == o_busy);
 
        else if (o_pipe_stalled)
 
                `ASSERT(o_busy);
 
 
 
        //
 
        // Only ever abort on reset
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(cyc))&&(!$past(i_wb_err)))
 
        begin
 
                if (($past(i_pipe_stb))&&(!$past(o_pipe_stalled)))
 
                        `ASSERT(cyc);
 
                else if ($past(f_outstanding > 1))
 
                        `ASSERT(cyc);
 
                else if (($past(f_outstanding == 1))
 
                                &&((!$past(i_wb_ack))
 
                                        ||(($past(f_stb))
 
                                                &&(!$past(i_wb_stall)))))
 
                        `ASSERT(cyc);
 
                else if (($past(f_outstanding == 0))
 
                                &&($past(f_stb)&&(!$past(i_wb_ack))))
 
                        `ASSERT(cyc);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((OPT_PIPE)&&(f_past_valid)&&(!$past(i_reset))&&(state != DC_READC))
 
        begin
 
                if ($past(cyc && i_wb_err))
 
                begin
 
                        `ASSERT(npending == 0);
 
                end else if (($past(i_pipe_stb))||($past(i_wb_stall && stb)))
 
                        `ASSERT((npending == f_outstanding+1)
 
                                ||(npending == f_outstanding+2));
 
                else
 
                        `ASSERT(npending == f_outstanding);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((OPT_PIPE)&&(state != DC_READC)&&(state != DC_IDLE))
 
                `ASSERT(last_ack == (npending <= 1));
 
 
 
        always @(*)
 
        `ASSERT(stb == f_stb);
 
 
 
        always @(*)
 
        if (r_rd_pending)
 
                `ASSERT(!r_svalid);
 
 
 
        always @(*)
 
        if (o_err)
 
                `ASSUME(!i_pipe_stb);
 
 
 
        always @(*)
 
        if (last_tag_valid)
 
                `ASSERT(|c_v);
 
 
 
        always @(posedge i_clk)
 
        if ((cyc)&&(state == DC_READC)&&($past(f_nacks > 0)))
 
                `ASSERT(!c_v[o_wb_addr[CS-1:LS]]);
 
 
 
        always @(*)
 
        if (last_tag_valid)
 
        begin
 
                `ASSERT((!cyc)||(o_wb_we)||(state == DC_READS)
 
                                        ||(o_wb_addr[AW-1:LS] != last_tag));
 
        end
 
 
 
        wire    f_cachable_last_tag, f_cachable_r_addr;
 
 
 
        iscachable #(.ADDRESS_WIDTH(AW))
 
                fccheck_last_tag({last_tag, {(LS){1'b0}}}, f_cachable_last_tag);
 
 
 
        iscachable #(.ADDRESS_WIDTH(AW))
 
                fccheck_r_cachable(r_addr, f_cachable_r_addr);
 
 
 
        always @(*)
 
        if ((r_cachable)&&(r_rd_pending))
 
        begin
 
                `ASSERT(state != DC_WRITE);
 
                // `ASSERT(state != DC_READS);
 
                `ASSERT(f_cachable_r_addr);
 
                if (cyc)
 
                        `ASSERT(o_wb_addr[AW-1:LS] == r_addr[AW-1:LS]);
 
        end
 
 
 
        always @(*)
 
        if (last_tag_valid)
 
        begin
 
                `ASSERT(f_cachable_last_tag);
 
                `ASSERT(c_v[last_tag[CS-LS-1:0]]);
 
                `ASSERT(c_vtags[last_tag[CS-LS-1:0]]==last_tag);
 
                `ASSERT((state != DC_READC)||(last_tag != o_wb_addr[AW-1:LS]));
 
        end
 
 
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        // Cover statements
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
 
 
        always @(posedge i_clk)
 
                cover(o_valid);
 
 
 
        always @(posedge i_clk)
 
        if (f_past_valid)
 
                cover($past(r_svalid));
 
 
 
        generate if (OPT_PIPE)
 
        begin : PIPE_COVER
 
 
 
                wire            recent_reset;
 
                reg     [2:0]    recent_reset_sreg;
 
                initial recent_reset_sreg = -1;
 
                always @(posedge i_clk)
 
                if (i_reset)
 
                        recent_reset_sreg <= -1;
 
                else
 
                        recent_reset_sreg <= { recent_reset_sreg[1:0], 1'b0 };
 
 
 
                assign recent_reset = (i_reset)||(|recent_reset_sreg);
 
 
 
                //
 
                //
 
                wire    f_cvr_cread = (!recent_reset)&&(i_pipe_stb)&&(!i_op[0])
 
                                        &&(w_cachable);
 
 
 
                wire    f_cvr_cwrite = (!recent_reset)&&(i_pipe_stb)&&(i_op[0])
 
                                &&(!cache_miss_inow);
 
 
 
                wire    f_cvr_writes = (!recent_reset)&&(i_pipe_stb)&&(i_op[0])
 
                                        &&(!w_cachable);
 
                wire    f_cvr_reads  = (!recent_reset)&&(i_pipe_stb)&&(!i_op[0])
 
                                        &&(!w_cachable);
 
                wire    f_cvr_test  = (!recent_reset)&&(cyc);
 
 
 
                always @(posedge i_clk)
 
                if ((f_past_valid)&&($past(o_valid)))
 
                        cover(o_valid);         // !
 
 
 
                always @(posedge i_clk)
 
                if ((f_past_valid)&&(!$past(i_reset))&&($past(i_pipe_stb)))
 
                        cover(i_pipe_stb);
 
 
 
                always @(posedge i_clk)
 
                if ((f_past_valid)&&($past(o_valid))&&($past(o_valid,2)))
 
                        cover(o_valid);
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_cread))&&(f_cvr_cread));
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_cwrite))&&(f_cvr_cwrite));
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_writes))&&(f_cvr_writes));
 
 
 
                /*
 
                * This cover statement will never pass.  Why not?  Because
 
                * cache reads must be separated from non-cache reads.  Hence,
 
                * we can only allow a single non-cache read at a time, otherwise
 
                * we'd bypass the cache read logic.
 
                *
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_reads))&&(f_cvr_reads));
 
                */
 
 
 
                //
 
                // This is unrealistic, as it depends upon the Wishbone
 
                // acknoledging the request on the same cycle
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_reads,2))&&(f_cvr_reads));
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(r_dvalid))&&(r_svalid));
 
 
 
                //
 
                // A minimum of one clock must separate two dvalid's.
 
                // This option is rather difficult to cover, since it means
 
                // we must first load two separate cache lines before
 
                // this can even be tried.
 
                always @(posedge i_clk)
 
                        cover(($past(r_dvalid,2))&&(r_dvalid));
 
 
 
                //
 
                // This is the optimal configuration we want:
 
                //      i_pipe_stb
 
                //      ##1 i_pipe_stb && r_svalid
 
                //      ##1 r_svalid && o_valid
 
                //      ##1 o_valid
 
                // It proves that we can handle a 2 clock delay, but that
 
                // we can also pipelin these cache accesses, so this
 
                // 2-clock delay becomes a 1-clock delay between pipelined
 
                // memory reads.
 
                //
 
                always @(posedge i_clk)
 
                        cover(($past(r_svalid))&&(r_svalid));
 
 
 
                //
 
                // While we'd never do this (it breaks the ZipCPU's pipeline
 
                // rules), it's nice to know we could.
 
                //      i_pipe_stb && (!i_op[0]) // a read
 
                //      ##1 i_pipe_stb && (i_op[0]) && r_svalid // a write
 
                //      ##1 o_valid
 
                always @(posedge i_clk)
 
                        cover(($past(r_svalid))&&(f_cvr_writes));
 
 
 
                /* Unreachable
 
                *
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_writes))&&(o_valid));
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_writes,2))&&(o_valid));
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_writes,3))&&(o_valid));
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(r_dvalid,3))&&(r_dvalid));
 
 
 
                */
 
 
 
                always @(posedge i_clk)
 
                        cover(($past(f_cvr_writes,4))&&(o_valid));
 
 
 
        end endgenerate
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        // Carelesss assumption section
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
 
 
        //
 
        // Can't jump from local to global mid lock
 
        always @(*)
 
        if((OPT_LOCK)&&(OPT_LOCAL_BUS))
 
        begin
 
                if ((i_lock)&&(o_wb_cyc_gbl)&&(i_pipe_stb))
 
                        assume(!(&i_addr[(DW-1):(DW-8)]));
 
                else if ((i_lock)&&(o_wb_cyc_lcl)&&(i_pipe_stb))
 
                        assume(&i_addr[(DW-1):(DW-8)]);
 
        end
 
 
 
        always @(*)
 
        if ((OPT_PIPE)&&(o_busy || i_lock)&&(!o_pipe_stalled))
 
        begin
 
                if (i_pipe_stb)
 
                        assume((!OPT_LOCAL_BUS)
 
                                ||(f_pending_addr[AW]==(&i_addr[DW-1:DW-8])));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(cyc))&&(!cyc))
 
                assume((!i_wb_err)&&(!i_wb_ack));
 
 
 
`endif
endmodule
endmodule
 
 
 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.