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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [peripherals/] [zipmmu.v] - Diff between revs 201 and 209

Show entire file | Details | Blame | View Log

Rev 201 Rev 209
Line 101... Line 101...
//
//
//      Flags:
//      Flags:
//         1-bit        Read-only / ~written (user set/read/written)
//         1-bit        Read-only / ~written (user set/read/written)
//                              If set, this page will cause a fault on any
//                              If set, this page will cause a fault on any
//                              attempt to write this memory.
//                              attempt to write this memory.
 
//         1-bit        This page may be executed
 
//         1-bit        Cacheable
 
//                              This is not a hardware page, but a memory page.
 
//                              Therefore, the values within this page may be
 
//                              cached.
//         1-bit        Accessed
//         1-bit        Accessed
//                              This an be used to implement a least-recently
//                              This an be used to implement a least-recently
//                              used measure.  The hardware will set this value
//                              used measure.  The hardware will set this value
//                              when the page is accessed.  The user can also
//                              when the page is accessed.  The user can also
//                              set or clear this at will.
//                              set or clear this at will.
//         1-bit        Cacheable
 
//                              This is not a hardware page, but a memory page.
 
//                              Therefore, the values within this page may be
 
//                              cached.
 
//         1-bit        This context
 
//                              This is a read-only bit, indicating that the
 
//                              context register of this address matches the
 
//                              context register in the control word.
 
//
//
//              (Loaded flag    Not necessary, just map the physical page to 0)
//              (Loaded flag    Not necessary, just map the physical page to 0)
//
//
//      We could equivalently do a 16-bit V&P addresses, for a 28-bit total
//      We could equivalently do a 16-bit V&P addresses, for a 28-bit total
//      address space, if we didn't want to support the entire 32-bit space.
//      address space, if we didn't want to support the entire 32-bit space.
Line 138... Line 135...
//
//
//              On any write, the context bits will be set from the context
//              On any write, the context bits will be set from the context
//              bits in the control register.
//              bits in the control register.
//
//
//      +----+----+-----+----+----+----+----+--+--+--+--+
//      +----+----+-----+----+----+----+----+--+--+--+--+
//      |                         | Lower 8b| R| A| C| T|
//      |                         | Lower 8b| R| E| C| A|
//      |  20-bit Virtual page ID | Context | O| C| C| H|
//      |  20-bit Virtual page ID | Context | O| X| C| C|
//      |(top 20 bits of the addr)|   ID    | n| C| H| S|
//      |(top 20 bits of the addr)|   ID    | n| E| H| C|
//      |                         |         | W| S| E| P|
//      |                         |         | W| F| E| S|
//      +----+----+-----+----+----+----+----+--+--+--+--+
//      +----+----+-----+----+----+----+----+--+--+--+--+
//
//
//      +----+----+-----+----+----+----+----+--+--+--+--+
//      +----+----+-----+----+----+----+----+--+--+--+--+
//      |                         | Upper 8b| R| A| C| T|
//      |                         | Upper 8b| R| A| C| T|
//      |  20-bit Physical pg ID  | Context | O| C| C| H|
//      |  20-bit Physical pg ID  | Context | O| C| C| H|
//      |(top 20 bits of the      |   ID    | n| C| H| S|
//      |(top 20 bits of the      |   ID    | n| C| H| S|
//      |    physical address     |         | W| S| E| P|
//      |    physical address)    |         | W| S| E| P|
//      +----+----+-----+----+----+----+----+--+--+--+--+
//      +----+----+-----+----+----+----+----+--+--+--+--+
//
//
//      5. PF Cache--handles words in both physical and virtual
//      5. PF Cache--handles words in both physical and virtual
//      - On any pf-read, the MMU returns the current pagetable/TBL mapping
//      - On any pf-read, the MMU returns the current pagetable/TBL mapping
//              This consists of [Context,Va,Pa].
//              This consists of [Context,Va,Pa].
Line 187... Line 184...
// Creator:     Dan Gisselquist, Ph.D.
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//              Gisselquist Technology, LLC
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
// Copyright (C) 2016-2017, 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 209... Line 206...
// License:     GPL, v3, as defined and found on www.gnu.org,
// License:     GPL, v3, as defined and found on www.gnu.org,
//              http://www.gnu.org/licenses/gpl.html
//              http://www.gnu.org/licenses/gpl.html
//
//
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
module zipmmu(i_clk, i_reset, i_ctrl_cyc_stb, i_wbm_cyc, i_wbm_stb, i_wb_we,
//
                        i_wb_addr, i_wb_data,
//
                o_cyc, o_stb, o_we, o_addr, o_data,
`default_nettype        none
 
//
 
`define ROFLAG  3       // Read-only flag
 
`define EXEFLG  2       // No-execute flag (invalid for I-cache)
 
`define CHFLAG  1       // Cachable flag
 
`define AXFLAG  0        // Accessed flag
 
//
 
module zipmmu(i_clk, i_reset, i_wbs_cyc_stb, i_wbs_we, i_wbs_addr,
 
                                i_wbs_data, o_wbs_ack, o_wbs_stall, o_wbs_data,
 
                i_wbm_cyc, i_wbm_stb, i_wbm_we, i_wbm_exe,
 
                        i_wbm_addr, i_wbm_data, i_wbm_sel, i_gie,
 
                o_cyc, o_stb, o_we, o_addr, o_data, o_sel,
                        i_stall, i_ack, i_err, i_data,
                        i_stall, i_ack, i_err, i_data,
                        o_rtn_stall, o_rtn_ack, o_rtn_err,
                        o_rtn_stall, o_rtn_ack, o_rtn_err,
                                o_rtn_miss, o_rtn_data,
                                o_rtn_miss, o_rtn_data,
                pf_return_stb, pf_return_we,
                pf_return_stb, pf_return_we,
                                pf_return_p, pf_return_v,
                                pf_return_p, pf_return_v,
                                pf_return_cachable);
                                pf_return_cachable);
        parameter       ADDRESS_WIDTH=28, LGTBL=6, PLGPGSZ=12, PLGCTXT=16, DW=32;
        parameter       // The size of the address bus.  Actual addressable
 
                        // size will likely be 2^(ADDRESS_WIDTH+2) octets
 
                        ADDRESS_WIDTH=28,
 
                        // Number of page table entries
 
`ifdef  FORMAL
 
                        LGTBL=4'h2,
 
`else
 
                        LGTBL=4'h6,
 
`endif
 
                        // The requested log page size in 8-bit bytes
 
                        PLGPGSZB=20,
 
                        // Number of bits describing context
 
`ifdef  FORMAL
 
                        PLGCTXT=2;
 
`else
 
                        PLGCTXT=16;
 
`endif
 
        parameter [0:0] OPT_DELAY_RETURN = 1'b0;
        localparam      // And for our derived parameters (don't set these ...)
        localparam      // And for our derived parameters (don't set these ...)
 
                        // Width of the data bus is 32-bits.  This may be hard
 
                        // to change.
 
                        DW = 32,
                        // AW is just shorthand for the name ADDRESS_WIDTH
                        // AW is just shorthand for the name ADDRESS_WIDTH
                        AW = ADDRESS_WIDTH,
                        AW = ADDRESS_WIDTH,
                        // Page sizes must allow for a minimum of one context
                        // Page sizes must allow for a minimum of one context
                        // bit per page, plus four flag bits, hence the minimum
                        // bit per page, plus four flag bits, hence the minimum
                        // number of bits for an address within a page is 5
                        // number of bits for an address within a page is 5
                        LGPGSZ=(PLGPGSZ < 5)? 5:PLGPGSZ,
                        LGPGSZB=(PLGPGSZB < 5)? 5:PLGPGSZB,     // in bytes
                        // The number of context bits is twice the number of
                        LGPGSZW=LGPGSZB-2,                      // in words
                        // bits left over from DW after removing the LGPGSZ
                        // The context value for a given page can be split
                        // and flags bits.
                        // across both virtual and physical words.  It cannot
                        LGCTXT=(((DW-LGPGSZ-4)<<1)<PLGCTXT)?
                        // have so many bits to it that it takes more bits
                                ((DW-LGPGSZ-4)<<1):PLGCTXT,
                        // then are available.
 
                        LGCTXT=((2*LGPGSZB-4)>PLGCTXT)?
 
                                PLGCTXT:(2*LGPGSZB-4),
                        // LGLCTX is the number of context bits in the low word
                        // LGLCTX is the number of context bits in the low word
                        LGLCTX=((LGPGSZ-4)<LGCTXT)?(LGPGSZ-4):LGCTXT,
                        LGLCTX=(LGCTXT > (LGPGSZB-4))?(LGPGSZB-4):LGCTXT,
                        // LGHCTX is the number of context bits in the high word
                        // LGHCTX is the number of context bits in the high word
                        LGHCTX= (LGCTXT-LGLCTX),
                        LGHCTX= (LGCTXT-LGLCTX>0)?(LGCTXT-LGLCTX):0,
                        VAW=(DW-LGPGSZ), //  Virtual address width
                        VAW=(DW-LGPGSZB), //  Virtual address width, in bytes
                        PAW=(AW-LGPGSZ), // Physical address width
                        PAW=(AW-LGPGSZW), // Physical address width, in words
                        TBL_BITS = LGTBL,       // Bits necessary to addr tbl
                        TBL_BITS = LGTBL,       // Bits necessary to addr tbl
                        TBL_SIZE=(1<<TBL_BITS);// Number of table entries
                        TBL_SIZE=(1<<TBL_BITS);// Number of table entries
        input                   i_clk, i_reset;
        input   wire            i_clk, i_reset;
        //
 
        input                   i_ctrl_cyc_stb;
 
        //
 
        input                   i_wbm_cyc, i_wbm_stb;
 
        //
        //
        input                   i_wb_we;
        input   wire            i_wbs_cyc_stb;
        input   [(DW-1):0]       i_wb_addr;
        input   wire            i_wbs_we;
        input   [(DW-1):0]       i_wb_data;
        input   wire    [(LGTBL+1):0]    i_wbs_addr;
 
        input   wire    [(DW-1):0]       i_wbs_data;
 
        output  reg                     o_wbs_ack;
 
        output  wire                    o_wbs_stall;
 
        output  reg     [(DW-1):0]       o_wbs_data;
 
        //
 
        input   wire            i_wbm_cyc, i_wbm_stb;
 
        //
 
        input   wire                    i_wbm_we, i_wbm_exe;
 
        input   wire [(DW-2-1):0]        i_wbm_addr;
 
        input   wire [(DW-1):0]          i_wbm_data;
 
        input   wire [(DW/8-1):0]        i_wbm_sel;
 
        input   wire                    i_gie;
        //
        //
        // Here's where we drive the slave side of the bus
        // Here's where we drive the slave side of the bus
        output  reg                     o_cyc;
        output  reg                     o_cyc;
        output  wire                    o_stb, o_we;
        output  wire                    o_stb, o_we;
        output  reg     [(AW-1):0]       o_addr;
        output  reg     [(AW-1):0]       o_addr;
        output  reg     [(DW-1):0]       o_data;
        output  reg     [(DW-1):0]       o_data;
 
        output  reg     [(DW/8-1):0]     o_sel;
        // and get our return information from driving the slave ...
        // and get our return information from driving the slave ...
        input                           i_stall, i_ack, i_err;
        input   wire                    i_stall, i_ack, i_err;
        input           [(DW-1):0]       i_data;
        input   wire    [(DW-1):0]       i_data;
        //
        //
        // Here's where we return information on either our slave/control bus
        // Here's where we return information on either our slave/control bus
        // or the memory bus we are controlled from.  Note that we share these
        // or the memory bus we are controlled from.  Note that we share these
        // wires ...
        // wires ...
        output  wire            o_rtn_stall;
        output  wire            o_rtn_stall;
        output  reg             o_rtn_ack;
        output  wire            o_rtn_ack;
        output  wire            o_rtn_err, o_rtn_miss;
        output  wire            o_rtn_err, o_rtn_miss;
        output  [(DW-1):0]       o_rtn_data;
        output  wire [(DW-1):0]  o_rtn_data;
        // Finally, to allow the prefetch to snoop on the MMU conversion ...
        // Finally, to allow the prefetch to snoop on the MMU conversion ...
        output  wire                    pf_return_stb, // snoop data is valid
        output  wire                    pf_return_stb, // snoop data is valid
                                        pf_return_we; // snoop data is chnging
                                        pf_return_we; // snoop data is chnging
        output  wire    [(PAW-1):0]      pf_return_p;
        output  wire    [(PAW-1):0]      pf_return_p;
        output  wire    [(VAW-1):0]      pf_return_v;
        output  wire    [(VAW-1):0]      pf_return_v;
Line 277... Line 316...
        //
        //
 
 
//
//
//
//
//
//
        reg     [3:1]                   tlb_flags       [0:(TBL_SIZE-1)];
        reg     [3:0]                    tlb_flags       [0:(TBL_SIZE-1)];
 
        wire    [3:0]                    s_tlb_flags;
        reg     [(LGCTXT-1):0]           tlb_cdata       [0:(TBL_SIZE-1)];
        reg     [(LGCTXT-1):0]           tlb_cdata       [0:(TBL_SIZE-1)];
        reg     [(DW-LGPGSZ-1):0]        tlb_vdata       [0:(TBL_SIZE-1)];
        reg     [(VAW-1):0]              tlb_vdata       [0:(TBL_SIZE-1)];
        reg     [(AW-LGPGSZ-1):0]        tlb_pdata       [0:(TBL_SIZE-1)];
        reg     [(PAW-1):0]              tlb_pdata       [0:(TBL_SIZE-1)];
 
        reg     [(TBL_SIZE-1):0] tlb_valid, tlb_accessed;
 
 
        wire    adr_control, adr_status, adr_vtable, adr_ptable;
        wire    adr_control, adr_vtable, adr_ptable;
        wire    wr_control, wr_status, wr_vtable, wr_ptable;
        wire    wr_control, wr_vtable, wr_ptable;
        wire    [(LGTBL-1):0]    wr_tlb_addr;
        wire    [(LGTBL-1):0]    wr_tlb_addr;
        assign  wr_tlb_addr= i_wb_addr[(LGTBL):1]; // Leave bottom for V/P
        assign  wr_tlb_addr= i_wbs_addr[(LGTBL):1]; // Leave bottom for V/P
        assign  adr_control= (i_ctrl_cyc_stb)&&(~i_wb_addr[(LGTBL+1)])&&(~i_wb_addr[0]);
        assign  adr_control= (i_wbs_cyc_stb)&&(~i_wbs_addr[(LGTBL+1)])&&(~i_wbs_addr[0]);
        assign  adr_status = (i_ctrl_cyc_stb)&&(~i_wb_addr[(LGTBL+1)])&&( i_wb_addr[0]);
        assign  adr_vtable = (i_wbs_cyc_stb)&&( i_wbs_addr[(LGTBL+1)])&&(~i_wbs_addr[0]);
        assign  adr_vtable = (i_ctrl_cyc_stb)&&( i_wb_addr[(LGTBL+1)])&&(~i_wb_addr[0]);
        assign  adr_ptable = (i_wbs_cyc_stb)&&( i_wbs_addr[(LGTBL+1)])&&( i_wbs_addr[0]);
        assign  adr_ptable = (i_ctrl_cyc_stb)&&( i_wb_addr[(LGTBL+1)])&&( i_wb_addr[0]);
        assign  wr_control = (adr_control)&&(i_wbs_we);
        assign  wr_control = (adr_control)&&(i_wb_we);
        assign  wr_vtable  = (adr_vtable )&&(i_wbs_we);
        assign  wr_status  = (adr_status )&&(i_wb_we);
        assign  wr_ptable  = (adr_ptable )&&(i_wbs_we);
        assign  wr_vtable  = (adr_vtable )&&(i_wb_we);
 
        assign  wr_ptable  = (adr_ptable )&&(i_wb_we);
        reg                     z_context;
 
        wire                    kernel_context;
        reg                     setup_ack, z_context, setup_this_page_flag;
        reg     [(LGCTXT-1):0]   r_context_word;
        reg     [(DW-1):0]       setup_data;
 
        reg     [(LGCTXT-1):0]   r_context_word, setup_page;
 
        //
        //
        wire    [31:0]           w_control_data,w_vtable_reg,w_ptable_reg;
        wire    [31:0]           w_control_data, w_ptable_reg;
        wire    [(LGCTXT-1):0]   w_ctable_reg;
        reg     [31:0]           w_vtable_reg;
        reg     [31:0]   status_word;
        reg     [31:0]   status_word;
        //
        //
        reg             rf_miss, rf_ropage, rf_table_err;
 
        wire    [31:0]   control_word;
 
        wire    [3:0]    lgaddr_bits, lgtblsz_bits, lgpagesz_bits,
 
                        lgcontext_bits;
 
 
 
        reg     [(AW-(LGPGSZ)):0]        r_mmu_err_vaddr;
 
        wire    [(DW-LGPGSZ):0]          w_mmu_err_vaddr;
 
        //
        //
        reg                     r_pending, r_we, last_page_valid, last_ro, r_valid;
        reg                     r_pending, r_we, r_exe, r_valid,
        reg     [(DW-1):0]       r_addr;
                                last_page_valid, last_ro, last_exe;
 
        reg     [(DW-3):0]       r_addr;
        reg     [(DW-1):0]       r_data;
        reg     [(DW-1):0]       r_data;
 
        wire    [(VAW-1):0]      vpage;
 
        wire    [AW-LGPGSZW-1:0] ppage;
 
        reg     [(DW/8-1):0]     r_sel;
        reg     [(PAW-1):0]      last_ppage;
        reg     [(PAW-1):0]      last_ppage;
        reg     [(VAW-1):0]      last_vpage;
        reg     [(VAW-1):0]      last_vpage;
        //
        //
        wire    [(TBL_SIZE-1):0] r_tlb_match;
        wire    [(TBL_SIZE-1):0] r_tlb_match;
        reg     [(LGTBL-1):0]            s_tlb_addr;
        reg     [(LGTBL-1):0]            s_tlb_addr, last_tlb;
        reg                             s_tlb_miss, s_tlb_hit, s_pending;
        reg                             s_tlb_miss, s_tlb_hit, s_pending;
        //
        //
        wire    ro_flag, simple_miss, ro_miss, table_err, cachable;
        wire    ro_flag, exe_flag, simple_miss, ro_miss, exe_miss, table_err, cachable;
        reg     p_tlb_miss,p_tlb_err, pf_stb, pf_cachable;
        reg     pf_stb, pf_cachable;
 
        reg     miss_pending;
        //
        //
        reg     rtn_err;
        reg     rtn_err;
 
 
 
 
 
        wire    this_page_valid, pending_page_valid;
 
        assign  this_page_valid = ((last_page_valid)
 
                                &&(i_wbm_addr[(DW-3):(DW-2-VAW)]==last_vpage)
 
                                &&((!last_ro)||(!i_wbm_we))
 
                                &&((!last_exe)||(!i_wbm_exe)));
 
        assign  pending_page_valid = ((s_pending)&&(s_tlb_hit)
 
                                &&((!r_we)||(!ro_flag))
 
                                &&((!r_exe)||(exe_flag)));
 
 
        //////////////////////////////////////////
        //////////////////////////////////////////
        //
        //
        //
        //
        // Step one -- handle the control bus--i_ctrl_cyc_stb
        // Step one -- handle the control bus--i_wbs_cyc_stb
        //
        //
        //
        //
        //////////////////////////////////////////
        //////////////////////////////////////////
        always @(posedge i_clk)
        always @(posedge i_clk)
        begin
        begin
                // Write to the Translation lookaside buffer
                // Write to the Translation lookaside buffer
                if (wr_vtable)
                if (wr_vtable)
                        tlb_vdata[wr_tlb_addr]<=i_wb_data[(DW-1):LGPGSZ];
                        tlb_vdata[wr_tlb_addr]<=i_wbs_data[(DW-1):LGPGSZB];
                if (wr_ptable)
                if (wr_ptable)
                        tlb_pdata[wr_tlb_addr]<=i_wb_data[(AW-1):LGPGSZ];
                        tlb_pdata[wr_tlb_addr]<=i_wbs_data[(AW+1):LGPGSZB];
                // Set the context register for the page
                // Set the context register for the page
                if ((wr_vtable)||(wr_ptable))
 
                        tlb_flags[wr_tlb_addr] <= i_wb_data[3:1];
 
                // Otherwise, keep track of the accessed bit if we ever access this page
 
                else if ((!z_context)&&(r_pending)&&(s_tlb_hit)&&((!r_we)||(!ro_flag)))
 
                        tlb_flags[s_tlb_addr][2] <= 1'b1;
 
                if (wr_vtable)
                if (wr_vtable)
                        tlb_cdata[wr_tlb_addr][((LGCTXT>=8)? 7:(LGCTXT-1)):0]
                        tlb_flags[wr_tlb_addr] <= { i_wbs_data[3:1], 1'b0 };
                                <= i_wb_data[((LGCTXT>=8)? 11:(4+LGCTXT-1)):4];
                if (wr_vtable)
                if ((wr_ptable)&&(LGCTXT > 8))
                        tlb_cdata[wr_tlb_addr][(LGLCTX-1):0]
                        tlb_cdata[wr_tlb_addr][(LGCTXT-1):8]
                                <= i_wbs_data[(LGLCTX+4-1):4];
                                <= i_wb_data[(4+LGCTXT-8-1):4];
 
                setup_ack <= (i_ctrl_cyc_stb)&&(!i_reset);
 
        end
        end
 
 
 
        initial tlb_accessed = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                tlb_accessed <= 0;
 
        else begin
 
                if (wr_vtable)
 
                        tlb_accessed[wr_tlb_addr] <= 1'b0;
 
                // Otherwise, keep track of the accessed bit if we
 
                // ever access this page
 
                else if ((!kernel_context)&&(pending_page_valid))
 
                        tlb_accessed[s_tlb_addr] <= 1'b1;
 
                else if ((!kernel_context)&&(this_page_valid))
 
                        tlb_accessed[last_tlb] <= 1'b1;
 
        end
 
 
 
        generate if (LGHCTX > 0)
 
        begin : HCTX
 
                always @(posedge i_clk)
 
                if (wr_ptable)
 
                        tlb_cdata[wr_tlb_addr][(LGCTXT-1):LGLCTX]
 
                                <= i_wbs_data[(LGHCTX+4-1):4];
 
        end endgenerate
 
 
        // Writing to the control word
        // Writing to the control word
        initial z_context = 1'b1;
        initial z_context = 1'b1;
        initial r_context_word = 0;
        initial r_context_word = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
        if (wr_control)
        if (wr_control)
                begin
                begin
                r_context_word <= i_wb_data[(LGCTXT-1):0];
                r_context_word <= i_wbs_data[(LGCTXT-1):0];
                z_context      <= (i_wb_data[(LGCTXT-1):0] == {(LGCTXT){1'b0}});
                z_context      <= (i_wbs_data[(LGCTXT-1):0] == {(LGCTXT){1'b0}});
                end
                end
 
        assign  kernel_context = (z_context)||(!i_gie);
        // Status words cannot be written to
        // Status words cannot be written to
 
 
        /* verilator lint_off WIDTH */
        always @(posedge i_clk)
        assign  w_control_data[31:28] = AW-17;
        if (i_reset)
        assign  w_control_data[27:24] = LGTBL;
                tlb_valid <= 0;
        assign  w_control_data[23:20] = LGPGSZ-8;
        else if (wr_ptable)
        assign  w_control_data[19:16] = LGCTXT-1;
                tlb_valid[wr_tlb_addr]<=1'b1; //(i_wbs_data[(AW+1):LGPGSZB]!=0);
        /* verilator lint_on WIDTH */
 
 
        /* v*rilator lint_off WIDTH */
 
        assign  w_control_data[31:28] = AW[3:0]-4'd1;
 
        assign  w_control_data[27:24] = LGTBL[3:0];
 
        assign  w_control_data[23:20] = LGPGSZB[3:0]-4'd10;
 
        assign  w_control_data[19:16] = LGCTXT[3:0]-1'b1;
 
        /* v*rilator lint_on WIDTH */
        assign  w_control_data[15: 0] = {{(16-LGCTXT){1'b0}}, r_context_word};
        assign  w_control_data[15: 0] = {{(16-LGCTXT){1'b0}}, r_context_word};
        //
        //
        assign  w_vtable_reg[(DW-1):LGPGSZ] = tlb_vdata[wr_tlb_addr];
        always @(*)
        assign  w_vtable_reg[(LGPGSZ-1):(LGLCTX+4-1)] = 0;
        begin
        assign  w_vtable_reg[(LGLCTX+4-1):4] = { tlb_cdata[wr_tlb_addr][(LGLCTX-1):0] };
                w_vtable_reg = 0;
        assign  w_vtable_reg[ 3:0]  = { tlb_flags[wr_tlb_addr], 1'b0 };
                w_vtable_reg[(DW-1):LGPGSZB] = tlb_vdata[wr_tlb_addr];
 
                w_vtable_reg[(LGLCTX+4-1):4] = { tlb_cdata[wr_tlb_addr][(LGLCTX-1):0] };
 
                w_vtable_reg[ 3:0]  = { tlb_flags[wr_tlb_addr][3:1],
 
                                        tlb_accessed[wr_tlb_addr] };
 
        end
        //
        //
        assign  w_ptable_reg[(DW-1):LGPGSZ] = { {(DW-AW){1'b0}},
        assign  w_ptable_reg[(DW-1):LGPGSZB] = { {(DW-PAW-LGPGSZB){1'b0}},
                                        tlb_pdata[wr_tlb_addr] };
                                        tlb_pdata[wr_tlb_addr] };
        assign  w_ptable_reg[LGPGSZ:(4+LGHCTX)] = 0;
        assign  w_ptable_reg[ 3:0]  = 4'h0;
        assign  w_ptable_reg[ 3:0]  = { tlb_flags[wr_tlb_addr], 1'b0 };
 
        assign  w_ctable_reg = tlb_cdata[wr_tlb_addr];
 
        //
        //
        generate
        generate
                if (4+LGHCTX-1>4)
                if (4+LGHCTX-1>4)
                        assign  w_ptable_reg[(4+LGHCTX-1):4] =  {
                        assign  w_ptable_reg[(4+LGHCTX-1):4] =  {
                                tlb_cdata[wr_tlb_addr][(LGCTXT-1):LGLCTX] };
                                tlb_cdata[wr_tlb_addr][(LGCTXT-1):LGLCTX] };
 
                if (LGPGSZB > LGLCTX+4)
 
                        assign  w_vtable_reg[(LGPGSZB-1):(LGLCTX+4)] = 0;
 
                if (LGPGSZB > LGHCTX+4)
 
                        assign  w_ptable_reg[(LGPGSZB-1):(LGHCTX+4)] = 0;
        endgenerate
        endgenerate
 
 
 
        //
        // Now, reading from the bus
        // Now, reading from the bus
        always @(posedge i_clk)
        /*
                setup_page <= w_ctable_reg;
        wire    [(LGCTXT-1):0]  w_ctable_reg;
        always @(posedge i_clk)
        assign  w_ctable_reg = tlb_cdata[wr_tlb_addr];
                setup_this_page_flag <= (i_ctrl_cyc_stb)&&(i_wb_addr[LGTBL+1]);
        reg                     setup_this_page_flag;
        always @(posedge i_clk)
        reg     [(LGCTXT-1):0]  setup_page;
                case({i_wb_addr[LGTBL+1],i_wb_addr[0]})
        initial setup_this_page_flag = 1'b0;
                2'b00: setup_data <= w_control_data;
        always @(posedge i_clk)
                2'b01: setup_data <= status_word;
                setup_page <= w_ctable_reg;
                2'b10: setup_data <= w_vtable_reg;
        always @(posedge i_clk)
                2'b11: setup_data <= w_ptable_reg;
                setup_this_page_flag <= (!i_reset)&&(i_wbs_cyc_stb)&&(i_wbs_addr[LGTBL+1]);
                endcase
        */
 
 
 
 
 
 
        //////////////////////////////////////////
        //////////////////////////////////////////
        //
        //
        //
        //
        // Step two -- handle the page lookup on the master bus
        // Step two -- handle the page lookup on the master bus
        //
        //
        //
        //
        //////////////////////////////////////////
        //////////////////////////////////////////
        assign w_mmu_err_vaddr = { {(DW-AW){1'b0}}, r_mmu_err_vaddr };
 
 
 
        //
        //
        //
        //
        // First clock, and the r_ register, copies the bus data from the bus.
        // First clock, and the r_ register, copies the bus data from the bus.
        // While this increases the bus latency, it also gives us a moment to
        // While this increases the bus latency, it also gives us a moment to
        // work.
        // work.
        //
        //
        //
        //
 
        wire    [(VAW-1):0]      r_vpage;
 
        wire    [(PAW-1):0]      r_ppage;
 
        assign  r_vpage = (r_addr[(DW-3):(DW-2-VAW)]);
 
        assign  r_ppage = (o_addr[(AW-1):LGPGSZW]);
 
 
 
        initial s_pending = 1'b0;
        initial r_pending = 1'b0;
        initial r_pending = 1'b0;
        initial r_valid   = 1'b0;
        initial r_valid   = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
 
        begin
 
                r_pending <= 1'b0;
 
                r_valid   <= 1'b0;
 
                o_addr    <= 0;
 
                r_we      <= 0;
 
                r_exe     <= 0;
 
                r_addr    <= 0;
 
                r_data    <= 0;
 
                r_sel     <= 0;
 
                //
 
                s_pending <= 1'b0;
 
        end else
        begin
        begin
                if (!o_rtn_stall)
                if (!o_rtn_stall)
                begin
                begin
                        r_pending <= i_wbm_stb;
                        r_pending <= (i_wbm_stb)&&(!kernel_context)
                        r_we      <= i_wb_we;
                                                &&(!this_page_valid);
                        r_addr    <= i_wb_addr;
                        r_we      <= i_wbm_we;
                        r_data    <= i_wb_data;
                        r_exe     <= i_wbm_exe;
                        r_valid   <= (i_wbm_stb)&&((z_context)||((last_page_valid)
                        o_addr    <= { { (kernel_context)?
                                        &&(i_wb_addr[(DW-1):LGPGSZ] == last_vpage)
                                i_wbm_addr[(AW-1):LGPGSZW] : last_ppage },
                                        &&((!last_ro)||(!i_wb_we))));
                                i_wbm_addr[(LGPGSZW-1):0] };
 
                        r_addr    <= i_wbm_addr;
 
                        r_data    <= i_wbm_data;
 
                        r_sel     <= i_wbm_sel;
 
                        r_valid   <= (i_wbm_stb)&&((kernel_context)||(this_page_valid));
                        s_pending <= 1'b0;
                        s_pending <= 1'b0;
 
                end else if (!r_valid) begin
 
                        r_valid <= (pending_page_valid);
 
                        o_addr <= { ppage , r_addr[(LGPGSZW-1):0] };
 
                        r_pending<= (r_pending)&&(!pending_page_valid);
 
                        s_pending <=(r_pending)&&(!pending_page_valid);
                end else begin
                end else begin
                        r_valid <= (r_valid)||((last_page_valid)
                        r_pending <= 1'b0;
                                        &&(r_addr[(DW-1):LGPGSZ] == last_vpage)
                        s_pending <= 1'b0;
                                        &&((!last_ro)||(!r_we)));
 
                        r_pending<= (r_pending)&&(i_wbm_cyc);
 
                        s_pending <= r_pending;
 
                end
                end
 
 
                if (i_reset)
                if ((!i_wbm_cyc)||(o_rtn_err)||((o_cyc)&&(i_err)))
 
                begin
 
                        s_pending <= 1'b0;
                        r_pending <= 1'b0;
                        r_pending <= 1'b0;
 
                        r_valid   <= 1'b0;
 
                end
        end
        end
 
 
 
`ifdef  FORMAL
 
        reg     f_past_valid;
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(r_pending))&&(r_pending)&&($past(o_rtn_stall))&&(i_wbm_cyc)&&(!o_stb))
 
                assert(s_pending);
 
`endif
 
 
        // Second clock: know which buffer entry this belong in.
        // Second clock: know which buffer entry this belong in.
        // If we don't already know, then the pipeline must be stalled for a
        // If we don't already know, then the pipeline must be stalled for a
        // while ...
        // while ...
        genvar k, s;
        genvar k, s;
        generate
        generate
        for(k=0; k<TBL_BITS; k = k + 1)
        for(k=0; k<TBL_SIZE; k = k + 1)
                assign r_tlb_match[k] =
                assign r_tlb_match[k] =
 
                        // The page  must be valid
 
                        (tlb_valid[k])
                        // Virtual address must match
                        // Virtual address must match
                        ((tlb_vdata[k] == r_addr[(DW-1):LGPGSZ])
                        &&(tlb_vdata[k] == r_vpage)
                        // Context must match as well
                        // Context must match as well
                                &&(tlb_cdata[k] == r_context_word));
                        &&(tlb_cdata[k][LGCTXT-1:1] == r_context_word[LGCTXT-1:1])
 
                        &&((!tlb_cdata[k][0])||(r_context_word[0]));
        endgenerate
        endgenerate
 
 
        initial s_tlb_miss = 1'b0;
        initial s_tlb_miss = 1'b0;
        initial s_tlb_hit  = 1'b0;
        initial s_tlb_hit  = 1'b0;
        generate
        generate
 
                integer i;
        always @(posedge i_clk)
        always @(posedge i_clk)
        begin // valid when s_ becomes valid
        begin // valid when s_ becomes valid
                s_tlb_addr <= {(LGTBL){1'b0}};
                s_tlb_addr <= {(LGTBL){1'b0}};
                for(k=0; k<TBL_SIZE; k=k+1)
                for(i=0; i<TBL_SIZE; i=i+1)
                        for(s=0; s<LGTBL; s=s+1)
                        if (r_tlb_match[i])
                                if (((k&(1<<s))!=0)&&(r_tlb_match[k]))
                                s_tlb_addr <= i[(LGTBL-1):0];
                                        s_tlb_addr[s] <= 1'b1;
                s_tlb_miss <= (r_pending)&&(r_tlb_match == 0);
                s_tlb_miss <= (r_pending)&&(r_tlb_match[(TBL_BITS-1):0] == 0);
 
                s_tlb_hit <= 1'b0;
                s_tlb_hit <= 1'b0;
                for(k=0; k<TBL_SIZE; k=k+1)
                for(i=0; i<TBL_SIZE; i=i+1)
                        if (r_tlb_match == (1<<k))
                        if (r_tlb_match == (1<<i))
                                s_tlb_hit <= (r_pending);
                                s_tlb_hit <= (r_pending)&&(!r_valid)&&(i_wbm_cyc);
        end endgenerate
        end endgenerate
 
 
 
 
        // Third clock: Read from the address the virtual table offset,
        // Third clock: Read from the address the virtual table offset,
        // whether read-only, etc.
        // whether read-only, etc.
        assign  ro_flag     = tlb_flags[s_tlb_addr][3];
        assign  s_tlb_flags = tlb_flags[s_tlb_addr];
 
        assign  ro_flag     = s_tlb_flags[`ROFLAG];
 
        assign  exe_flag    = s_tlb_flags[`EXEFLG];
 
        assign  cachable    = s_tlb_flags[`CHFLAG];
        assign  simple_miss = (s_pending)&&(s_tlb_miss);
        assign  simple_miss = (s_pending)&&(s_tlb_miss);
        assign  ro_miss     = (s_pending)&&(s_tlb_hit)&&(r_we)&&(ro_flag);
        assign  ro_miss     = (s_pending)&&(s_tlb_hit)&&(r_we)&&(ro_flag);
 
        assign  exe_miss    = (s_pending)&&(s_tlb_hit)&&(r_exe)&&(!exe_flag);
        assign  table_err   = (s_pending)&&(!s_tlb_miss)&&(!s_tlb_hit);
        assign  table_err   = (s_pending)&&(!s_tlb_miss)&&(!s_tlb_hit);
        assign  cachable    = tlb_flags[s_tlb_addr][1];
        assign  vpage       = tlb_vdata[s_tlb_addr];
        // assign       tlb_access_flag    = tlb_flags[s_tlb_addr][2];
        assign  ppage       = tlb_pdata[s_tlb_addr];
 
 
 
        initial pf_cachable = 1'b0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                pf_cachable <= 1'b0;
 
        else
 
                pf_cachable <= cachable;
 
 
        initial pf_stb = 1'b0;
        initial pf_stb = 1'b0;
        initial p_tlb_err  = 1'b0;
        initial last_ppage = 0;
        initial p_tlb_miss = 1'b0;
        initial last_vpage = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
        begin
        begin
                p_tlb_miss <= (simple_miss)||(ro_miss);
                pf_stb <= 1'b0;
                p_tlb_err  <= (s_pending)&&((!s_tlb_miss)&&(!s_tlb_hit));
                last_ppage <= 0;
 
                last_vpage <= 0;
                pf_cachable <= cachable;
                last_tlb   <= 0;
                if ((!z_context)&&(r_pending))
        end else if ((!kernel_context)&&(r_pending)&&(!last_page_valid))
                begin
                begin
                        last_ppage <= tlb_pdata[s_tlb_addr];
                last_tlb   <= s_tlb_addr;
                        last_vpage <= tlb_vdata[s_tlb_addr];
                last_ppage <= ppage;
 
                last_vpage <= vpage;
 
                last_exe   <= exe_flag;
                        last_ro    <= ro_flag;
                        last_ro    <= ro_flag;
                        pf_stb <= 1'b1;
                        pf_stb <= 1'b1;
                end else
                end else
                        pf_stb <= 1'b0;
                        pf_stb <= 1'b0;
                if ((table_err)||(ro_miss)||(simple_miss))
 
                        status_word <= { r_addr[(DW-1):LGPGSZ],
 
                                {(LGPGSZ-3){1'b0}},
 
                                (table_err), (ro_miss), (simple_miss) };
 
 
 
                if (wr_control)
        initial status_word = 0;
                        last_page_valid <= (last_page_valid)
        always @(posedge i_clk)
                          &&(r_context_word == i_wb_data[(LGCTXT-1):0]);
        if (i_reset)
                else if ((r_pending)&&(!z_context))
                status_word <= 0;
                        last_page_valid <= (s_tlb_hit)&&(!ro_miss);
        else if (wr_control)
 
                status_word <= 0;
 
        else if ((table_err)||(ro_miss)||(simple_miss)||(exe_miss))
 
                status_word <= { r_vpage,
 
                                {(LGPGSZB-4){1'b0}},
 
                                (table_err), (exe_miss),
 
                                (ro_miss), (simple_miss) };
 
 
 
        initial last_page_valid = 1'b0;
 
        always @(posedge i_clk)
                if (i_reset)
                if (i_reset)
                        last_page_valid <= 1'b0;
                        last_page_valid <= 1'b0;
 
        else if ((i_wbs_cyc_stb)&&(i_wbs_we))
 
                last_page_valid <= 1'b0;
 
        else if (!kernel_context)
 
        begin
 
                if (!o_rtn_stall)
 
                        // A new bus request
 
                        last_page_valid <= (last_page_valid)
 
                                &&(i_wbm_addr[(DW-3):(DW-2-VAW)] == last_vpage);
 
                else if ((r_pending)&&(!last_page_valid))
 
                        last_page_valid <= (s_pending)&&(s_tlb_hit);
        end
        end
 
 
 
        parameter       LGFIFO = 6;
 
        reg     [LGFIFO-1:0]     bus_outstanding;
 
        initial bus_outstanding = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                bus_outstanding <= 0;
 
        else if (!o_cyc)
 
                bus_outstanding <= 0;
 
        else case({ (o_stb)&&(!i_stall), (i_ack)||(i_err) } )
 
        2'b01: bus_outstanding <= bus_outstanding - 1'b1;
 
        2'b10: bus_outstanding <= bus_outstanding + 1'b1;
 
        default: begin end
 
        endcase
 
 
 
        reg     bus_pending;
 
        initial bus_pending = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                bus_pending <= 0;
 
        else if (!o_cyc)
 
                bus_pending <= 1'b0;
 
        else case({ (o_stb)&&(!i_stall), ((i_ack)||(i_err)) })
 
        2'b01: bus_pending <= (bus_outstanding > 1);
 
        2'b10: bus_pending <= 1'b1;
 
        default: begin end
 
        endcase
 
 
        initial rtn_err = 1'b0;
        initial rtn_err = 1'b0;
 
        initial o_cyc   = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
        begin
        begin
                o_cyc <=  (!i_reset)&&(i_wbm_cyc);
                o_cyc <= 1'b0;
 
                rtn_err   <= 1'b0;
 
        end else begin
 
                o_cyc <=  (i_wbm_cyc)&&(!o_rtn_err)&&((!i_err)||(!o_cyc)); /// &&((o_cyc)||(r_valid));
 
 
                o_rtn_ack  <= (!i_reset)&&((setup_ack)||(i_wbm_cyc)&&(i_ack));
                rtn_err  <= (i_wbm_cyc)&&(i_err)&&(o_cyc);
                o_rtn_data <= (setup_ack) ? setup_data : i_data;
 
                if (setup_this_page_flag)
 
                        o_rtn_data[0] <= ((setup_page == r_context_word)? 1'b1:1'b0);
 
                rtn_err  <= (!i_reset)&&(i_wbm_cyc)&&(i_err);
 
        end
        end
 
 
 
        generate if (OPT_DELAY_RETURN)
 
        begin
 
                reg             r_rtn_ack;
 
                reg     [31:0]   r_rtn_data;
 
 
 
                initial r_rtn_data = 0;
 
                initial r_rtn_ack  = 0;
 
                always @(posedge i_clk)
 
                if (i_reset)
 
                begin
 
                        r_rtn_ack  <= 0;
 
                        r_rtn_data <= 0;
 
                end else begin
 
                        r_rtn_ack  <= (i_wbm_cyc)&&(i_ack)&&(o_cyc);
 
                        r_rtn_data <= i_data;
 
                end
 
 
 
                assign  o_rtn_ack  = r_rtn_ack;
 
                assign  o_rtn_data = r_rtn_data;
 
        end else begin
 
 
 
                assign  o_rtn_ack  = (i_ack)&&(o_cyc);
 
                assign  o_rtn_data = i_data;
 
        end endgenerate
 
 
        assign  o_stb = (r_valid);
        assign  o_stb = (r_valid);
        assign  o_we  =  (r_we);
        assign  o_we  =  (r_we);
        assign  o_rtn_stall = (i_wbm_cyc)&&(((r_pending)&&(!r_valid))||(i_stall));
        assign  o_rtn_stall = (i_wbm_cyc)&&(
        assign  o_rtn_miss  = p_tlb_miss;
                        (o_rtn_err)
        assign  o_rtn_err   = (rtn_err)||(p_tlb_err);
                        ||((r_pending)&&(!r_valid))
 
                        ||((o_stb)&&(i_stall))
        assign  o_addr[(AW-1):0] = {(z_context)?
                        ||(miss_pending));
                                r_addr[(AW-1):LGPGSZ] : last_ppage,
 
                        r_addr[(LGPGSZ-1):0]};
        initial miss_pending = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                miss_pending <= 0;
 
        else if (!i_wbm_cyc)
 
                miss_pending <= 0;
 
        else
 
                miss_pending <= (i_wbm_cyc)&&(
 
                                (simple_miss)||(ro_miss)||(exe_miss)
 
                                ||((s_pending)&&(!s_tlb_miss)&&(!s_tlb_hit)));
 
 
 
        assign  o_rtn_miss  = (miss_pending)&&(!bus_pending);
 
        assign  o_rtn_err   = (rtn_err);
 
 
 
        assign  o_sel  = r_sel;
        assign  o_data = r_data;
        assign  o_data = r_data;
 
 
        //
        //
 
        assign  o_wbs_stall = 1'b0;
 
        initial o_wbs_ack = 1'b0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                o_wbs_ack <= 1'b0;
 
        else
 
                o_wbs_ack <= (i_wbs_cyc_stb);
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                o_wbs_data <= 0;
 
        else case({i_wbs_addr[LGTBL+1],i_wbs_addr[0]})
 
        2'b00: o_wbs_data <= w_control_data;
 
        2'b01: o_wbs_data <= status_word;
 
        2'b10: o_wbs_data <= w_vtable_reg;
 
        2'b11: o_wbs_data <= w_ptable_reg;
 
        endcase
 
 
 
        //
        // Bus snooping returns ...
        // Bus snooping returns ...
        //
        //
        assign  pf_return_stb = pf_stb;
        assign  pf_return_stb = pf_stb;
        assign  pf_return_we = r_we;
        assign  pf_return_we = r_we;
        assign  pf_return_p  = last_ppage;
        assign  pf_return_p  = last_ppage;
        assign  pf_return_v  = last_vpage;
        assign  pf_return_v  = last_vpage;
        assign  pf_return_cachable = pf_cachable;
        assign  pf_return_cachable = pf_cachable;
 
 
 
        // Also requires being told when/if the page changed
 
        // So, on a page change,
 
        // pf_return_we = 1
 
        // pf_stb = 1
 
        // and pf_return_p has the physical address
 
 
 
        // Make verilator happy
 
        // verilator lint_off UNUSED
 
        wire [(PAW-1):0] unused;
 
        assign  unused = r_ppage;
 
        generate if (4+LGCTXT < LGPGSZB)
 
        begin
 
                wire    [LGPGSZB-(4+LGCTXT)-1:0] unused_data;
 
                assign  unused_data = i_wbs_data[LGPGSZB-1:4+LGCTXT];
 
        end endgenerate
 
 
 
        wire    unused_always;
 
        assign  unused_always = s_tlb_flags[0];
 
        // verilator lint_on  UNUSED
 
 
 
`ifdef  FORMAL
 
        initial f_past_valid = 0;
 
        always @(posedge i_clk)
 
                f_past_valid <= 1'b1;
 
 
 
        initial assume(i_reset);
 
        always @(*)
 
                if (!f_past_valid)
 
                        assume(i_reset);
 
 
 
        always @(*)
 
                if (i_reset)
 
                        assume(!i_wbs_cyc_stb);
 
        always @(posedge i_clk)
 
        if (f_past_valid)
 
                assert(o_wbs_ack == $past(i_wbs_cyc_stb));
 
        always @(*)
 
                assert(o_wbs_stall == 1'b0);
 
 
 
        always @(*)
 
                assume((!i_wbm_cyc)||(!i_wbs_cyc_stb));
 
 
 
        localparam      F_LGDEPTH = 6;
 
        reg     [F_LGDEPTH-1:0]  fv_nreqs, fv_nacks, fv_outstanding,
 
                        fp_nreqs, fp_nacks, fp_outstanding;
 
 
 
        localparam      F_MAX_STALL = 3,
 
                        F_MAX_WAIT  = 2,
 
                        F_MAX_REQ   = 9;
 
 
 
        //
 
        // The stall period needs to be long enough to allow all in-progress
 
        // transactions to complete, as in the case of a page miss.  Hence,
 
        // the max stall amount depends upon the max wait time for the
 
        // physical half of the interaction.  It is artificially limited here
 
        // in order to limit the amount of proof time required.
 
        //
 
        fwb_slave #(.F_MAX_STALL(F_MAX_STALL+(F_MAX_WAIT*F_MAX_REQ)+2),
 
                        .AW(DW-2),
 
                        .F_MAX_ACK_DELAY(F_MAX_STALL+F_MAX_WAIT+5),
 
                        .F_MAX_REQUESTS(F_MAX_REQ),
 
                        .F_LGDEPTH(F_LGDEPTH),
 
                        .F_OPT_MINCLOCK_DELAY(0))
 
                busslave(i_clk, i_reset,
 
                                i_wbm_cyc, i_wbm_stb, i_wbm_we, i_wbm_addr,
 
                                        i_wbm_data, i_wbm_sel,
 
                                o_rtn_ack, o_rtn_stall, o_rtn_data,
 
                                        o_rtn_err|o_rtn_miss,
 
                                fv_nreqs, fv_nacks, fv_outstanding);
 
 
 
        fwb_master #(.F_MAX_STALL(F_MAX_STALL),
 
                        .AW(ADDRESS_WIDTH),
 
                        .F_MAX_ACK_DELAY(F_MAX_WAIT),
 
                        .F_MAX_REQUESTS(F_MAX_REQ),
 
                        .F_LGDEPTH(F_LGDEPTH),
 
                        .F_OPT_MINCLOCK_DELAY(0))
 
                busmaster(i_clk, i_reset,
 
                                o_cyc, o_stb, o_we, o_addr,
 
                                        o_data, o_sel,
 
                                i_ack, i_stall, i_data, i_err,
 
                                fp_nreqs, fp_nacks, fp_outstanding);
 
 
 
        always @(*)
 
                assert((!o_cyc)||(fp_outstanding == bus_outstanding));
 
 
 
        always @(*)
 
                assume(fv_nreqs < F_MAX_REQ);
 
        always @(*)
 
        if ((i_wbm_cyc)&&(o_cyc)&&(fv_outstanding == fp_outstanding))
 
                assert(fv_nreqs == fp_nreqs);
 
        always @(*)
 
        if ((i_wbm_cyc)&&(o_cyc))
 
        begin
 
                assert(fp_nreqs <= fv_nreqs);
 
                assert(fp_nacks >= fv_nacks);
 
        end
 
 
 
        reg     [F_LGDEPTH-1:0]  f_expected, f_ex_nreqs, f_ex_nacks;
 
        always @(*)
 
        if (!i_wbm_cyc)
 
        begin
 
                f_ex_nreqs <= 0;
 
                f_ex_nacks <= 0;
 
                f_expected <= 0;
 
        end else if (OPT_DELAY_RETURN)
 
        begin
 
                if (r_pending)
 
                begin
 
                        f_ex_nreqs <= fp_nreqs + 1'b1;
 
                        f_ex_nacks <= fp_nacks + o_rtn_ack;
 
                        f_expected <= fp_outstanding + 1'b1
 
                                                + o_rtn_ack;
 
                end else begin
 
                        f_expected <= fp_outstanding + (o_stb)
 
                                + (o_rtn_ack);
 
                        f_ex_nreqs <= fp_nreqs + o_stb;
 
                        f_ex_nacks <= fp_nacks + o_rtn_ack;
 
                end
 
        end else begin
 
                if (r_pending)
 
                begin
 
                        f_ex_nreqs <= fp_nreqs + 1'b1;
 
                        f_ex_nacks <= fp_nacks;
 
                        f_expected <= fp_outstanding + 1'b1;
 
                end else begin
 
                        f_ex_nreqs <= fp_nreqs + o_stb;
 
                        f_ex_nacks <= fp_nacks;
 
                        f_expected <= fp_outstanding + (o_stb);
 
                end
 
        end
 
 
 
        reg     f_kill_input;
 
        initial f_kill_input = 1'b0;
 
        always @(posedge i_clk)
 
                f_kill_input <= (i_wbm_cyc)&&(
 
                        (i_reset)
 
                        ||(o_rtn_miss)
 
                        ||(o_rtn_err));
 
        always @(*)
 
                if (f_kill_input)
 
                        assume(!i_wbm_cyc);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_rtn_miss))&&($past(i_wbm_cyc)))
 
        begin
 
                assume(!o_cyc);
 
                assume(!i_wbm_cyc);
 
        end
 
 
 
        wire    fv_is_one, fp_is_zero;
 
        assign  fv_is_one  = (fv_outstanding == 1);
 
        assign  fp_is_zero = (fp_outstanding == 0);
 
        always @(*)
 
        if ((i_wbm_cyc)&&(o_cyc))
 
        begin
 
                if (o_rtn_miss)
 
                begin
 
                        assert(fp_outstanding == 0);
 
                        assert(fv_outstanding == 1);
 
                        assert(fv_is_one);
 
                        assert(fp_is_zero);
 
                end else begin
 
                        assert(fv_nreqs == f_ex_nreqs);
 
                        assert(fv_nacks == f_ex_nacks);
 
                        assert(fv_outstanding >= fp_outstanding);
 
                        assert(fv_outstanding == f_expected);
 
                end
 
        end
 
 
 
        always @(*)
 
                assert(z_context == (r_context_word == 0));
 
        always @(*)
 
                assert(kernel_context == ( ((r_context_word == 0)||(!i_gie)) ? 1'b1 : 1'b0));
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_wbs_cyc_stb)))
 
                assume(!i_wbm_cyc);
 
        always @(*)
 
        if (o_wbs_ack)
 
                assume(!i_wbm_cyc);
 
 
 
        always @(*)
 
                assert((!i_wbm_cyc)||(!o_wbs_ack));
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(r_pending)&&($past(kernel_context))
 
                        &&($past(i_wbm_stb))&&(!$past(i_stall))&&(i_wbm_cyc)
 
                        &&(!o_rtn_stall))
 
                assert(o_addr[(AW-1):0] == $past(i_wbm_addr[(AW-1):0]));
 
        always @(*)
 
                assert(bus_pending == (bus_outstanding > 0));
 
 
 
        always @(*)
 
        if ((s_pending)&&(!s_tlb_miss))
 
                assert(r_tlb_match[s_tlb_addr]);
 
 
 
        // Check out all of the criteria which should clear these flags
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(($past(i_reset))
 
                        ||(!$past(i_wbm_cyc))
 
                        ||(!$past(o_rtn_stall))))
 
        begin
 
                assert(!simple_miss);
 
                assert(!ro_miss);
 
                assert(!exe_miss);
 
                assert(!table_err);
 
                if (!$past(i_wbm_we))
 
                        assert(!ro_miss);
 
 
 
                if (!kernel_context)
 
                begin
 
                        assert((!o_stb)||(!(simple_miss|ro_miss|table_err)));
 
                        // This doesn't belong on the clear list, but on the
 
                        // should be set list
 
                        // assert((!o_stb)||(!s_tlb_hit));
 
                end
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wbm_cyc))
 
                        &&(!$past(o_rtn_stall)))
 
        begin
 
                if ((!$past(kernel_context))&&(o_stb))
 
                        assert((last_page_valid)||(s_tlb_hit));
 
        end
 
 
 
        reg     [(LGTBL-1):0]            f_last_page;
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!kernel_context)&&(r_pending)&&(!last_page_valid))
 
                f_last_page <= s_tlb_addr;
 
 
 
        wire    [3:0]    tlb_flag_last_page;
 
        assign  tlb_flag_last_page = tlb_flags[f_last_page];
 
        always @(*)
 
        if (last_page_valid)
 
        begin
 
                assert(tlb_valid[f_last_page]);
 
                assert(last_tlb   == f_last_page);
 
                assert(last_ppage == tlb_pdata[f_last_page]);
 
                assert(last_vpage == tlb_vdata[f_last_page]);
 
                assert(last_ro    == tlb_flag_last_page[`ROFLAG]);
 
                assert(last_exe   == tlb_flag_last_page[`EXEFLG]);
 
                assert(r_context_word[LGCTXT-1:1] == tlb_cdata[f_last_page][LGCTXT-1:1]);
 
                if (!r_context_word[0])
 
                        assert(!tlb_cdata[f_last_page][0]);
 
                assert((!r_context_word[0])||(r_context_word[0]));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                        &&($past(last_page_valid))&&(!$past(kernel_context))
 
                        &&($past(o_stb))&&($past(i_wbm_cyc)))
 
                assert(tlb_accessed[$past(last_tlb)]);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                        &&($past(pending_page_valid))&&(!$past(kernel_context))
 
                        &&($past(o_stb))&&($past(i_wbm_cyc)))
 
                assert(tlb_accessed[$past(s_tlb_addr)]);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(kernel_context))&&(o_stb))
 
        begin
 
                assert(last_page_valid);
 
                assert(r_ppage == last_ppage);
 
                assert((!last_ro)||(!o_we));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_stb))&&(o_stb)&&(i_wbm_cyc))
 
                assert((last_page_valid)||(kernel_context));
 
 
 
        always @(*)
 
                assert((!s_tlb_hit)||(!s_tlb_miss));
 
        // always @(*)
 
        // if ((fp_outstanding > 0)&&(o_cyc)&&(!o_stb)&&(!r_pending)&&(!kernel_context))
 
                // assert(last_page_valid);
 
        // always @(*) assume(kernel_context);
 
        always @(*)
 
                assume((!i_wbs_cyc_stb)||(!i_gie));
 
 
 
        reg     f_past_gie, f_past_wbm_cyc;
 
 
 
        initial f_past_gie = 1'b0;
 
        always @(posedge i_clk)
 
                f_past_gie <= i_gie;
 
 
 
        initial f_past_wbm_cyc = 1'b0;
 
        always @(posedge i_clk)
 
                f_past_wbm_cyc <= i_wbm_cyc;
 
        always @(*)
 
        if ((f_past_valid)&&(bus_pending))
 
                assume(i_gie == f_past_gie);
 
        always @(*)
 
        if ((f_past_wbm_cyc)&&(i_wbm_cyc))
 
                assume(i_gie == f_past_gie);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(i_wbm_cyc)&&($past(i_wbm_cyc)))
 
                assume(i_gie == $past(i_gie));
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_reset)))
 
                assume(!i_gie);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wbm_cyc))
 
                        &&($past(!kernel_context))
 
                        &&($past(r_pending))
 
                        &&(!$past(last_page_valid)))
 
        begin
 
                if (($past(s_tlb_hit))
 
                                &&(!$past(ro_miss))
 
                                &&(!$past(exe_miss)))
 
                begin
 
                        assert(last_vpage == $past(r_vpage));
 
                        assert(last_page_valid);
 
                        assert(!miss_pending);
 
                        assert(tlb_accessed[s_tlb_addr]);
 
                end else if (($past(s_tlb_hit))&&($past(ro_miss)))
 
                begin
 
                        assert(miss_pending);
 
                        assert(last_page_valid);
 
                        assert(status_word[3:0] == 4'h2);
 
                end else if (($past(s_tlb_hit))&&($past(exe_miss)))
 
                begin
 
                        assert(miss_pending);
 
                        assert(last_page_valid);
 
                        assert(status_word[3:0] == 4'h4);
 
                end else if (($past(s_tlb_hit))&&($past(simple_miss)))
 
                begin
 
                        assert(miss_pending);
 
                        assert(last_page_valid);
 
                        assert(status_word[3:0] == 4'h1);
 
                end else if (!$past(s_tlb_hit))
 
                begin
 
                        assert(!last_page_valid);
 
                end
 
        end
 
 
 
        always @(*)
 
                assert((!ro_miss)||(!exe_miss)||(!simple_miss)||(!table_err));
 
 
 
        reg     [4:0]    f_tlb_pipe;
 
 
 
        initial f_tlb_pipe = 5'h0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                f_tlb_pipe <= 5'h0;
 
        else if ((!r_pending)||(o_stb))
 
                f_tlb_pipe <= 5'h0;
 
        else if ((r_pending)&&(!r_valid)&&(!miss_pending))
 
                f_tlb_pipe <= { f_tlb_pipe[3:0], 1'b1 };
 
 
 
        always @(*)
 
                assert(f_tlb_pipe != 5'h1f);
 
 
 
        always @(*) // WE or EXE, never both
 
        assume((!i_wbm_stb)||(!i_wbm_we)||(!i_wbm_exe));
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_wbm_stb))&&($past(o_rtn_stall)))
 
                assume(i_wbm_exe == $past(i_wbm_exe));
 
 
 
        always @(*)
 
                assert((!r_pending)||(!o_stb));
 
        always @(*)
 
                assert((!s_pending)||(!o_stb));
 
        always @(*)
 
                assert((!s_pending)||(r_pending));
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_wbm_cyc)))
 
                assume(!i_wbs_cyc_stb);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(|status_word[3:0])&&(!$past(i_wbm_cyc)))
 
                assume(!i_gie);
 
`endif
endmodule
endmodule
 
 
 No newline at end of file
 No newline at end of file

powered by: WebSVN 2.1.0

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