diff --git a/docs/examples/fifo/fifo.sby b/docs/examples/fifo/fifo.sby index ab063a9..62e9d85 100644 --- a/docs/examples/fifo/fifo.sby +++ b/docs/examples/fifo/fifo.sby @@ -1,7 +1,8 @@ [tasks] prove_oss prove oss -prove_tabby prove tabby +noskip prove oss cover_oss cover oss +prove_tabby prove tabby cover_tabby cover tabby prove_oss cover_oss : default @@ -20,6 +21,7 @@ prove: abc pdr [script] read -sv fifo.sv tabby: read -define USE_VERIFIC=1 +noskip: read -define NOSKIP=1 read -formal top.sv prep -top fifo diff --git a/docs/examples/fifo/top.sv b/docs/examples/fifo/top.sv index f9ba475..f5eec51 100644 --- a/docs/examples/fifo/top.sv +++ b/docs/examples/fifo/top.sv @@ -57,10 +57,15 @@ module fifo ( assign empty = (data_count == 0) && rst_n; assign count = data_count; +`ifndef NOSKIP // write while full => overwrite oldest data, move read pointer assign rskip = wen && !ren && data_count >= MAX_DATA; // read while empty => read invalid data, keep write pointer in sync assign wskip = ren && !wen && data_count == 0; +`else + assign rskip = 0; + assign wskip = 0; +`endif // NOSKIP `ifdef FORMAL // observers