mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Now actually fills up properly

Browse source 
As opposed to only storing MAX-1
This commit is contained in:
KrystalDelusion 2022-05-02 12:34:57 +12:00
parent 48d846d529
commit 60de15293d
1 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
docs/examples/fifo/top.sv
View file

@ -3,13 +3,13 @@ module fifo (
input wen, ren, clk, rst_n, input wen, ren, clk, rst_n,
input [7:0] wdata, input [7:0] wdata,
output [7:0] rdata, output [7:0] rdata,
output [3:0] count, output [4:0] count,
output full, empty output full, empty
); );
parameter MAX_DATA = 16; parameter MAX_DATA = 16;
// internals // internals
reg [3:0] data_count; reg [4:0] data_count;
initial begin initial begin
data_count <= 0; data_count <= 0;
end end
@ -45,7 +45,7 @@ module fifo (
always @(posedge clk or negedge rst_n) begin always @(posedge clk or negedge rst_n) begin
if (~rst_n) if (~rst_n)
data_count <= 0; data_count <= 0;
else if (wen && !ren && data_count < MAX_DATA-1) else if (wen && !ren && data_count < MAX_DATA)
data_count <= data_count + 1; data_count <= data_count + 1;
else if (ren && !wen && data_count > 0) else if (ren && !wen && data_count > 0)
data_count <= data_count - 1; data_count <= data_count - 1;
@ -53,12 +53,12 @@ module fifo (
data_count <= data_count; data_count <= data_count;
end end
assign full = data_count == MAX_DATA-1; assign full = data_count == MAX_DATA;
assign empty = (data_count == 0) && rst_n; assign empty = (data_count == 0) && rst_n;
assign count = data_count; assign count = data_count;
// write while full => overwrite oldest data, move read pointer // write while full => overwrite oldest data, move read pointer
assign rskip = wen && !ren && data_count >= MAX_DATA-1; assign rskip = wen && !ren && data_count >= MAX_DATA;
// read while empty => read invalid data, keep write pointer in sync // read while empty => read invalid data, keep write pointer in sync
assign wskip = ren && !wen && data_count == 0; assign wskip = ren && !wen && data_count == 0;
@ -78,11 +78,12 @@ module fifo (
// count never less than zero, or more than max // count never less than zero, or more than max
a_uflow: assert (count >= 0); a_uflow: assert (count >= 0);
a_uflow2: assert (raddr >= 0); a_uflow2: assert (raddr >= 0);
a_oflow: assert (count < MAX_DATA); a_oflow: assert (count <= MAX_DATA);
a_oflow2: assert (waddr < MAX_DATA); a_oflow2: assert (waddr < MAX_DATA);
// count should be equal to the difference between writer and reader address // count should be equal to the difference between writer and reader address
a_count_diff: assert (count == addr_diff); a_count_diff: assert (count == addr_diff
|| count == MAX_DATA && addr_diff == 0);
// count should only be able to increase or decrease by 1 // count should only be able to increase or decrease by 1
a_counts: assert (count == 0 a_counts: assert (count == 0
@ -107,8 +108,8 @@ module fifo (
// ap_waddr3: assert property (!wen && !empty |=> waddr == $past(waddr)); // ap_waddr3: assert property (!wen && !empty |=> waddr == $past(waddr));
// full and empty work as expected // full and empty work as expected
a_full: assert (!full || full && count == MAX_DATA-1); a_full: assert (!full || full && count == MAX_DATA);
w_full: cover (wen && !ren && count == MAX_DATA-2); w_full: cover (wen && !ren && count == MAX_DATA-1);
a_empty: assert (!empty || empty && count == 0); a_empty: assert (!empty || empty && count == 0);
w_empty: cover property (ren && !wen && count == 1); w_empty: cover property (ren && !wen && count == 1);