Adding noskip task

Demonstrate failing model check by disabling rskip and wskip.

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
 

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