diff --git a/docs/examples/fifo/top.sv b/docs/examples/fifo/top.sv
index 5e06692..e153a57 100644
--- a/docs/examples/fifo/top.sv
+++ b/docs/examples/fifo/top.sv
@@ -54,7 +54,7 @@ module fifo (
end
assign full = data_count == MAX_DATA-1;
- assign empty = data_count == 0;
+ assign empty = (data_count == 0) && rst_n;
assign count = data_count;
// write while full => overwrite oldest data, move read pointer
@@ -65,72 +65,74 @@ module fifo (
`ifdef FORMAL
// observers
wire [4:0] addr_diff;
- assign addr_diff = waddr >= raddr ? waddr - raddr : waddr + MAX_DATA - raddr;
-
- // tests should not run through a reset
- // not entirely sure what this actually does
- default clocking @(posedge clk); endclocking
- default disable iff (~rst_n);
+ assign addr_diff = waddr >= raddr
+ ? waddr - raddr
+ : waddr + MAX_DATA - raddr;
// tests
- always @(posedge clk or negedge rst_n) begin
- // waddr and raddr are zero while reset is low
- ap_reset: assert property (~rst_n |=> !waddr && !raddr);
- wp_reset: cover property (rst_n);
+ always @(posedge clk) begin
+ if (rst_n) begin
+ // waddr and raddr can only be non zero if reset is high
+ w_nreset: cover (waddr || raddr);
- // waddr and raddr can only be non zero if reset is high
- ap_nreset: assert property (waddr || raddr |=> $past(rst_n));
- wp_nreset: cover property (waddr || raddr);
+ // count never less than zero, or more than max
+ a_uflow: assert (count >= 0);
+ a_uflow2: assert (raddr >= 0);
+ a_oflow: assert (count < MAX_DATA);
+ a_oflow2: assert (waddr < MAX_DATA);
- // count never less than zero, or more than max
- ap_uflow: assert (count >= 0);
- ap_uflow2: assert (raddr >= 0);
- ap_oflow: assert (count < MAX_DATA);
- ap_oflow2: assert (waddr < MAX_DATA);
+ // count should be equal to the difference between writer and reader address
+ a_count_diff: assert (count == addr_diff);
- // count should be equal to the difference between writer and reader address
- ap_count_diff: assert (count == addr_diff);
+ // count should only be able to increase or decrease by 1
+ a_counts: assert (count == 0
+ || count == $past(count)
+ || count == $past(count) + 1
+ || count == $past(count) - 1);
- // count should only be able to increase or decrease by 1
- ap_counts: assert (count == 0
- || count == $past(count)
- || count == $past(count) + 1
- || count == $past(count) - 1);
+ // read/write addresses can only increase (or stay the same)
+ a_raddr: assert (raddr == 0
+ || raddr == $past(raddr)
+ || raddr == $past(raddr + 1));
+ a_waddr: assert (waddr == 0
+ || waddr == $past(waddr)
+ || waddr == $past(waddr + 1));
- // read/write addresses can only increase (or stay the same)
- ap_raddr: assert (raddr == 0
- || raddr == $past(raddr)
- || raddr == $past(raddr + 1));
- ap_waddr: assert (waddr == 0
- || waddr == $past(waddr)
- || waddr == $past(waddr + 1));
+ // read/write enables enable
+ // ap_raddr2: assert property (ren |=> raddr != $past(raddr));
+ // ap_waddr2: assert property (wen |=> waddr != $past(waddr));
- // read/write enables enable
- ap_raddr2: assert property (ren |=> raddr != $past(raddr));
- ap_waddr2: assert property (wen |=> waddr != $past(waddr));
+ // read/write needs enable UNLESS full/empty
+ // ap_raddr3: assert property (!ren && !full |=> raddr == $past(raddr));
+ // ap_waddr3: assert property (!wen && !empty |=> waddr == $past(waddr));
- // read/write needs enable UNLESS full/empty
- ap_raddr3: assert property (!ren && !full |=> raddr == $past(raddr));
- ap_waddr3: assert property (!wen && !empty |=> waddr == $past(waddr));
+ // full and empty work as expected
+ a_full: assert (!full || full && count == MAX_DATA-1);
+ w_full: cover (wen && !ren && count == MAX_DATA-2);
+ a_empty: assert (!empty || empty && count == 0);
+ w_empty: cover property (ren && !wen && count == 1);
+
+ // can we corrupt our data?
+ // ap_overfill: assert property (wen && full |=> raddr != $past(raddr));
+ w_overfill: cover ($past(rskip) && raddr);
+ // ap_underfill: assert property (ren && empty |=> waddr != $past(waddr));
+ 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);
- // full and empty work as expected
- ap_full: assert property (wen && !ren && count == MAX_DATA-2 |=> full);
- wp_full: cover property (wen && !ren && count == MAX_DATA-2);
- ap_empty: assert property (ren && !wen && count == 1 |=> empty);
- wp_empty: cover property (ren && !wen && count == 1);
-
- // can we corrupt our data?
- ap_overfill: assert property (wen && full |=> raddr != $past(raddr));
- wp_overfill: cover property (wen && full);
- ap_underfill: assert property (ren && empty |=> waddr != $past(waddr));
- wp_underfill: cover property (ren && empty);
+ // outputs are zero while reset is low
+ a_zero_out: assert (!empty && !full && !count);
+ end
end
// assumptions
- always @(posedge clk or negedge rst_n) begin
+ always @(posedge clk) begin
// data will change when writing (and only when writing) so we can line up reads with writes
- assume property (wen |=> wdata != $past(wdata));
- assume property (!wen |=> wdata == $past(wdata));
+ assume ((wen && wdata != $past(wdata)) || (!wen && wdata == $past(wdata)));
+ // assume property (wen |=> wdata != $past(wdata));
+ // assume property (!wen |=> wdata == $past(wdata));
end
`endif