Permalink
Browse files

Initial formal FIFO verification support. Bugs found in the process--…

…fixed
  • Loading branch information...
ZipCPU committed Oct 17, 2017
1 parent 2c2130d commit 01efb009ce963b536213f5e8e695acf1c93c2d84
Showing with 106 additions and 16 deletions.
  1. +106 −16 rtl/smplfifo.v
View
@@ -35,16 +35,17 @@
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
//
module smplfifo(i_clk, i_rst, i_wr, i_data,
o_empty_n, i_rd, o_data, o_status, o_err);
parameter BW=12; // Byte/data width
parameter [4:0] LGFLEN=9; // 512 samples
parameter RXFIFO=1'b1;
input i_clk, i_rst;
input i_wr;
input [(BW-1):0] i_data;
input wire i_clk, i_rst;
input wire i_wr;
input wire [(BW-1):0] i_data;
output wire o_empty_n; // True if something is in FIFO
input i_rd;
input wire i_rd;
output wire [(BW-1):0] o_data;
output wire [15:0] o_status;
output wire o_err;
@@ -110,7 +111,7 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
if (i_rst)
will_underflow <= 1'b1;
else if (i_wr)
will_underflow <= (will_underflow)&&(i_rd);
will_underflow <= 1'b0;
else if (i_rd)
will_underflow <= (will_underflow)||(w_last_plus_one == r_first);
else
@@ -124,6 +125,7 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
// reg r_unfl;
// initial r_unfl = 1'b0;
initial r_last = 0;
initial r_next = { {(LGFLEN-1){1'b0}}, 1'b1 };
always @(posedge i_clk)
if (i_rst)
begin
@@ -132,7 +134,7 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
// r_unfl <= 1'b0;
end else if (i_rd)
begin
if ((i_wr)||(!will_underflow)) // (r_first != r_last)
if (!will_underflow) // (r_first != r_last)
begin
r_last <= r_next;
r_next <= r_last +{{(LGFLEN-2){1'b0}},2'b10};
@@ -175,10 +177,10 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
r_empty_n <= 1'b0;
else casez({i_wr, i_rd, will_underflow})
3'b00?: r_empty_n <= (r_first != r_last);
3'b11?: r_empty_n <= (r_first != r_last);
3'b10?: r_empty_n <= 1'b1;
3'b010: r_empty_n <= (r_first != w_last_plus_one);
// 3'b001: r_empty_n <= 1'b0;
3'b10?: r_empty_n <= 1'b1;
3'b110: r_empty_n <= (r_first != r_last);
3'b111: r_empty_n <= 1'b1;
default: begin end
endcase
@@ -193,6 +195,7 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
//
// Adjust for these differences here.
reg [(LGFLEN-1):0] r_fill;
initial r_fill = 0;
always @(posedge i_clk)
begin
// Calculate the number of elements in our FIFO
@@ -202,10 +205,11 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
// another context.
if (i_rst)
r_fill <= 0;
else case({(i_wr)&&(!will_overflow), (i_rd)&&(!will_underflow)})
2'b01: r_fill <= r_first - r_next;
2'b10: r_fill <= r_first - r_last + 1'b1;
default: r_fill <= r_first - r_last;
else casez({(i_wr), (!will_overflow), (i_rd)&&(!will_underflow)})
3'b0?1: r_fill <= r_first - r_next;
3'b110: r_fill <= r_first - r_last + 1'b1;
3'b1?1: r_fill <= r_first - r_last;
default: r_fill <= r_first - r_last;
endcase
end
@@ -215,6 +219,7 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
wire [4:0] lglen;
assign lglen = LGFLEN;
wire w_half_full;
wire [13:0] w_fill;
generate
if (LGFLEN > 14)
@@ -228,7 +233,6 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
end
endgenerate
wire w_half_full;
assign w_half_full = r_fill[(LGFLEN-1)];
assign o_status = {
@@ -244,5 +248,91 @@ module smplfifo(i_clk, i_rst, i_wr, i_data,
};
assign o_empty_n = r_empty_n;
`ifdef FORMAL
`ifdef SMPLFIFO
`define ASSUME assume
`else
`define ASSUME assert
`endif
//
// Assumptions about our input(s)
//
//
reg f_past_valid, f_last_clk;
initial restrict(i_rst);
always @($global_clock)
begin
restrict(i_clk == !f_last_clk);
f_last_clk <= i_clk;
if (!$rose(i_clk))
begin
`ASSUME($stable(i_rst));
`ASSUME($stable(i_wr));
`ASSUME($stable(i_data));
`ASSUME($stable(i_rd));
end
end
//
// Underflows are a very real possibility, should the user wish to read from this
// FIFO while it is empty. Our parent module will need to deal with this.
//
// always @(posedge i_clk)
// `ASSUME((!will_underflow)||(!i_rd)||(i_rst));
//
// Assertions about our outputs
//
//
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
wire [(LGFLEN-1):0] f_fill, f_next;
assign f_fill = r_first - r_last;
assign f_next = r_last + 1'b1;
always @(posedge i_clk)
begin
assert(f_fill == r_fill);
if (f_fill == 0)
begin
assert(will_underflow);
assert(!o_empty_n);
end else begin
assert(!will_underflow);
assert(o_empty_n);
end
if (f_fill == {(LGFLEN){1'b1}})
assert(will_overflow);
else
assert(!will_overflow);
assert(r_next == f_next);
end
always @(posedge i_clk)
if (f_past_valid)
begin
if ($past(i_rst))
assert(!o_err);
else begin
// No underflow detection in this core
//
// if (($past(i_rd))&&($past(r_fill == 0)))
// assert(o_err);
//
// We do, though, have overflow detection
if (($past(i_wr))&&(!$past(i_rd))
&&($past(will_overflow)))
assert(o_err);
end
end
`endif
endmodule

0 comments on commit 01efb00

Please sign in to comment.