| 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
|
