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 |