From 48d846d529485b0b5a02774609bc1530e482c236 Mon Sep 17 00:00:00 2001 From: KrystalDelusion Date: Mon, 2 May 2022 12:20:27 +1200 Subject: [PATCH] Adjusting for use with OSS i.e. doesn't use concurrent assertions --- docs/examples/fifo/top.sv | 108 +++++++++++++++++++------------------- 1 file changed, 55 insertions(+), 53 deletions(-) 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