mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-05 22:14:08 +00:00
Changes to reset
Active high. Removed init. Better over/underfill cover properties for verific. Moved basic cover statement to only be used when there is no verific. Other general tidy up. Also updated/fixed a couple minor things in newstart.rst.
This commit is contained in:
parent
a76286ed34
commit
cfa4352bae
|
@ -1,32 +1,36 @@
|
|||
// address generator/counter
|
||||
module addr_gen
|
||||
#( parameter MAX_DATA=16
|
||||
) ( input en, clk, rst_n,
|
||||
) ( input en, clk, rst,
|
||||
output reg [3:0] addr
|
||||
);
|
||||
initial addr <= 0;
|
||||
|
||||
// async reset
|
||||
// increment address when enabled
|
||||
always @(posedge clk or negedge rst_n)
|
||||
if (~rst_n)
|
||||
always @(posedge clk or posedge rst)
|
||||
if (rst)
|
||||
addr <= 0;
|
||||
else if (en)
|
||||
else if (en) begin
|
||||
if (addr == MAX_DATA-1)
|
||||
addr <= 0;
|
||||
else
|
||||
addr <= addr + 1;
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Define our top level fifo entity
|
||||
module fifo
|
||||
#( parameter MAX_DATA=16
|
||||
) ( input wen, ren, clk, rst_n,
|
||||
) ( input wen, ren, clk, rst,
|
||||
input [7:0] wdata,
|
||||
output [7:0] rdata,
|
||||
output [4:0] count,
|
||||
output full, empty
|
||||
);
|
||||
wire wskip, rskip;
|
||||
reg [4:0] data_count;
|
||||
|
||||
// fifo storage
|
||||
// async read, sync write
|
||||
wire [3:0] waddr, raddr;
|
||||
|
@ -42,7 +46,7 @@ module fifo
|
|||
fifo_writer (
|
||||
.en (wen || wskip),
|
||||
.clk (clk ),
|
||||
.rst_n (rst_n),
|
||||
.rst (rst),
|
||||
.addr (waddr)
|
||||
);
|
||||
|
||||
|
@ -50,16 +54,15 @@ module fifo
|
|||
fifo_reader (
|
||||
.en (ren || rskip),
|
||||
.clk (clk ),
|
||||
.rst_n (rst_n),
|
||||
.rst (rst),
|
||||
.addr (raddr)
|
||||
);
|
||||
|
||||
// status signals
|
||||
reg [4:0] data_count;
|
||||
initial data_count <= 0;
|
||||
|
||||
always @(posedge clk or negedge rst_n) begin
|
||||
if (~rst_n)
|
||||
always @(posedge clk or posedge rst) begin
|
||||
if (rst)
|
||||
data_count <= 0;
|
||||
else if (wen && !ren && data_count < MAX_DATA)
|
||||
data_count <= data_count + 1;
|
||||
|
@ -68,11 +71,10 @@ module fifo
|
|||
end
|
||||
|
||||
assign full = data_count == MAX_DATA;
|
||||
assign empty = (data_count == 0) && rst_n;
|
||||
assign empty = (data_count == 0) && ~rst;
|
||||
assign count = data_count;
|
||||
|
||||
// overflow protection
|
||||
wire wskip, rskip;
|
||||
`ifndef NO_FULL_SKIP
|
||||
// write while full => overwrite oldest data, move read pointer
|
||||
assign rskip = wen && !ren && data_count >= MAX_DATA;
|
||||
|
@ -90,19 +92,10 @@ module fifo
|
|||
? waddr - raddr
|
||||
: waddr + MAX_DATA - raddr;
|
||||
|
||||
reg init = 0;
|
||||
always @(posedge clk) begin
|
||||
if (rst_n)
|
||||
init <= 1;
|
||||
// if init is low we don't care about the value of rst_n
|
||||
// if init is high (rst_n has ben high), then rst_n must remain high
|
||||
assume (!init || rst_n);
|
||||
end
|
||||
|
||||
// tests
|
||||
always @(posedge clk) begin
|
||||
if (rst_n) begin
|
||||
// waddr and raddr can only be non zero if reset is high
|
||||
if (~rst) begin
|
||||
// waddr and raddr can only be non zero if reset is low
|
||||
w_nreset: cover (waddr || raddr);
|
||||
|
||||
// count never more than max
|
||||
|
@ -132,49 +125,44 @@ module fifo
|
|||
w_full: cover (wen && !ren && count == MAX_DATA-1);
|
||||
a_empty: assert (!empty || count == 0);
|
||||
w_empty: cover (ren && !wen && count == 1);
|
||||
|
||||
// can we corrupt our data?
|
||||
w_overfill: cover ($past(rskip) && raddr);
|
||||
w_underfill: cover ($past(wskip) && waddr);
|
||||
end else begin
|
||||
// waddr and raddr are zero while reset is low
|
||||
a_reset: assert (!waddr && !raddr);
|
||||
w_reset: cover (~rst_n);
|
||||
|
||||
// outputs are zero while reset is low
|
||||
// reading/writing non zero values
|
||||
w_nzero_write: cover (wen && wdata);
|
||||
w_nzero_read: cover (ren && rdata);
|
||||
end else begin
|
||||
// waddr and raddr are zero while reset is high
|
||||
a_reset: assert (!waddr && !raddr);
|
||||
w_reset: cover (rst);
|
||||
|
||||
// outputs are zero while reset is high
|
||||
a_zero_out: assert (!empty && !full && !count);
|
||||
end
|
||||
end
|
||||
|
||||
`ifdef VERIFIC
|
||||
// if we have verific we can also do the following additional tests
|
||||
always @(posedge clk) begin
|
||||
if (rst_n) begin
|
||||
// read/write enables enable
|
||||
ap_raddr2: assert property (ren |=> $changed(raddr));
|
||||
ap_waddr2: assert property (wen |=> $changed(waddr));
|
||||
// read/write enables enable
|
||||
ap_raddr2: assert property (@(posedge clk) disable iff (rst) ren |=> $changed(raddr));
|
||||
ap_waddr2: assert property (@(posedge clk) disable iff (rst) wen |=> $changed(waddr));
|
||||
|
||||
// read/write needs enable UNLESS full/empty
|
||||
ap_raddr3: assert property (!ren && !full |=> $stable(raddr));
|
||||
ap_waddr3: assert property (!wen && !empty |=> $stable(waddr));
|
||||
|
||||
// can we corrupt our data?
|
||||
// these should already be covered by ap_{r,w}addr2
|
||||
ap_overfill: assert property (wen && full |=> $changed(raddr));
|
||||
ap_underfill: assert property (ren && empty |=> $changed(waddr));
|
||||
|
||||
// change data when writing (and only when writing) so we can line
|
||||
// up reads with writes
|
||||
//TODO: this but with a cover statement
|
||||
// assume property (wen |=> $changed(wdata));
|
||||
// assume property (!wen |=> $stable(wdata));
|
||||
end
|
||||
end
|
||||
// read/write needs enable UNLESS full/empty
|
||||
ap_raddr3: assert property (@(posedge clk) disable iff (rst) !ren && !full |=> $stable(raddr));
|
||||
ap_waddr3: assert property (@(posedge clk) disable iff (rst) !wen && !empty |=> $stable(waddr));
|
||||
|
||||
// can we corrupt our data?
|
||||
w_underfill: cover property (@(posedge clk) disable iff (rst) !wen |=> $changed(waddr));
|
||||
// look for an overfill where the value in memory changes
|
||||
let d_change = (wdata != rdata);
|
||||
w_overfill: cover property (@(posedge clk) disable iff (rst) !ren && d_change |=> $changed(raddr));
|
||||
`else // !VERIFIC
|
||||
// without verific we are more limited in describing the above assumption
|
||||
always @(posedge clk) begin
|
||||
assume ((wen && wdata != $past(wdata))
|
||||
|| (!wen && wdata == $past(wdata)));
|
||||
if (~rst) begin
|
||||
// this is less reliable because $past() can sometimes give false
|
||||
// positives in the first cycle
|
||||
w_overfill: cover ($past(rskip) && raddr);
|
||||
w_underfill: cover ($past(wskip) && waddr);
|
||||
|
||||
end
|
||||
end
|
||||
`endif // VERIFIC
|
||||
|
||||
|
|
|
@ -2,33 +2,37 @@
|
|||
module addr_gen
|
||||
#( parameter MAX_DATA=16,
|
||||
parameter ADDR_BITS=5
|
||||
) ( input en, clk, rst_n,
|
||||
) ( input en, clk, rst,
|
||||
output reg [ADDR_BITS-1:0] addr
|
||||
);
|
||||
initial addr <= 0;
|
||||
|
||||
// async reset
|
||||
// increment address when enabled
|
||||
always @(posedge clk or negedge rst_n)
|
||||
if (~rst_n)
|
||||
always @(posedge clk or posedge rst)
|
||||
if (rst)
|
||||
addr <= 0;
|
||||
else if (en)
|
||||
else if (en) begin
|
||||
if (addr == MAX_DATA-1)
|
||||
addr <= 0;
|
||||
else
|
||||
addr <= addr + 1;
|
||||
end
|
||||
endmodule
|
||||
|
||||
// Define our top level fifo entity
|
||||
module fifo
|
||||
#( parameter MAX_DATA=16,
|
||||
parameter ADDR_BITS=5
|
||||
) ( input wen, ren, clk, rst_n,
|
||||
) ( input wen, ren, clk, rst,
|
||||
input [7:0] wdata,
|
||||
output [7:0] rdata,
|
||||
output [ADDR_BITS:0] count,
|
||||
output full, empty
|
||||
);
|
||||
wire wskip, rskip;
|
||||
reg [ADDR_BITS:0] data_count;
|
||||
|
||||
// fifo storage
|
||||
// async read, sync write
|
||||
wire [ADDR_BITS-1:0] waddr, raddr;
|
||||
|
@ -44,7 +48,7 @@ module fifo
|
|||
fifo_writer (
|
||||
.en (wen || wskip),
|
||||
.clk (clk ),
|
||||
.rst_n (rst_n),
|
||||
.rst (rst),
|
||||
.addr (waddr)
|
||||
);
|
||||
|
||||
|
@ -52,16 +56,15 @@ module fifo
|
|||
fifo_reader (
|
||||
.en (ren || rskip),
|
||||
.clk (clk ),
|
||||
.rst_n (rst_n),
|
||||
.rst (rst),
|
||||
.addr (raddr)
|
||||
);
|
||||
|
||||
// status signals
|
||||
reg [ADDR_BITS:0] data_count;
|
||||
initial data_count <= 0;
|
||||
|
||||
always @(posedge clk or negedge rst_n) begin
|
||||
if (~rst_n)
|
||||
always @(posedge clk or posedge rst) begin
|
||||
if (rst)
|
||||
data_count <= 0;
|
||||
else if (wen && !ren && data_count < MAX_DATA)
|
||||
data_count <= data_count + 1;
|
||||
|
@ -70,11 +73,10 @@ module fifo
|
|||
end
|
||||
|
||||
assign full = data_count == MAX_DATA;
|
||||
assign empty = (data_count == 0) && rst_n;
|
||||
assign empty = (data_count == 0) && ~rst;
|
||||
assign count = data_count;
|
||||
|
||||
// overflow protection
|
||||
wire wskip, rskip;
|
||||
`ifndef NO_FULL_SKIP
|
||||
// write while full => overwrite oldest data, move read pointer
|
||||
assign rskip = wen && !ren && data_count >= MAX_DATA;
|
||||
|
@ -89,22 +91,13 @@ module fifo
|
|||
// observers
|
||||
wire [ADDR_BITS:0] addr_diff;
|
||||
assign addr_diff = waddr >= raddr
|
||||
? waddr - raddr
|
||||
: waddr + MAX_DATA - raddr;
|
||||
|
||||
reg init = 0;
|
||||
always @(posedge clk) begin
|
||||
if (rst_n)
|
||||
init <= 1;
|
||||
// if init is low we don't care about the value of rst_n
|
||||
// if init is high (rst_n has ben high), then rst_n must remain high
|
||||
assume (!init || rst_n);
|
||||
end
|
||||
? waddr - raddr
|
||||
: waddr + MAX_DATA - raddr;
|
||||
|
||||
// tests
|
||||
always @(posedge clk) begin
|
||||
if (rst_n) begin
|
||||
// waddr and raddr can only be non zero if reset is high
|
||||
if (~rst) begin
|
||||
// waddr and raddr can only be non zero if reset is low
|
||||
w_nreset: cover (waddr || raddr);
|
||||
|
||||
// count never more than max
|
||||
|
@ -134,35 +127,43 @@ module fifo
|
|||
w_full: cover (wen && !ren && count == MAX_DATA-1);
|
||||
a_empty: assert (!empty || count == 0);
|
||||
w_empty: cover (ren && !wen && count == 1);
|
||||
|
||||
// can we corrupt our data?
|
||||
w_overfill: cover ($past(rskip) && raddr);
|
||||
w_underfill: cover ($past(wskip) && waddr);
|
||||
end else begin
|
||||
// waddr and raddr are zero while reset is low
|
||||
a_reset: assert (!waddr && !raddr);
|
||||
w_reset: cover (~rst_n);
|
||||
|
||||
// outputs are zero while reset is low
|
||||
// reading/writing non zero values
|
||||
w_nzero_write: cover (wen && wdata);
|
||||
w_nzero_read: cover (ren && rdata);
|
||||
end else begin
|
||||
// waddr and raddr are zero while reset is high
|
||||
a_reset: assert (!waddr && !raddr);
|
||||
w_reset: cover (rst);
|
||||
|
||||
// outputs are zero while reset is high
|
||||
a_zero_out: assert (!empty && !full && !count);
|
||||
end
|
||||
end
|
||||
|
||||
`ifdef VERIFIC
|
||||
// if we have verific we can also do the following additional tests
|
||||
always @(posedge clk) begin
|
||||
if (rst_n) begin
|
||||
// read/write enables enable
|
||||
ap_raddr2: assert property (ren |=> $changed(raddr));
|
||||
ap_waddr2: assert property (wen |=> $changed(waddr));
|
||||
// read/write enables enable
|
||||
ap_raddr2: assert property (@(posedge clk) disable iff (rst) ren |=> $changed(raddr));
|
||||
ap_waddr2: assert property (@(posedge clk) disable iff (rst) wen |=> $changed(waddr));
|
||||
|
||||
// read/write needs enable UNLESS full/empty
|
||||
ap_raddr3: assert property (@(posedge clk) disable iff (rst) !ren && !full |=> $stable(raddr));
|
||||
ap_waddr3: assert property (@(posedge clk) disable iff (rst) !wen && !empty |=> $stable(waddr));
|
||||
|
||||
// can we corrupt our data?
|
||||
w_underfill: cover property (@(posedge clk) disable iff (rst) !wen |=> $changed(waddr));
|
||||
// look for an overfill where the value in memory changes
|
||||
let d_change = (wdata != rdata);
|
||||
w_overfill: cover property (@(posedge clk) disable iff (rst) !ren && d_change |=> $changed(raddr));
|
||||
`else // !VERIFIC
|
||||
always @(posedge clk) begin
|
||||
if (~rst) begin
|
||||
// this is less reliable because $past() can sometimes give false
|
||||
// positives in the first cycle
|
||||
w_overfill: cover ($past(rskip) && raddr);
|
||||
w_underfill: cover ($past(wskip) && waddr);
|
||||
|
||||
// read/write needs enable UNLESS full/empty
|
||||
ap_raddr3: assert property (!ren && !full |=> $stable(raddr));
|
||||
ap_waddr3: assert property (!wen && !empty |=> $stable(waddr));
|
||||
|
||||
// can we corrupt our data?
|
||||
ap_overfill: assert property (wen && full |=> $changed(raddr));
|
||||
ap_underfill: assert property (ren && empty |=> $changed(waddr));
|
||||
end
|
||||
end
|
||||
`endif // VERIFIC
|
||||
|
|
|
@ -131,7 +131,7 @@ adjustments to code and rerunning tests to validate.
|
|||
|
||||
sby -f fifo.sby nofullskip
|
||||
|
||||
The noskip task disables the code shown below. Because the count signal has
|
||||
The nofullskip task disables the code shown below. Because the count signal has
|
||||
been written such that it cannot exceed MAX_DATA, removing this code will lead
|
||||
to the ``a_count_diff`` assertion failing. Without this assertion, there is no
|
||||
guarantee that data will be read in the same order it was written should an
|
||||
|
@ -143,13 +143,12 @@ overflow occur and the oldest data be written.
|
|||
:end-at: endif
|
||||
:lines: 1-5,9
|
||||
|
||||
The last few lines of output for the noskip task should be similar to the
|
||||
The last few lines of output for the nofullskip task should be similar to the
|
||||
following:
|
||||
|
||||
.. code-block:: text
|
||||
|
||||
SBY [fifo_nofullskip] engine_0.basecase: ## Assert failed in fifo: a_count_diff
|
||||
SBY [fifo_nofullskip] engine_0.basecase: ## Assert failed in fifo: ap_underfill
|
||||
SBY [fifo_nofullskip] engine_0.basecase: ## Writing trace to VCD file: engine_0/trace.vcd
|
||||
SBY [fifo_nofullskip] engine_0.basecase: ## Writing trace to Verilog testbench: engine_0/trace_tb.v
|
||||
SBY [fifo_nofullskip] engine_0.basecase: ## Writing trace to constraints file: engine_0/trace.smtc
|
||||
|
@ -162,7 +161,7 @@ following:
|
|||
SBY [fifo_nofullskip] summary: engine_0 (smtbmc boolector) returned FAIL for basecase
|
||||
SBY [fifo_nofullskip] summary: counterexample trace: fifo_nofullskip/engine_0/trace.vcd
|
||||
SBY [fifo_nofullskip] DONE (FAIL, rc=2)
|
||||
SBY The following tasks failed: ['noskip']
|
||||
SBY The following tasks failed: ['nofullskip']
|
||||
|
||||
Using the ``noskip.gtkw`` file provided, use the below command to examine the
|
||||
error trace.
|
||||
|
@ -189,16 +188,16 @@ Searching the file for ``w_underfill`` will reveal the below.
|
|||
|
||||
.. code-block:: text
|
||||
|
||||
$ grep "w_underfill" fifo_cover/logfile.txt -A 1
|
||||
$ grep "w_underfill" fifo_cover/logfile.txt -A 2
|
||||
SBY [fifo_cover] engine_0: ## Reached cover statement at w_underfill in step 2.
|
||||
SBY [fifo_cover] engine_0: ## Writing trace to VCD file: engine_0/trace2.vcd
|
||||
SBY [fifo_cover] engine_0: ## Writing trace to VCD file: engine_0/trace4.vcd
|
||||
|
||||
We can then run gtkwave with the trace file indicated to see the correct
|
||||
operation as in the image below. When the buffer is empty, a read with no write
|
||||
will result in the ``wksip`` signal going high, incrementing *both* read and
|
||||
write addresses and avoiding underflow.
|
||||
|
||||
gtkwave fifo_cover/engine_0/trace2.vcd noskip.gtkw
|
||||
gtkwave fifo_cover/engine_0/trace4.vcd noskip.gtkw
|
||||
|
||||
.. image:: media/gtkwave_coverskip.png
|
||||
|
||||
|
|
Loading…
Reference in a new issue