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

Subversion Repositories zipcpu

Compare Revisions

  • This comparison shows the changes necessary to convert path
    /zipcpu/trunk/rtl/peripherals
    from Rev 201 to Rev 209
    Reverse comparison

Rev 201 → Rev 209

/README.md
0,0 → 1,26
# ZipCPU Peripherals
 
These are not your normal peripherals, per se, but rather peripherals that
get tightly integrated with the CPU when built with the ZipSystem. These
include:
 
- [icontrol.v](./icontrol.v), an interrupt controller
 
- [zipcounter.v](./zipcounter.v), a *really* simple counter, for estimating CPU performance. The counter will interrupt the CPU if/when it ever rolls over.
 
- [ziptimer.v](./ziptimer.v), a similarly simple timer. It just counts down and creates an interrupt
 
- [zipjiffies.v](./zipjiffies.v). Modeled after the Jiffies used within the Linux Kernel, the zipjiffies peripheral counts up one count per clock. Numbers written to it request an interrupt when the clock gets to the number written. Hence, you can get really fine grained timing control using this peripheral.
 
- [wbdmac.v](./wbdmac.v), a direct memory access controller. This can be used to copy memory, or even copy memory on an interrupt. Source and destination addresses may or may not increment depending upon how the controller is set. As of today, though, this controller only handles 32-bit transfers.
 
- [zipmmu.v](./zipmmu.v), an experimental MMU. Has only been tested offline.
An implementation exists which integrates this MMU, however that integration
has not been tested so there are certainly some integration bugs remaining.
 
*All of these peripherals* have been formally proven.
If you are looking for the more normal peripherals, block RAM, SDRAM, etc.,
feel free to examine some of the distributions that use the ZipCPU.
 
 
/icontrol.v
52,7 → 52,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015,2017, Gisselquist Technology, LLC
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
76,20 → 76,23
////////////////////////////////////////////////////////////////////////////////
//
//
module icontrol(i_clk, i_reset, i_wr, i_proc_bus, o_proc_bus,
`default_nettype none
//
module icontrol(i_clk, i_reset, i_wr, i_data, o_data,
i_brd_ints, o_interrupt);
parameter IUSED = 15;
input i_clk, i_reset;
input i_wr;
input [31:0] i_proc_bus;
output wire [31:0] o_proc_bus;
input [(IUSED-1):0] i_brd_ints;
parameter IUSED = 15, BW=32;
input wire i_clk, i_reset;
input wire i_wr;
input wire [BW-1:0] i_data;
output reg [BW-1:0] o_data;
input wire [(IUSED-1):0] i_brd_ints;
output wire o_interrupt;
 
reg [(IUSED-1):0] r_int_state;
reg [(IUSED-1):0] r_int_enable;
wire [(IUSED-1):0] nxt_int_state;
reg r_any, r_interrupt, r_gie;
reg r_interrupt, r_gie;
wire w_any;
 
assign nxt_int_state = (r_int_state|i_brd_ints);
initial r_int_state = 0;
97,7 → 100,7
if (i_reset)
r_int_state <= 0;
else if (i_wr)
r_int_state <= nxt_int_state & (~i_proc_bus[(IUSED-1):0]);
r_int_state <= i_brd_ints | (r_int_state & (~i_data[(IUSED-1):0]));
else
r_int_state <= nxt_int_state;
initial r_int_enable = 0;
104,10 → 107,10
always @(posedge i_clk)
if (i_reset)
r_int_enable <= 0;
else if ((i_wr)&&(i_proc_bus[31]))
r_int_enable <= r_int_enable | i_proc_bus[(16+IUSED-1):16];
else if ((i_wr)&&(~i_proc_bus[31]))
r_int_enable <= r_int_enable & (~ i_proc_bus[(16+IUSED-1):16]);
else if ((i_wr)&&(i_data[BW-1]))
r_int_enable <= r_int_enable | i_data[(16+IUSED-1):16];
else if ((i_wr)&&(!i_data[BW-1]))
r_int_enable <= r_int_enable & (~ i_data[(16+IUSED-1):16]);
 
initial r_gie = 1'b0;
always @(posedge i_clk)
114,46 → 117,98
if (i_reset)
r_gie <= 1'b0;
else if (i_wr)
r_gie <= i_proc_bus[31];
r_gie <= i_data[BW-1];
 
initial r_any = 1'b0;
always @(posedge i_clk)
r_any <= ((r_int_state & r_int_enable) != 0);
assign w_any = ((r_int_state & r_int_enable) != 0);
 
initial r_interrupt = 1'b0;
always @(posedge i_clk)
r_interrupt <= r_gie & r_any;
if (i_reset)
r_interrupt <= 1'b0;
else
r_interrupt <= (r_gie)&&(w_any);
 
generate
if (IUSED < 15)
begin
assign o_proc_bus = {
always @(posedge i_clk)
o_data <= {
r_gie, { {(15-IUSED){1'b0}}, r_int_enable },
r_any, { {(15-IUSED){1'b0}}, r_int_state } };
w_any, { {(15-IUSED){1'b0}}, r_int_state } };
end else begin
assign o_proc_bus = { r_gie, r_int_enable, r_any, r_int_state };
always @(posedge i_clk)
o_data <= { r_gie, r_int_enable, w_any, r_int_state };
end endgenerate
 
/*
reg int_condition;
initial int_condition = 1'b0;
initial o_interrupt_strobe = 1'b0;
assign o_interrupt = r_interrupt;
 
// Make verilator happy
// verilator lint_off UNUSED
wire [30:0] unused;
assign unused = i_data[30:0];
// verilator lint_on UNUSED
 
`ifdef FORMAL
`ifdef ICONTROL
`define ASSUME assume
`else
`define ASSUME assert
`endif
 
reg f_past_valid;
 
initial f_past_valid = 1'b0;
always @(posedge i_clk)
if (i_reset)
begin
int_condition <= 1'b0;
o_interrupt_strobe <= 1'b0;
end else if (~r_interrupt) // This might end up generating
begin // many, many, (wild many) interrupts
int_condition <= 1'b0;
o_interrupt_strobe <= 1'b0;
end else if ((~int_condition)&&(r_interrupt))
begin
int_condition <= 1'b1;
o_interrupt_strobe <= 1'b1;
end else
o_interrupt_strobe <= 1'b0;
*/
f_past_valid <= 1'b1;
 
assign o_interrupt = r_interrupt;
initial `ASSUME(i_reset);
always @(*)
if (!f_past_valid)
`ASSUME(i_reset);
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
begin
assert(w_any == 0);
assert(r_interrupt == 0);
assert(r_gie == 0);
assert(r_int_enable == 0);
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset)))
assert((r_int_state & $past(i_brd_ints))==$past(i_brd_ints));
 
always @(posedge i_clk)
if (((f_past_valid)&&(!$past(i_reset)))
&&($past(r_int_state) & $past(r_int_enable))
&&($past(r_gie)) )
assert(o_interrupt);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(w_any))&&(!$past(i_wr))&&(!$past(i_reset)))
assert(w_any);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(r_gie)))
assert(!o_interrupt);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(w_any)))
assert(!o_interrupt);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr)))
begin
// Interrupts cannot be cleared, unless they are set
assert(r_int_state == (($past(i_brd_ints))
|(($past(r_int_state))&(~$past(i_data[IUSED-1:0])))));
assert(r_gie == $past(i_data[BW-1]));
end else if ((f_past_valid)&&(!$past(i_reset)))
begin
assert(r_int_state == ($past(r_int_state)|$past(i_brd_ints)));
assert(r_gie == $past(r_gie));
end
 
`endif
endmodule
/wbdmac.v
56,7 → 56,11
// The minimum transfer length is one, while zero
// is mapped to a transfer length of 1kW.
//
// Write 32'hffed00 to halt an ongoing transaction, completing anything
// remaining, or 32'hafed00 to abort the current transaction leaving
// any unfinished read/write in an undetermined state.
//
//
// To use this, follow this checklist:
// 1. Wait for any prior DMA operation to complete
// (Read address 0, wait 'till either top bit is set or cfg_len==0)
82,7 → 86,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
114,7 → 118,7
`define DMA_WRITE_REQ 3'b101
`define DMA_WRITE_ACK 3'b110
 
module wbdmac(i_clk, i_rst,
module wbdmac(i_clk, i_reset,
i_swb_cyc, i_swb_stb, i_swb_we, i_swb_addr, i_swb_data,
o_swb_ack, o_swb_stall, o_swb_data,
o_mwb_cyc, o_mwb_stb, o_mwb_we, o_mwb_addr, o_mwb_data,
121,13 → 125,14
i_mwb_ack, i_mwb_stall, i_mwb_data, i_mwb_err,
i_dev_ints,
o_interrupt);
parameter ADDRESS_WIDTH=32, LGMEMLEN = 10,
DW=32, LGDV=5,AW=ADDRESS_WIDTH;
input i_clk, i_rst;
parameter ADDRESS_WIDTH=30, LGMEMLEN = 10, DW=32;
localparam LGDV=5;
localparam AW=ADDRESS_WIDTH;
input wire i_clk, i_reset;
// Slave/control wishbone inputs
input i_swb_cyc, i_swb_stb, i_swb_we;
input [1:0] i_swb_addr;
input [(DW-1):0] i_swb_data;
input wire i_swb_cyc, i_swb_stb, i_swb_we;
input wire [1:0] i_swb_addr;
input wire [(DW-1):0] i_swb_data;
// Slave/control wishbone outputs
output reg o_swb_ack;
output wire o_swb_stall;
137,11 → 142,11
output reg [(AW-1):0] o_mwb_addr;
output reg [(DW-1):0] o_mwb_data;
// Master/DMA wishbone responses from the bus
input i_mwb_ack, i_mwb_stall;
input [(DW-1):0] i_mwb_data;
input i_mwb_err;
input wire i_mwb_ack, i_mwb_stall;
input wire [(DW-1):0] i_mwb_data;
input wire i_mwb_err;
// The interrupt device interrupt lines
input [(DW-1):0] i_dev_ints;
input wire [(DW-1):0] i_dev_ints;
// An interrupt to be set upon completion
output reg o_interrupt;
// Need to release the bus for a higher priority user
153,7 → 158,42
// input i_other_busmaster_requests_bus;
//
 
wire s_cyc, s_stb, s_we;
wire [1:0] s_addr;
wire [31:0] s_data;
`define DELAY_ACCESS
`ifdef DELAY_ACCESS
reg r_s_cyc, r_s_stb, r_s_we;
reg [1:0] r_s_addr;
reg [31:0] r_s_data;
 
always @(posedge i_clk)
r_s_cyc <= i_swb_cyc;
always @(posedge i_clk)
if (i_reset)
r_s_stb <= 1'b0;
else
r_s_stb <= i_swb_stb;
always @(posedge i_clk)
r_s_we <= i_swb_we;
always @(posedge i_clk)
r_s_addr<= i_swb_addr;
always @(posedge i_clk)
r_s_data<= i_swb_data;
 
assign s_cyc = r_s_cyc;
assign s_stb = r_s_stb;
assign s_we = r_s_we;
assign s_addr= r_s_addr;
assign s_data= r_s_data;
`else
assign s_cyc = i_swb_cyc;
assign s_stb = i_swb_stb;
assign s_we = i_swb_we;
assign s_addr= i_swb_addr;
assign s_data= i_swb_data;
`endif
 
reg [2:0] dma_state;
reg cfg_err, cfg_len_nonzero;
reg [(AW-1):0] cfg_waddr, cfg_raddr, cfg_len;
176,53 → 216,46
 
initial dma_state = `DMA_IDLE;
initial o_interrupt = 1'b0;
initial cfg_len = {(AW){1'b0}};
initial cfg_blocklen_sub_one = {(LGMEMLEN){1'b1}};
initial cfg_on_dev_trigger = 1'b0;
initial cfg_len_nonzero = 1'b0;
always @(posedge i_clk)
case(dma_state)
if (i_reset)
begin
dma_state <= `DMA_IDLE;
cfg_on_dev_trigger <= 1'b0;
cfg_incs <= 1'b0;
cfg_incd <= 1'b0;
end else case(dma_state)
`DMA_IDLE: begin
o_mwb_addr <= cfg_raddr;
nwritten <= 0;
nread <= 0;
nracks <= 0;
nwacks <= 0;
cfg_len_nonzero <= (|cfg_len);
 
// When the slave wishbone writes, and we are in this
// (ready) configuration, then allow the DMA to be controlled
// and thus to start.
if ((i_swb_stb)&&(i_swb_we))
if ((s_stb)&&(s_we))
begin
case(i_swb_addr)
case(s_addr)
2'b00: begin
if ((i_swb_data[31:16] == 16'h0fed)
if ((s_data[27:16] == 12'hfed)
&&(s_data[31:30] == 2'b00)
&&(cfg_len_nonzero))
dma_state <= `DMA_WAIT;
cfg_blocklen_sub_one
<= i_swb_data[(LGMEMLEN-1):0]
<= s_data[(LGMEMLEN-1):0]
+ {(LGMEMLEN){1'b1}};
// i.e. -1;
cfg_dev_trigger <= i_swb_data[14:10];
cfg_on_dev_trigger <= i_swb_data[15];
cfg_incs <= ~i_swb_data[29];
cfg_incd <= ~i_swb_data[28];
cfg_dev_trigger <= s_data[14:10];
cfg_on_dev_trigger <= s_data[15];
cfg_incs <= !s_data[29];
cfg_incd <= !s_data[28];
end
2'b01: begin
cfg_len <= i_swb_data[(AW-1):0];
cfg_len_nonzero <= (|i_swb_data[(AW-1):0]);
end
2'b10: cfg_raddr <= i_swb_data[(AW-1):0];
2'b11: cfg_waddr <= i_swb_data[(AW-1):0];
2'b01: begin end // This is done elsewhere
2'b10: cfg_raddr <= s_data[(AW+2-1):2];
2'b11: cfg_waddr <= s_data[(AW+2-1):2];
endcase
end end
`DMA_WAIT: begin
o_mwb_addr <= cfg_raddr;
nracks <= 0;
nwacks <= 0;
nwritten <= 0;
nread <= 0;
if (abort)
dma_state <= `DMA_IDLE;
else if (user_halt)
231,13 → 264,10
dma_state <= `DMA_READ_REQ;
end
`DMA_READ_REQ: begin
nwritten <= 0;
 
if (~i_mwb_stall)
if (!i_mwb_stall)
begin
// Number of read acknowledgements needed
nracks <= nracks+1;
if (last_read_request)
if ((last_read_request)||(user_halt))
//((nracks == {1'b0, cfg_blocklen_sub_one})||(bus_nracks == cfg_len-1))
// Wishbone interruptus
dma_state <= `DMA_READ_ACK;
246,33 → 276,21
+ {{(AW-1){1'b0}},1'b1};
end
 
if (user_halt)
dma_state <= `DMA_READ_ACK;
if (i_mwb_err)
begin
cfg_len <= 0;
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
end
 
if (abort)
dma_state <= `DMA_IDLE;
if (i_mwb_ack)
else if (i_mwb_ack)
begin
nread <= nread+1;
if (cfg_incs)
cfg_raddr <= cfg_raddr
+ {{(AW-1){1'b0}},1'b1};
if (last_read_ack)
dma_state <= `DMA_PRE_WRITE;
end end
`DMA_READ_ACK: begin
nwritten <= 0;
 
if (i_mwb_err)
begin
cfg_len <= 0;
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
end else if (i_mwb_ack)
else if (i_mwb_ack)
begin
nread <= nread+1;
if (last_read_ack) // (nread+1 == nracks)
dma_state <= `DMA_PRE_WRITE;
if (user_halt)
281,8 → 299,6
cfg_raddr <= cfg_raddr
+ {{(AW-1){1'b0}},1'b1};
end
if (abort)
dma_state <= `DMA_IDLE;
end
`DMA_PRE_WRITE: begin
o_mwb_addr <= cfg_waddr;
289,9 → 305,8
dma_state <= (abort)?`DMA_IDLE:`DMA_WRITE_REQ;
end
`DMA_WRITE_REQ: begin
if (~i_mwb_stall)
if (!i_mwb_stall)
begin
nwritten <= nwritten+1;
if (last_write_request) // (nwritten == nread-1)
// Wishbone interruptus
dma_state <= `DMA_WRITE_ACK;
304,39 → 319,20
end
end
 
if (i_mwb_err)
begin
cfg_len <= 0;
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
end
if (i_mwb_ack)
begin
nwacks <= nwacks+1;
cfg_len <= cfg_len +{(AW){1'b1}}; // -1
end
if (user_halt)
dma_state <= `DMA_WRITE_ACK;
if (abort)
else if ((i_mwb_ack)&&(last_write_ack))
dma_state <= (cfg_len <= 1)?`DMA_IDLE:`DMA_WAIT;
else if (!cfg_len_nonzero)
dma_state <= `DMA_IDLE;
end
`DMA_WRITE_ACK: begin
if (i_mwb_err)
begin
cfg_len <= 0;
nread <= 0;
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
end else if (i_mwb_ack)
begin
nwacks <= nwacks+1;
cfg_len <= cfg_len +{(AW){1'b1}};//cfg_len -= 1;
if (last_write_ack) // (nwacks+1 == nwritten)
begin
nread <= 0;
dma_state <= (cfg_len == 1)?`DMA_IDLE:`DMA_WAIT;
end
end
 
if (abort)
else if ((i_mwb_ack)&&(last_write_ack))
// (nwacks+1 == nwritten)
dma_state <= (cfg_len <= 1)?`DMA_IDLE:`DMA_WAIT;
else if (!cfg_len_nonzero)
dma_state <= `DMA_IDLE;
end
default:
345,71 → 341,150
 
initial o_interrupt = 1'b0;
always @(posedge i_clk)
if (i_reset)
o_interrupt <= 1'b0;
else
o_interrupt <= ((dma_state == `DMA_WRITE_ACK)&&(i_mwb_ack)
&&(last_write_ack)
&&(cfg_len == {{(AW-1){1'b0}},1'b1}))
||((dma_state != `DMA_IDLE)&&(i_mwb_err));
 
 
initial cfg_len = 0;
initial cfg_len_nonzero = 1'b0;
always @(posedge i_clk)
if (i_reset)
begin
cfg_len <= 0;
cfg_len_nonzero <= 1'b0;
end else if ((dma_state == `DMA_IDLE)
&&(s_stb)&&(s_we)&&(s_addr == 2'b01))
begin
cfg_len <= s_data[(AW-1):0];
cfg_len_nonzero <= (|s_data[(AW-1):0]);
end else if ((o_mwb_cyc)&&(o_mwb_we)&&(i_mwb_ack))
begin
cfg_len <= cfg_len - 1'b1;
cfg_len_nonzero <= (cfg_len > 1);
end
 
initial nracks = 0;
always @(posedge i_clk)
if (i_reset)
nracks <= 0;
else if ((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT))
nracks <= 0;
else if ((o_mwb_stb)&&(!o_mwb_we)&&(!i_mwb_stall))
nracks <= nracks + 1'b1;
 
initial nread = 0;
always @(posedge i_clk)
if (i_reset)
nread <= 0;
else if ((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT))
nread <= 0;
else if ((!o_mwb_we)&&(i_mwb_ack))
nread <= nread + 1'b1;
 
initial nwritten = 0;
always @(posedge i_clk)
if (i_reset)
nwritten <= 0;
else if ((!o_mwb_cyc)||(!o_mwb_we))
nwritten <= 0;
else if ((o_mwb_stb)&&(!i_mwb_stall))
nwritten <= nwritten + 1'b1;
 
initial nwacks = 0;
always @(posedge i_clk)
if (i_reset)
nwacks <= 0;
else if ((!o_mwb_cyc)||(!o_mwb_we))
nwacks <= 0;
else if (i_mwb_ack)
nwacks <= nwacks + 1'b1;
 
initial cfg_err = 1'b0;
always @(posedge i_clk)
if (dma_state == `DMA_IDLE)
begin
if ((i_swb_stb)&&(i_swb_we)&&(i_swb_addr==2'b00))
cfg_err <= 1'b0;
end else if (((i_mwb_err)&&(o_mwb_cyc))||(abort))
cfg_err <= 1'b1;
if (i_reset)
cfg_err <= 1'b0;
else if (dma_state == `DMA_IDLE)
begin
if ((s_stb)&&(s_we)&&(s_addr==2'b00))
cfg_err <= 1'b0;
end else if (((i_mwb_err)&&(o_mwb_cyc))||(abort))
cfg_err <= 1'b1;
 
initial last_read_request = 1'b0;
always @(posedge i_clk)
if ((dma_state == `DMA_WAIT)||(dma_state == `DMA_READ_REQ))
if (i_reset)
last_read_request <= 1'b0;
else if ((dma_state == `DMA_WAIT)||(dma_state == `DMA_READ_REQ))
begin
if ((!i_mwb_stall)&&(dma_state == `DMA_READ_REQ))
begin
if ((~i_mwb_stall)&&(dma_state == `DMA_READ_REQ))
begin
last_read_request <=
(nracks + 1 == { 1'b0, cfg_blocklen_sub_one})
||(bus_nracks == cfg_len-2);
end else
last_read_request <=
(nracks== { 1'b0, cfg_blocklen_sub_one})
||(bus_nracks == cfg_len-1);
last_read_request <=
(nracks + 1 == { 1'b0, cfg_blocklen_sub_one})
||(bus_nracks == cfg_len-2);
end else
last_read_request <= 1'b0;
last_read_request <=
(nracks== { 1'b0, cfg_blocklen_sub_one})
||(bus_nracks == cfg_len-1);
end else
last_read_request <= 1'b0;
 
 
wire [(LGMEMLEN):0] next_nread;
assign next_nread = nread + 1'b1;
 
initial last_read_ack = 1'b0;
always @(posedge i_clk)
if ((dma_state == `DMA_READ_REQ)||(dma_state == `DMA_READ_ACK))
begin
if ((i_mwb_ack)&&((~o_mwb_stb)||(i_mwb_stall)))
last_read_ack <= (nread+2 == nracks);
else
last_read_ack <= (nread+1 == nracks);
end else
last_read_ack <= 1'b0;
if (i_reset)
last_read_ack <= 0;
else if (dma_state == `DMA_READ_REQ)
begin
if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
last_read_ack <= (next_nread == { 1'b0, cfg_blocklen_sub_one });
else
last_read_ack <= (nread == { 1'b0, cfg_blocklen_sub_one });
end else if (dma_state == `DMA_READ_ACK)
begin
if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
last_read_ack <= (nread+2 == nracks);
else
last_read_ack <= (next_nread == nracks);
end else
last_read_ack <= 1'b0;
 
initial last_write_request = 1'b0;
always @(posedge i_clk)
if (dma_state == `DMA_PRE_WRITE)
last_write_request <= (nread <= 1);
else if (dma_state == `DMA_WRITE_REQ)
begin
if (i_mwb_stall)
last_write_request <= (nwritten >= nread-1);
else
last_write_request <= (nwritten >= nread-2);
end else
last_write_request <= 1'b0;
if (i_reset)
last_write_request <= 1'b0;
else if (dma_state == `DMA_PRE_WRITE)
last_write_request <= (nread <= 1);
else if (dma_state == `DMA_WRITE_REQ)
begin
if (i_mwb_stall)
last_write_request <= (nwritten >= nread-1);
else
last_write_request <= (nwritten >= nread-2);
end else
last_write_request <= 1'b0;
 
initial last_write_ack = 1'b0;
always @(posedge i_clk)
if((dma_state == `DMA_WRITE_REQ)||(dma_state == `DMA_WRITE_ACK))
begin
if ((i_mwb_ack)&&((~o_mwb_stb)||(i_mwb_stall)))
last_write_ack <= (nwacks+2 == nwritten);
else
last_write_ack <= (nwacks+1 == nwritten);
end else
last_write_ack <= 1'b0;
if (i_reset)
last_write_ack <= 1'b0;
else if((dma_state == `DMA_WRITE_REQ)||(dma_state == `DMA_WRITE_ACK))
begin
if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
last_write_ack <= (nwacks+2 == nwritten);
else
last_write_ack <= (nwacks+1 == nwritten);
end else
last_write_ack <= 1'b0;
 
 
assign o_mwb_cyc = (dma_state == `DMA_READ_REQ)
||(dma_state == `DMA_READ_ACK)
||(dma_state == `DMA_WRITE_REQ)
430,32 → 505,41
// want to read from, unless we are idling. So ... the math is touchy.
//
reg [(LGMEMLEN-1):0] rdaddr;
 
initial rdaddr = 0;
always @(posedge i_clk)
if((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT)
||(dma_state == `DMA_WRITE_ACK))
rdaddr <= 0;
else if ((dma_state == `DMA_PRE_WRITE)
||((dma_state==`DMA_WRITE_REQ)&&(~i_mwb_stall)))
rdaddr <= rdaddr + {{(LGMEMLEN-1){1'b0}},1'b1};
if (i_reset)
rdaddr <= 0;
else if((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT)
||(dma_state == `DMA_WRITE_ACK))
rdaddr <= 0;
else if ((dma_state == `DMA_PRE_WRITE)
||((dma_state==`DMA_WRITE_REQ)&&(!i_mwb_stall)))
rdaddr <= rdaddr + {{(LGMEMLEN-1){1'b0}},1'b1};
 
always @(posedge i_clk)
if ((dma_state != `DMA_WRITE_REQ)||(~i_mwb_stall))
o_mwb_data <= dma_mem[rdaddr];
if (i_reset)
o_mwb_data <= 0;
else if ((dma_state != `DMA_WRITE_REQ)||(!i_mwb_stall))
o_mwb_data <= dma_mem[rdaddr];
always @(posedge i_clk)
if((dma_state == `DMA_READ_REQ)||(dma_state == `DMA_READ_ACK))
dma_mem[nread[(LGMEMLEN-1):0]] <= i_mwb_data;
 
always @(posedge i_clk)
casez(i_swb_addr)
if (i_reset)
o_swb_data <= 0;
else casez(s_addr)
2'b00: o_swb_data <= { (dma_state != `DMA_IDLE), cfg_err,
~cfg_incs, ~cfg_incd,
!cfg_incs, !cfg_incd,
1'b0, nread,
cfg_on_dev_trigger, cfg_dev_trigger,
cfg_blocklen_sub_one
};
2'b01: o_swb_data <= { {(DW-AW){1'b0}}, cfg_len };
2'b10: o_swb_data <= { {(DW-AW){1'b0}}, cfg_raddr};
2'b11: o_swb_data <= { {(DW-AW){1'b0}}, cfg_waddr};
endcase
2'b10: o_swb_data <= { {(DW-2-AW){1'b0}}, cfg_raddr, 2'b00 };
2'b11: o_swb_data <= { {(DW-2-AW){1'b0}}, cfg_waddr, 2'b00 };
endcase
 
// This causes us to wait a minimum of two clocks before starting: One
// to go into the wait state, and then one while in the wait state to
462,30 → 546,291
// develop the trigger.
initial trigger = 1'b0;
always @(posedge i_clk)
if (i_reset)
trigger <= 1'b0;
else
trigger <= (dma_state == `DMA_WAIT)
&&((~cfg_on_dev_trigger)
&&((!cfg_on_dev_trigger)
||(i_dev_ints[cfg_dev_trigger]));
 
// Ack any access. We'll quietly ignore any access where we are busy,
// but ack it anyway. In other words, before writing to the device,
// double check that it isn't busy, and then write.
initial o_swb_ack = 1'b0;
always @(posedge i_clk)
o_swb_ack <= (i_swb_stb);
if (i_reset)
o_swb_ack <= 1'b0;
else if (!i_swb_cyc)
o_swb_ack <= 1'b0;
else
o_swb_ack <= (s_stb);
 
assign o_swb_stall = 1'b0;
 
initial abort = 1'b0;
always @(posedge i_clk)
abort <= (i_rst)||((i_swb_stb)&&(i_swb_we)
&&(i_swb_addr == 2'b00)
&&(i_swb_data == 32'hffed0000));
if (i_reset)
abort <= 1'b0;
else if (dma_state == `DMA_IDLE)
abort <= 1'b0;
else
abort <= ((s_stb)&&(s_we)
&&(s_addr == 2'b00)
&&(s_data == 32'hffed0000));
 
initial user_halt = 1'b0;
always @(posedge i_clk)
user_halt <= ((user_halt)&&(dma_state != `DMA_IDLE))
||((i_swb_stb)&&(i_swb_we)&&(dma_state != `DMA_IDLE)
&&(i_swb_addr == 2'b00)
&&(i_swb_data == 32'hafed0000));
||((s_stb)&&(s_we)&&(dma_state != `DMA_IDLE)
&&(s_addr == 2'b00)
&&(s_data == 32'hafed0000));
 
 
// Make verilator happy
// verilator lint_off UNUSED
wire unused;
assign unused = s_cyc;
// verilator lint_on UNUSED
`ifdef FORMAL
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
always @(*)
if (!f_past_valid)
assume(i_reset);
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
assert(dma_state == `DMA_IDLE);
 
parameter F_SLV_LGDEPTH = 3;
parameter F_MSTR_LGDEPTH = LGMEMLEN+1;
 
wire [F_SLV_LGDEPTH-1:0] f_swb_nreqs, f_swb_nacks, f_swb_outstanding;
wire [F_MSTR_LGDEPTH-1:0] f_mwb_nreqs, f_mwb_nacks, f_mwb_outstanding;
 
fwb_slave #(
.AW(2), .DW(32), .F_MAX_STALL(0), .F_MAX_ACK_DELAY(2),
.F_LGDEPTH(F_SLV_LGDEPTH)
) control_port(i_clk, i_reset,
i_swb_cyc, i_swb_stb, i_swb_we, i_swb_addr, i_swb_data,4'b1111,
o_swb_ack, o_swb_stall, o_swb_data, 1'b0,
f_swb_nreqs, f_swb_nacks, f_swb_outstanding);
always @(*)
assert(o_swb_stall == 0);
`ifdef DELAY_ACCESS
always @(*)
if ((!i_reset)&&(i_swb_cyc))
begin
if ((!s_stb)&&(!o_swb_ack))
assert(f_swb_outstanding == 0);
else if ((s_stb)&&(!o_swb_ack))
assert(f_swb_outstanding == 1);
else if ((!s_stb)&&(o_swb_ack))
assert(f_swb_outstanding == 1);
else if ((s_stb)&&(o_swb_ack))
assert(f_swb_outstanding == 2);
end
`else
always @(*)
if ((!i_reset)&&(!o_swb_ack))
assert(f_swb_outstanding == 0);
`endif
 
fwb_master #(.AW(AW), .DW(32), .F_MAX_STALL(4), .F_MAX_ACK_DELAY(8),
.F_LGDEPTH(F_MSTR_LGDEPTH),
.F_OPT_RMW_BUS_OPTION(1'b1),
.F_OPT_DISCONTINUOUS(1'b0),
.F_OPT_SOURCE(1'b1)
) external_bus(i_clk, i_reset,
o_mwb_cyc, o_mwb_stb, o_mwb_we, o_mwb_addr, o_mwb_data,4'b1111,
i_mwb_ack, i_mwb_stall, i_mwb_data, i_mwb_err,
f_mwb_nreqs, f_mwb_nacks, f_mwb_outstanding);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(dma_state == `DMA_IDLE)))
assert(o_mwb_cyc == 1'b0);
 
always @(*)
if ((o_mwb_cyc)&&(!o_mwb_we))
begin
assert(nracks == f_mwb_nreqs);
assert(nread == f_mwb_nacks);
end
 
always @(*)
if ((o_mwb_cyc)&&(o_mwb_we))
begin
assert(nwacks == f_mwb_nacks);
assert(nwritten == f_mwb_nreqs);
end
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(abort))&&($past(dma_state != `DMA_IDLE)))
assert(dma_state == `DMA_IDLE);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_mwb_cyc))&&(o_mwb_cyc)&&(
(( !cfg_incs)&&(!o_mwb_we))
||((!cfg_incd)&&( o_mwb_we))))
begin
assert(o_mwb_addr == $past(o_mwb_addr));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_mwb_cyc))&&(
((!cfg_incs)||($past(o_mwb_we))||(!$past(i_mwb_ack)))))
assert(cfg_raddr == $past(cfg_raddr));
 
always @(posedge i_clk)
if ((f_past_valid)&&(dma_state == `DMA_WRITE_REQ))
assert(cfg_waddr == o_mwb_addr);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))
&&($past(o_mwb_stb))&&(!$past(i_mwb_stall)))
begin
assert( ((!cfg_incs)&&(!$past(o_mwb_we)))
||((!cfg_incd)&&( $past(o_mwb_we)))
||(o_mwb_addr==$past(o_mwb_addr)+1'b1));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(o_mwb_cyc))&&(o_mwb_cyc))
begin
if (o_mwb_we)
assert(o_mwb_addr == cfg_waddr);
else
assert(o_mwb_addr == cfg_raddr);
end
 
always @(*)
assert(cfg_len_nonzero == (cfg_len != 0));
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
begin
assert(cfg_len == 0);
assert(!cfg_len_nonzero);
end else if ((f_past_valid)&&($past(o_mwb_cyc)))
begin
if (($past(i_mwb_ack))&&($past(o_mwb_we)))
assert(cfg_len == $past(cfg_len)-1'b1);
else
assert(cfg_len == $past(cfg_len));
end else if ((f_past_valid)&&(($past(dma_state) != `DMA_IDLE)
||(!$past(s_stb))||(!$past(s_we))
||($past(s_addr)!=2'b01)))
assert(cfg_len == $past(cfg_len));
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_mwb_cyc))&&($past(cfg_len == 0))
&&(!$past(user_halt)))
begin
assert(cfg_len == 0);
assert((dma_state != $past(dma_state))||(!o_mwb_cyc));
end
 
always @(posedge i_clk)
if (cfg_len == 0)
assert(!o_mwb_stb);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(dma_state) != `DMA_IDLE))
begin
assert(cfg_incs == $past(cfg_incs));
assert(cfg_incd == $past(cfg_incd));
assert(cfg_blocklen_sub_one == $past(cfg_blocklen_sub_one));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(dma_state) == `DMA_IDLE))
assert(cfg_len_nonzero == (cfg_len != 0));
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(o_mwb_cyc))||(!$past(o_mwb_we)))
assert((nwritten == 0)&&(nwacks == 0));
always @(posedge i_clk)
if ((o_mwb_cyc)&&(!o_mwb_we))
assert(bus_nracks <= cfg_len);
always @(posedge i_clk)
if ((o_mwb_cyc)&&(!o_mwb_we))
assert(nread <= nracks);
always @(posedge i_clk)
if ((o_mwb_cyc)&&(o_mwb_we))
assert(nwritten-nwacks
+((o_mwb_stb)? 1'b1:1'b0)
- f_mwb_outstanding
// -((i_mwb_ack)? 1'b1:1'b0)
<= cfg_len);
always @(*)
assert(f_mwb_outstanding
+ ((o_mwb_stb)? 1'b1:1'b0) <= cfg_len);
 
wire [LGMEMLEN:0] f_cfg_blocklen;
assign f_cfg_blocklen = { 1'b0, cfg_blocklen_sub_one} + 1'b1;
 
always @(*)
if (dma_state == `DMA_WAIT)
assert(cfg_len > 0);
 
always @(*)
if ((o_mwb_stb)&&(o_mwb_we))
assert(nread == nracks);
 
always @(*)
if (o_mwb_stb)
assert(nwritten <= cfg_blocklen_sub_one);
always @(posedge i_clk)
assert(nwritten <= f_cfg_blocklen);
 
always @(*)
if ((o_mwb_stb)&&(!o_mwb_we))
assert(nracks < f_cfg_blocklen);
else
assert(nracks <= f_cfg_blocklen);
always @(*)
if ((o_mwb_cyc)&&(i_mwb_ack)&&(!o_mwb_we))
assert(nread < f_cfg_blocklen);
always @(*)
assert(nread <= nracks);
 
always @(*)
if ((o_mwb_cyc)&&(o_mwb_we)&&(!user_halt))
assert(nread == nracks);
 
always @(*)
if ((o_mwb_cyc)&&(o_mwb_we))
assert(nwritten >= nwacks);
 
always @(*)
if (dma_state == `DMA_WRITE_REQ)
assert(last_write_request == (nwritten == nread-1));
 
always @(*)
assert(nwritten >= nwacks);
 
always @(*)
assert(nread >= nwritten);
 
always @(*)
assert(nracks >= nread);
 
wire [LGMEMLEN:0] f_npending;
assign f_npending = nread-nwacks;
always @(*)
if (dma_state != `DMA_IDLE)
assert({ {(AW-LGMEMLEN-1){1'b0}}, f_npending} <= cfg_len);
 
always @(posedge i_clk)
begin
assert(cfg_len_nonzero == (cfg_len != 0));
if ((f_past_valid)&&($past(dma_state != `DMA_IDLE))&&($past(cfg_len == 0)))
assert(cfg_len == 0);
end
 
 
`endif
endmodule
 
/wbwatchdog.v
6,32 → 6,24
//
// Purpose: A Zip timer, redesigned to be a bus watchdog
//
// This is a **really** stripped down Zip Timer. All options for external
// control have been removed. This timer may be reset, and ... that's
// about it. The goal is that this stripped down timer be used as a bus
// watchdog element. Even at that, it's not really fully featured. The
// rest of the important features can be found in the zipsystem module.
// This is basically a timer, but there are some unique features to it.
//
// As a historical note, the wishbone watchdog timer began as a normal
// timer, with some fixed inputs. This makes sense, if you think about it:
// if the goal is to interrupt a stalled wishbone transaction by inserting
// a bus error, then you can't use the bus to set it up or configure it
// simply because the bus in question is ... well, unreliable. You're
// trying to make it reliable.
// 1. There is no way to "write" the timeout to this watchdog. It is
// fixed with an input (that is assumed to be constant)
// 2. The counter returns to i_timer and the interrupt is cleared on any
// reset.
// 3. Between resets, the counter counts down to zero. Once (and if) it
// hits zero, it will remain at zero until reset.
// 4. Any time the counter is at zero, and until the reset that resets
// the counter, the output interrupt will be set.
//
// The problem with using the ziptimer in a stripped down implementation
// was that the fixed inputs caused the synthesis tool to complain about
// the use of registers values would never change. This solves that
// problem by explicitly removing the cruft that would otherwise
// just create synthesis warnings and errors.
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015,2017, Gisselquist Technology, LLC
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
55,28 → 47,84
////////////////////////////////////////////////////////////////////////////////
//
//
module wbwatchdog(i_clk, i_rst, i_ce, i_timeout, o_int);
`default_nettype none
//
module wbwatchdog(i_clk, i_reset, i_timeout, o_int);
parameter BW = 32;
input i_clk, i_rst, i_ce;
input wire i_clk, i_reset;
// Inputs (these were at one time wishbone controlled ...)
input [(BW-1):0] i_timeout;
input wire [(BW-1):0] i_timeout;
// Interrupt line
output reg o_int;
 
reg [(BW-1):0] r_value;
initial r_value = 0;
initial r_value = {(BW){1'b1}};
always @(posedge i_clk)
if (i_rst)
if (i_reset)
r_value <= i_timeout[(BW-1):0];
else if ((i_ce)&&(~o_int))
else if (!o_int)
r_value <= r_value + {(BW){1'b1}}; // r_value - 1;
 
// Set the interrupt on our last tick.
initial o_int = 1'b0;
always @(posedge i_clk)
if ((i_rst)||(~i_ce))
if (i_reset)
o_int <= 1'b0;
else
else if (!o_int)
o_int <= (r_value == { {(BW-1){1'b0}}, 1'b1 });
 
`ifdef FORMAL
reg f_past_valid;
 
initial f_past_valid = 1'b0;
always @(posedge f_past_valid)
f_past_valid <= 1'b1;
 
///////////////////////////////////////////////
//
//
// Assumptions about our inputs
//
//
///////////////////////////////////////////////
always @(*)
assume(i_timeout > 1);
always @(posedge i_clk)
if (f_past_valid)
assume(i_timeout == $past(i_timeout));
 
//
//
///////////////////////////////////////////////
//
//
// Assertions about our internal state and our outputs
//
//
///////////////////////////////////////////////
//
//
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_int))&&(!$past(i_reset)))
assert(o_int);
 
always @(*)
assert(o_int == (r_value == 0));
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(o_int)))
begin
assert(r_value == $past(r_value)-1'b1);
end
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
begin
if (!f_past_valid)
assert(r_value == {(BW){1'b1}});
else // if ($past(i_reset))
assert(r_value == $past(i_timeout));
assert(!o_int);
end
`endif
endmodule
/zipcounter.v
27,7 → 27,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
51,15 → 51,20
////////////////////////////////////////////////////////////////////////////////
//
//
module zipcounter(i_clk, i_ce,
`default_nettype none
//
module zipcounter(i_clk, i_reset, i_event,
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,
o_wb_ack, o_wb_stall, o_wb_data,
o_int);
parameter BW = 32;
input i_clk, i_ce;
//
localparam F_LGDEPTH = 2;
//
input wire i_clk, i_reset, i_event;
// Wishbone inputs
input i_wb_cyc, i_wb_stb, i_wb_we;
input [(BW-1):0] i_wb_data;
input wire i_wb_cyc, i_wb_stb, i_wb_we;
input wire [(BW-1):0] i_wb_data;
// Wishbone outputs
output reg o_wb_ack;
output wire o_wb_stall;
70,9 → 75,11
initial o_int = 0;
initial o_wb_data = 32'h00;
always @(posedge i_clk)
if ((i_wb_stb)&&(i_wb_we))
if (i_reset)
{ o_int, o_wb_data } <= 0;
else if ((i_wb_stb)&&(i_wb_we))
{ o_int, o_wb_data } <= { 1'b0, i_wb_data };
else if (i_ce)
else if (i_event)
{ o_int, o_wb_data } <= o_wb_data+{{(BW-1){1'b0}},1'b1};
else
o_int <= 1'b0;
79,6 → 86,124
 
initial o_wb_ack = 1'b0;
always @(posedge i_clk)
o_wb_ack <= (i_wb_stb);
if (i_reset)
o_wb_ack <= 1'b0;
else
o_wb_ack <= i_wb_stb;
assign o_wb_stall = 1'b0;
 
 
// Make verilator happy
// verilator lint_off UNUSED
wire unused;
assign unused = i_wb_cyc;
// verilator lint_on UNUSED
 
`ifdef FORMAL
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
always @(*)
if (!f_past_valid)
assume(i_reset);
 
////////////////////////////////////////////////
//
//
// Assumptions about our inputs
//
//
////////////////////////////////////////////////
//
 
////////////////////////////////////////////////
//
//
// Bus interface properties
//
//
////////////////////////////////////////////////
//
 
// We never stall the bus
always @(*)
assert(!o_wb_stall);
 
// We always ack every transaction on the following clock
always @(posedge i_clk)
assert(o_wb_ack == ((f_past_valid)&&(!$past(i_reset))
&&($past(i_wb_stb))));
 
wire [(F_LGDEPTH-1):0] f_nreqs, f_nacks, f_outstanding;
 
fwb_slave #( .AW(1), .F_MAX_STALL(0),
.F_MAX_ACK_DELAY(1), .F_LGDEPTH(F_LGDEPTH)
) fwbi(i_clk, i_reset,
i_wb_cyc, i_wb_stb, i_wb_we, 1'b0, i_wb_data, 4'hf,
o_wb_ack, o_wb_stall, o_wb_data, 1'b0,
f_nreqs, f_nacks, f_outstanding);
 
always @(*)
if ((o_wb_ack)&&(i_wb_cyc))
assert(f_outstanding==1);
else
assert(f_outstanding == 0);
 
////////////////////////////////////////////////
//
//
// Assumptions about our outputs
//
//
////////////////////////////////////////////////
//
 
// Drop the interrupt line and reset the counter on any reset
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
assert((!o_int)&&(o_wb_data == 0));
 
// Clear the interrupt and set the counter on any write (other than
// during a reset)
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))
&&($past(i_wb_stb))&&($past(i_wb_we)))
assert((!o_int)&&(o_wb_data == $past(i_wb_data)));
 
// Normal logic of the routine itself
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_wb_stb)))
begin
if (!$past(i_event))
begin
// If the CE line wasn't set on the last clock, then the
// counter must not change, and the interrupt line must
// be low.
assert(o_wb_data == $past(o_wb_data));
assert(!o_int);
end else // if ($past(i_event))
begin
// Otherwise, if the CE line was high on the last clock,
// then our counter should have incremented.
assert(o_wb_data == $past(o_wb_data) + 1'b1);
 
// Likewise, if the counter rolled over, then the
// output interrupt, o_int, should be true.
if ($past(o_wb_data)=={(BW){1'b1}})
assert(o_int);
else
// In all other circumstances it should be clear
assert(!o_int);
end
end
 
//
// The output interrupt should never be true two clocks in a row
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_int)))
assert(!o_int);
 
`endif
endmodule
/zipjiffies.v
45,7 → 45,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
69,15 → 69,17
////////////////////////////////////////////////////////////////////////////////
//
//
module zipjiffies(i_clk, i_ce,
`default_nettype none
//
module zipjiffies(i_clk, i_reset, i_ce,
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,
o_wb_ack, o_wb_stall, o_wb_data,
o_int);
parameter BW = 32;
input i_clk, i_ce;
input wire i_clk, i_reset, i_ce;
// Wishbone inputs
input i_wb_cyc, i_wb_stb, i_wb_we;
input [(BW-1):0] i_wb_data;
input wire i_wb_cyc, i_wb_stb, i_wb_we;
input wire [(BW-1):0] i_wb_data;
// Wishbone outputs
output reg o_wb_ack;
output wire o_wb_stall;
94,8 → 96,11
// together, one clock at a time.
//
reg [(BW-1):0] r_counter;
initial r_counter = 0;
always @(posedge i_clk)
if (i_ce)
if (i_reset)
r_counter <= 0;
else if (i_ce)
r_counter <= r_counter+1;
 
//
110,9 → 115,13
 
initial new_set = 1'b0;
always @(posedge i_clk)
if (i_reset)
begin
// Delay things by a clock to simplify our logic
new_set <= ((i_wb_cyc)&&(i_wb_stb)&&(i_wb_we));
new_set <= 1'b0;
new_when <= 0;
end else begin
// Delay WB commands (writes) by a clock to simplify our logic
new_set <= ((i_wb_stb)&&(i_wb_we));
// new_when is a don't care when new_set = 0, so don't worry
// about setting it at all times.
new_when<= i_wb_data;
121,7 → 130,11
initial o_int = 1'b0;
initial int_set = 1'b0;
always @(posedge i_clk)
if (i_reset)
begin
o_int <= 0;
int_set <= 0;
end else begin
o_int <= 1'b0;
if ((i_ce)&&(int_set)&&(r_counter == int_when))
// Interrupts are self-clearing
133,18 → 146,151
int_set <= 1'b1;
else if ((i_ce)&&(r_counter == int_when))
int_set <= 1'b0;
 
if ((new_set)&&(till_wb > 0)&&((till_wb<till_when)||(~int_set)))
int_when <= new_when;
end
 
always @(posedge i_clk)
if ((new_set)&&(till_wb > 0)&&((till_wb<till_when)||(!int_set)))
int_when <= new_when;
 
//
// Acknowledge any wishbone accesses -- everything we did took only
// one clock anyway.
//
initial o_wb_ack = 1'b0;
always @(posedge i_clk)
o_wb_ack <= (i_wb_cyc)&&(i_wb_stb);
if (i_reset)
o_wb_ack <= 1'b0;
else
o_wb_ack <= i_wb_stb;
 
assign o_wb_data = r_counter;
assign o_wb_stall = 1'b0;
 
// Make verilator happy
// verilator lint_off UNUSED
wire unused;
assign unused = i_wb_cyc;
// verilator lint_on UNUSED
`ifdef FORMAL
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
////////////////////////////////////////////////
//
//
// Assumptions about our inputs
//
//
////////////////////////////////////////////////
//
// Some basic WB assumtions
 
// We will not start out in a wishbone cycle
initial assume(!i_wb_cyc);
 
// Following any reset the cycle line will be low
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
assume(!i_wb_cyc);
 
// Anytime the stb is high, the cycle line must also be high
always @(posedge i_clk)
assume((!i_wb_stb)||(i_wb_cyc));
 
 
////////////////////////////////////////////////
//
//
// Assumptions about our bus outputs
//
//
////////////////////////////////////////////////
//
 
// We never stall the bus
always @(*)
assert(!o_wb_stall);
// We always ack every transaction on the following clock
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb)))
assert(o_wb_ack);
else
assert(!o_wb_ack);
 
 
////////////////////////////////////////////////
//
//
// Assumptions about our internal state and our outputs
//
//
////////////////////////////////////////////////
//
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
begin
assert(!o_wb_ack);
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
&&($past(i_wb_we)))
assert(new_when == $past(i_wb_data));
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
&&($past(i_wb_we)))
assert(new_set);
else
assert(!new_set);
 
//
//
//
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
assert(!o_int);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
begin
assert(!int_set);
assert(!new_set);
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(new_set))
&&(!$past(till_wb[BW-1]))
&&($past(till_wb) > 0))
assert(int_set);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_ce))
&&($past(r_counter)==$past(int_when)))
begin
assert((o_int)||(!$past(int_set)));
assert((!int_set)||($past(new_set)));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(new_set))&&(!$past(int_set)))
assert(!int_set);
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
assert(!o_int);
else if (($past(new_set))&&($past(till_wb) < 0))
assert(o_int);
 
always @(posedge i_clk)
if ((f_past_valid)&&
((!$past(new_set))
||($past(till_wb[BW-1]))
||($past(till_wb == 0))))
assert(int_when == $past(int_when));
//
`endif
endmodule
/zipmmu.v
8,7 → 8,7
// unit, that is configured from one wishbone bus and modifies a
// separate wishbone bus. Both busses will not be active at the same time.
//
// The idea is that the CPU can use one portion of its peripheral
// The idea is that the CPU can use one portion of its peripheral
// system memory space to configure the MMU, and another portion of its
// memory space to access the MMU. Even more, configuring the MMU is to
// be done when the CPU is in supervisor mode. This means that all
33,7 → 33,7
// clock cycle. Further, multiple accesses to the same page
// should not take any longer than the one cycle delay. Accesses
// to other pages should take a minimum number of clocks.
// Accesses from one page to the next, such as from one page to
// Accesses from one page to the next, such as from one page to
// the next subsequent one, should cost no delays.
//
// 2. One independent control word to set the current context
48,7 → 48,7
// bus of width (lgpage+17), or a memory space of (2^(lgpage+17)).
// Under this formula, the number of valid address bits can range
// from 17 to 32.
// - Contains 4 RdOnly bits indicating log_2 TLB table size.
// - Contains 4 RdOnly bits indicating log_2 TLB table size.
// Size is given by (2^(lgsize)). I'm considering sizes of 6,7&8
// - Contains 4 RdOnly bits indicating the log page size, offset by
// eight. Page sizes are therefore given by (2^(lgpage+8)), and
69,7 → 69,7
// Supervisor *cannot* have page table entries, since there are no
// interrupts (page faults) allowed in supervisor context.
//
// To be valid,
// To be valid,
// Context Size (1..16), NFlags ( 4) < Page Size (8-23 bits)
// Page size (8-23 bits) > NFlags bits (4)
//
78,7 → 78,7
// 3. One status word, which contains the address that failed and some
// flags:
//
// Top Virtual address bits indicate which page ... caused a problem.
// Top Virtual address bits indicate which page ... caused a problem.
// These will be the top N bits of the word, where N is the size
// of the virtual address bits. (Bits are cleared upon any write.)
//
87,7 → 87,7
// - 4: Multiple page table matches
// - 2: Attempt to write a read-only page
// - 1: Page not found
//
//
// 3. Two words per active page table entry, accessed through two bus
// addresses. This word contains:
//
103,19 → 103,16
// 1-bit Read-only / ~written (user set/read/written)
// If set, this page will cause a fault on any
// 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
// This an be used to implement a least-recently
// used measure. The hardware will set this value
// when the page is accessed. The user can also
// 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)
//
125,7 → 122,7
//
// 4. Can read/write this word in two parts:
//
// (20-bit Virtual )(8-bits lower context)(4-bit flags), and
// (20-bit Virtual )(8-bits lower context)(4-bit flags), and
// (20-bit Physical)(8-bits upper context)(4-bit flags)
//
// Actual bit lengths will vary as the MMU configuration changes,
140,10 → 137,10
// bits in the control register.
//
// +----+----+-----+----+----+----+----+--+--+--+--+
// | | Lower 8b| R| A| C| T|
// | 20-bit Virtual page ID | Context | O| C| C| H|
// |(top 20 bits of the addr)| ID | n| C| H| S|
// | | | W| S| E| P|
// | | Lower 8b| R| E| C| A|
// | 20-bit Virtual page ID | Context | O| X| C| C|
// |(top 20 bits of the addr)| ID | n| E| H| C|
// | | | W| F| E| S|
// +----+----+-----+----+----+----+----+--+--+--+--+
//
// +----+----+-----+----+----+----+----+--+--+--+--+
150,7 → 147,7
// | | Upper 8b| R| A| C| T|
// | 20-bit Physical pg ID | Context | O| C| C| H|
// |(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
163,7 → 160,7
// will have long been available, the "Valid" bit will be turned
// on and associated with the physical mapping.
// - On any data-write (pf doesn't write), MMU sends [Context,Va,Pa]
// TLB mapping to the pf-cache.
// TLB mapping to the pf-cache.
// - If the write matches any physical PF-cache addresses (???), the
// pfcache declares that address line invalid, and just plain
// clears the valid bit for that page.
189,7 → 186,7
//
////////////////////////////////////////////////////////////////////////////////
//
// 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
// modify it under the terms of the GNU General Public License as published
211,9 → 208,20
//
//
////////////////////////////////////////////////////////////////////////////////
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,
o_rtn_stall, o_rtn_ack, o_rtn_err,
o_rtn_miss, o_rtn_data,
220,36 → 228,66
pf_return_stb, pf_return_we,
pf_return_p, pf_return_v,
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 ...)
// 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 = ADDRESS_WIDTH,
// Page sizes must allow for a minimum of one context
// bit per page, plus four flag bits, hence the minimum
// number of bits for an address within a page is 5
LGPGSZ=(PLGPGSZ < 5)? 5:PLGPGSZ,
// The number of context bits is twice the number of
// bits left over from DW after removing the LGPGSZ
// and flags bits.
LGCTXT=(((DW-LGPGSZ-4)<<1)<PLGCTXT)?
((DW-LGPGSZ-4)<<1):PLGCTXT,
LGPGSZB=(PLGPGSZB < 5)? 5:PLGPGSZB, // in bytes
LGPGSZW=LGPGSZB-2, // in words
// The context value for a given page can be split
// across both virtual and physical words. It cannot
// have so many bits to it that it takes more bits
// then are available.
LGCTXT=((2*LGPGSZB-4)>PLGCTXT)?
PLGCTXT:(2*LGPGSZB-4),
// 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= (LGCTXT-LGLCTX),
VAW=(DW-LGPGSZ), // Virtual address width
PAW=(AW-LGPGSZ), // Physical address width
LGHCTX= (LGCTXT-LGLCTX>0)?(LGCTXT-LGLCTX):0,
VAW=(DW-LGPGSZB), // Virtual address width, in bytes
PAW=(AW-LGPGSZW), // Physical address width, in words
TBL_BITS = LGTBL, // Bits necessary to addr tbl
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 wire i_wbs_cyc_stb;
input wire i_wbs_we;
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 i_wbm_cyc, i_wbm_stb;
input wire i_wbm_cyc, i_wbm_stb;
//
input i_wb_we;
input [(DW-1):0] i_wb_addr;
input [(DW-1):0] i_wb_data;
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
output reg o_cyc;
256,17 → 294,18
output wire o_stb, o_we;
output reg [(AW-1):0] o_addr;
output reg [(DW-1):0] o_data;
output reg [(DW/8-1):0] o_sel;
// and get our return information from driving the slave ...
input i_stall, i_ack, i_err;
input [(DW-1):0] i_data;
input wire i_stall, i_ack, i_err;
input wire [(DW-1):0] i_data;
//
// 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
// wires ...
output wire o_rtn_stall;
output reg o_rtn_ack;
output wire o_rtn_ack;
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 ...
output wire pf_return_stb, // snoop data is valid
pf_return_we; // snoop data is chnging
279,60 → 318,67
//
//
//
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 [(DW-LGPGSZ-1):0] tlb_vdata [0:(TBL_SIZE-1)];
reg [(AW-LGPGSZ-1):0] tlb_pdata [0:(TBL_SIZE-1)];
reg [(VAW-1):0] tlb_vdata [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 wr_control, wr_status, wr_vtable, wr_ptable;
wire adr_control, adr_vtable, adr_ptable;
wire wr_control, wr_vtable, wr_ptable;
wire [(LGTBL-1):0] wr_tlb_addr;
assign wr_tlb_addr= i_wb_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_status = (i_ctrl_cyc_stb)&&(~i_wb_addr[(LGTBL+1)])&&( i_wb_addr[0]);
assign adr_vtable = (i_ctrl_cyc_stb)&&( i_wb_addr[(LGTBL+1)])&&(~i_wb_addr[0]);
assign adr_ptable = (i_ctrl_cyc_stb)&&( i_wb_addr[(LGTBL+1)])&&( i_wb_addr[0]);
assign wr_control = (adr_control)&&(i_wb_we);
assign wr_status = (adr_status )&&(i_wb_we);
assign wr_vtable = (adr_vtable )&&(i_wb_we);
assign wr_ptable = (adr_ptable )&&(i_wb_we);
assign wr_tlb_addr= i_wbs_addr[(LGTBL):1]; // Leave bottom for V/P
assign adr_control= (i_wbs_cyc_stb)&&(~i_wbs_addr[(LGTBL+1)])&&(~i_wbs_addr[0]);
assign adr_vtable = (i_wbs_cyc_stb)&&( i_wbs_addr[(LGTBL+1)])&&(~i_wbs_addr[0]);
assign adr_ptable = (i_wbs_cyc_stb)&&( i_wbs_addr[(LGTBL+1)])&&( i_wbs_addr[0]);
assign wr_control = (adr_control)&&(i_wbs_we);
assign wr_vtable = (adr_vtable )&&(i_wbs_we);
assign wr_ptable = (adr_ptable )&&(i_wbs_we);
 
reg setup_ack, z_context, setup_this_page_flag;
reg [(DW-1):0] setup_data;
reg [(LGCTXT-1):0] r_context_word, setup_page;
reg z_context;
wire kernel_context;
reg [(LGCTXT-1):0] r_context_word;
//
wire [31:0] w_control_data,w_vtable_reg,w_ptable_reg;
wire [(LGCTXT-1):0] w_ctable_reg;
wire [31:0] w_control_data, w_ptable_reg;
reg [31:0] w_vtable_reg;
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 [(DW-1):0] r_addr;
reg r_pending, r_we, r_exe, r_valid,
last_page_valid, last_ro, last_exe;
reg [(DW-3):0] r_addr;
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 [(VAW-1):0] last_vpage;
//
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;
//
wire ro_flag, simple_miss, ro_miss, table_err, cachable;
reg p_tlb_miss,p_tlb_err, pf_stb, pf_cachable;
wire ro_flag, exe_flag, simple_miss, ro_miss, exe_miss, table_err, cachable;
reg pf_stb, pf_cachable;
reg miss_pending;
//
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
//
//
//////////////////////////////////////////
340,23 → 386,40
begin
// Write to the Translation lookaside buffer
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)
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
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)
tlb_cdata[wr_tlb_addr][((LGCTXT>=8)? 7:(LGCTXT-1)):0]
<= i_wb_data[((LGCTXT>=8)? 11:(4+LGCTXT-1)):4];
if ((wr_ptable)&&(LGCTXT > 8))
tlb_cdata[wr_tlb_addr][(LGCTXT-1):8]
<= i_wb_data[(4+LGCTXT-8-1):4];
setup_ack <= (i_ctrl_cyc_stb)&&(!i_reset);
tlb_flags[wr_tlb_addr] <= { i_wbs_data[3:1], 1'b0 };
if (wr_vtable)
tlb_cdata[wr_tlb_addr][(LGLCTX-1):0]
<= i_wbs_data[(LGLCTX+4-1):4];
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
initial z_context = 1'b1;
initial r_context_word = 0;
363,48 → 426,62
always @(posedge i_clk)
if (wr_control)
begin
r_context_word <= i_wb_data[(LGCTXT-1):0];
z_context <= (i_wb_data[(LGCTXT-1):0] == {(LGCTXT){1'b0}});
r_context_word <= i_wbs_data[(LGCTXT-1):0];
z_context <= (i_wbs_data[(LGCTXT-1):0] == {(LGCTXT){1'b0}});
end
assign kernel_context = (z_context)||(!i_gie);
// Status words cannot be written to
 
/* verilator lint_off WIDTH */
assign w_control_data[31:28] = AW-17;
assign w_control_data[27:24] = LGTBL;
assign w_control_data[23:20] = LGPGSZ-8;
assign w_control_data[19:16] = LGCTXT-1;
/* verilator lint_on WIDTH */
always @(posedge i_clk)
if (i_reset)
tlb_valid <= 0;
else if (wr_ptable)
tlb_valid[wr_tlb_addr]<=1'b1; //(i_wbs_data[(AW+1):LGPGSZB]!=0);
 
/* 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_vtable_reg[(DW-1):LGPGSZ] = tlb_vdata[wr_tlb_addr];
assign w_vtable_reg[(LGPGSZ-1):(LGLCTX+4-1)] = 0;
assign w_vtable_reg[(LGLCTX+4-1):4] = { tlb_cdata[wr_tlb_addr][(LGLCTX-1):0] };
assign w_vtable_reg[ 3:0] = { tlb_flags[wr_tlb_addr], 1'b0 };
always @(*)
begin
w_vtable_reg = 0;
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] };
assign w_ptable_reg[LGPGSZ:(4+LGHCTX)] = 0;
assign w_ptable_reg[ 3:0] = { tlb_flags[wr_tlb_addr], 1'b0 };
assign w_ctable_reg = tlb_cdata[wr_tlb_addr];
assign w_ptable_reg[ 3:0] = 4'h0;
//
generate
if (4+LGHCTX-1>4)
assign w_ptable_reg[(4+LGHCTX-1):4] = {
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
 
//
// Now, reading from the bus
/*
wire [(LGCTXT-1):0] w_ctable_reg;
assign w_ctable_reg = tlb_cdata[wr_tlb_addr];
reg setup_this_page_flag;
reg [(LGCTXT-1):0] setup_page;
initial setup_this_page_flag = 1'b0;
always @(posedge i_clk)
setup_page <= w_ctable_reg;
always @(posedge i_clk)
setup_this_page_flag <= (i_ctrl_cyc_stb)&&(i_wb_addr[LGTBL+1]);
always @(posedge i_clk)
case({i_wb_addr[LGTBL+1],i_wb_addr[0]})
2'b00: setup_data <= w_control_data;
2'b01: setup_data <= status_word;
2'b10: setup_data <= w_vtable_reg;
2'b11: setup_data <= w_ptable_reg;
endcase
setup_this_page_flag <= (!i_reset)&&(i_wbs_cyc_stb)&&(i_wbs_addr[LGTBL+1]);
*/
 
 
 
415,7 → 492,6
//
//
//////////////////////////////////////////
assign w_mmu_err_vaddr = { {(DW-AW){1'b0}}, r_mmu_err_vaddr };
 
//
//
424,125 → 500,280
// 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_valid = 1'b0;
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
if (!o_rtn_stall)
begin
r_pending <= i_wbm_stb;
r_we <= i_wb_we;
r_addr <= i_wb_addr;
r_data <= i_wb_data;
r_valid <= (i_wbm_stb)&&((z_context)||((last_page_valid)
&&(i_wb_addr[(DW-1):LGPGSZ] == last_vpage)
&&((!last_ro)||(!i_wb_we))));
r_pending <= (i_wbm_stb)&&(!kernel_context)
&&(!this_page_valid);
r_we <= i_wbm_we;
r_exe <= i_wbm_exe;
o_addr <= { { (kernel_context)?
i_wbm_addr[(AW-1):LGPGSZW] : last_ppage },
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;
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
r_valid <= (r_valid)||((last_page_valid)
&&(r_addr[(DW-1):LGPGSZ] == last_vpage)
&&((!last_ro)||(!r_we)));
r_pending<= (r_pending)&&(i_wbm_cyc);
s_pending <= r_pending;
r_pending <= 1'b0;
s_pending <= 1'b0;
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_valid <= 1'b0;
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.
// If we don't already know, then the pipeline must be stalled for a
// while ...
genvar k, s;
generate
for(k=0; k<TBL_BITS; k = k + 1)
for(k=0; k<TBL_SIZE; k = k + 1)
assign r_tlb_match[k] =
// The page must be valid
(tlb_valid[k])
// Virtual address must match
((tlb_vdata[k] == r_addr[(DW-1):LGPGSZ])
&&(tlb_vdata[k] == r_vpage)
// 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
 
initial s_tlb_miss = 1'b0;
initial s_tlb_hit = 1'b0;
generate
integer i;
always @(posedge i_clk)
begin // valid when s_ becomes valid
s_tlb_addr <= {(LGTBL){1'b0}};
for(k=0; k<TBL_SIZE; k=k+1)
for(s=0; s<LGTBL; s=s+1)
if (((k&(1<<s))!=0)&&(r_tlb_match[k]))
s_tlb_addr[s] <= 1'b1;
s_tlb_miss <= (r_pending)&&(r_tlb_match[(TBL_BITS-1):0] == 0);
for(i=0; i<TBL_SIZE; i=i+1)
if (r_tlb_match[i])
s_tlb_addr <= i[(LGTBL-1):0];
s_tlb_miss <= (r_pending)&&(r_tlb_match == 0);
s_tlb_hit <= 1'b0;
for(k=0; k<TBL_SIZE; k=k+1)
if (r_tlb_match == (1<<k))
s_tlb_hit <= (r_pending);
for(i=0; i<TBL_SIZE; i=i+1)
if (r_tlb_match == (1<<i))
s_tlb_hit <= (r_pending)&&(!r_valid)&&(i_wbm_cyc);
end endgenerate
 
 
// Third clock: Read from the address the virtual table offset,
// 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 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 cachable = tlb_flags[s_tlb_addr][1];
// assign tlb_access_flag = tlb_flags[s_tlb_addr][2];
assign vpage = tlb_vdata[s_tlb_addr];
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 p_tlb_err = 1'b0;
initial p_tlb_miss = 1'b0;
initial last_ppage = 0;
initial last_vpage = 0;
always @(posedge i_clk)
if (i_reset)
begin
p_tlb_miss <= (simple_miss)||(ro_miss);
p_tlb_err <= (s_pending)&&((!s_tlb_miss)&&(!s_tlb_hit));
pf_stb <= 1'b0;
last_ppage <= 0;
last_vpage <= 0;
last_tlb <= 0;
end else if ((!kernel_context)&&(r_pending)&&(!last_page_valid))
begin
last_tlb <= s_tlb_addr;
last_ppage <= ppage;
last_vpage <= vpage;
last_exe <= exe_flag;
last_ro <= ro_flag;
pf_stb <= 1'b1;
end else
pf_stb <= 1'b0;
 
pf_cachable <= cachable;
if ((!z_context)&&(r_pending))
begin
last_ppage <= tlb_pdata[s_tlb_addr];
last_vpage <= tlb_vdata[s_tlb_addr];
last_ro <= ro_flag;
pf_stb <= 1'b1;
end else
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)
last_page_valid <= (last_page_valid)
&&(r_context_word == i_wb_data[(LGCTXT-1):0]);
else if ((r_pending)&&(!z_context))
last_page_valid <= (s_tlb_hit)&&(!ro_miss);
initial status_word = 0;
always @(posedge i_clk)
if (i_reset)
status_word <= 0;
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) };
 
if (i_reset)
last_page_valid <= 1'b0;
initial last_page_valid = 1'b0;
always @(posedge i_clk)
if (i_reset)
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
 
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 o_cyc = 1'b0;
always @(posedge i_clk)
if (i_reset)
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));
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);
rtn_err <= (i_wbm_cyc)&&(i_err)&&(o_cyc);
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_we = (r_we);
assign o_rtn_stall = (i_wbm_cyc)&&(((r_pending)&&(!r_valid))||(i_stall));
assign o_rtn_miss = p_tlb_miss;
assign o_rtn_err = (rtn_err)||(p_tlb_err);
assign o_rtn_stall = (i_wbm_cyc)&&(
(o_rtn_err)
||((r_pending)&&(!r_valid))
||((o_stb)&&(i_stall))
||(miss_pending));
 
assign o_addr[(AW-1):0] = {(z_context)?
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_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 ...
//
assign pf_return_stb = pf_stb;
551,4 → 782,378
assign pf_return_v = last_vpage;
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
/ziptimer.v
45,7 → 45,7
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015,2017, Gisselquist Technology, LLC
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
69,15 → 69,17
////////////////////////////////////////////////////////////////////////////////
//
//
module ziptimer(i_clk, i_rst, i_ce,
`default_nettype none
//
module ziptimer(i_clk, i_reset, i_ce,
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,
o_wb_ack, o_wb_stall, o_wb_data,
o_int);
parameter BW = 32, VW = (BW-1), RELOADABLE=1;
input i_clk, i_rst, i_ce;
input wire i_clk, i_reset, i_ce;
// Wishbone inputs
input i_wb_cyc, i_wb_stb, i_wb_we;
input [(BW-1):0] i_wb_data;
input wire i_wb_cyc, i_wb_stb, i_wb_we;
input wire [(BW-1):0] i_wb_data;
// Wishbone outputs
output reg o_wb_ack;
output wire o_wb_stall;
88,31 → 90,34
reg r_running;
 
wire wb_write;
assign wb_write = ((i_wb_cyc)&&(i_wb_stb)&&(i_wb_we));
assign wb_write = ((i_wb_stb)&&(i_wb_we));
 
wire auto_reload;
wire [(VW-1):0] reload_value;
wire auto_reload;
wire [(VW-1):0] interval_count;
 
initial r_running = 1'b0;
always @(posedge i_clk)
if (i_rst)
if (i_reset)
r_running <= 1'b0;
else if (wb_write)
r_running <= (|i_wb_data[(VW-1):0]);
else if ((o_int)&&(~auto_reload))
else if ((r_zero)&&(!auto_reload))
r_running <= 1'b0;
 
generate
if (RELOADABLE != 0)
begin
reg r_auto_reload;
reg [(VW-1):0] r_reload_value;
reg r_auto_reload;
reg [(VW-1):0] r_interval_count;
 
initial r_auto_reload = 1'b0;
 
always @(posedge i_clk)
if (wb_write)
r_auto_reload <= (i_wb_data[(BW-1)]);
if (i_reset)
r_auto_reload <= 1'b0;
else if (wb_write)
r_auto_reload <= (i_wb_data[(BW-1)])
&&(|i_wb_data[(VW-1):0]);
 
assign auto_reload = r_auto_reload;
 
119,12 → 124,12
// If setting auto-reload mode, and the value to other
// than zero, set the auto-reload value
always @(posedge i_clk)
if ((wb_write)&&(i_wb_data[(BW-1)])&&(|i_wb_data[(VW-1):0]))
r_reload_value <= i_wb_data[(VW-1):0];
assign reload_value = r_reload_value;
if (wb_write)
r_interval_count <= i_wb_data[(VW-1):0];
assign interval_count = r_interval_count;
end else begin
assign auto_reload = 1'b0;
assign reload_value = 0;
assign interval_count = 0;
end endgenerate
 
 
131,27 → 136,44
reg [(VW-1):0] r_value;
initial r_value = 0;
always @(posedge i_clk)
if (wb_write)
if (i_reset)
r_value <= 0;
else if (wb_write)
r_value <= i_wb_data[(VW-1):0];
else if ((r_running)&&(i_ce)&&(~o_int))
r_value <= r_value + {(VW){1'b1}}; // r_value - 1;
else if ((r_running)&&(auto_reload)&&(o_int))
r_value <= reload_value;
else if ((i_ce)&&(r_running))
begin
if (!r_zero)
r_value <= r_value - 1'b1;
else if (auto_reload)
r_value <= interval_count;
end
 
reg r_zero = 1'b1;
always @(posedge i_clk)
if (i_reset)
r_zero <= 1'b1;
else if (wb_write)
r_zero <= (i_wb_data[(VW-1):0] == 0);
else if ((r_running)&&(i_ce))
begin
if (r_value == { {(VW-1){1'b0}}, 1'b1 })
r_zero <= 1'b1;
else if ((r_zero)&&(auto_reload))
r_zero <= 1'b0;
end
 
// Set the interrupt on our last tick, as we transition from one to
// zero.
initial o_int = 1'b0;
always @(posedge i_clk)
if (i_rst)
if ((i_reset)||(wb_write)||(!i_ce))
o_int <= 1'b0;
else if (i_ce)
o_int <= (r_running)&&(r_value == { {(VW-1){1'b0}}, 1'b1 });
else
o_int <= 1'b0;
else // if (i_ce)
o_int <= (r_value == { {(VW-1){1'b0}}, 1'b1 });
 
initial o_wb_ack = 1'b0;
always @(posedge i_clk)
o_wb_ack <= (i_wb_cyc)&&(i_wb_stb);
o_wb_ack <= (!i_reset)&&(i_wb_stb);
assign o_wb_stall = 1'b0;
 
generate
161,4 → 183,103
assign o_wb_data = { auto_reload, r_value };
endgenerate
 
// Make verilator happy
// verilator lint_off UNUSED
wire [32:0] unused;
assign unused = { i_wb_cyc, i_wb_data };
// verilator lint_on UNUSED
 
`ifdef FORMAL
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
initial assume(i_reset);
always @(*)
if (!f_past_valid)
assume(i_reset);
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
begin
assert(r_value == 0);
assert(r_running == 0);
assert(auto_reload == 0);
assert(r_zero == 1'b1);
end
 
 
always @(*)
assert(r_zero == (r_value == 0));
 
always @(*)
if (r_value != 0)
assert(r_running);
 
always @(*)
if (auto_reload)
assert(r_running);
 
always @(*)
if (!RELOADABLE)
assert(auto_reload == 0);
 
always @(*)
if (auto_reload)
assert(interval_count != 0);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(r_value)==0)
&&(!$past(wb_write))&&(!$past(auto_reload)))
assert(r_value == 0);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(wb_write))
&&($past(r_value)==0)&&($past(auto_reload)))
begin
if ($past(i_ce))
assert(r_value == interval_count);
else
assert(r_value == $past(r_value));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))
&&(!$past(wb_write))&&($past(r_value)!=0))
begin
if ($past(i_ce))
assert(r_value == $past(r_value)-1'b1);
else
assert(r_value == $past(r_value));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(wb_write)))
assert(r_value == $past(i_wb_data[(VW-1):0]));
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(wb_write))
&&(RELOADABLE)&&(|$past(i_wb_data[(VW-1):0])))
assert(auto_reload == $past(i_wb_data[(BW-1)]));
 
always @(posedge i_clk)
if (!(f_past_valid)||($past(i_reset)))
assert(!o_int);
else if (($past(wb_write))||(!$past(i_ce)))
assert(!o_int);
else
assert(o_int == ((r_running)&&(r_value == 0)));
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
assert(!o_wb_ack);
else if ($past(i_wb_stb))
assert(o_wb_ack);
 
always @(*)
assert(!o_wb_stall);
always @(*)
assert(o_wb_data[BW-1] == auto_reload);
always @(*)
assert(o_wb_data[VW-1:0] == r_value);
`endif
endmodule

powered by: WebSVN 2.1.0

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