diff --git a/docs/examples/fifo/fifo.sby b/docs/examples/fifo/fifo.sby
index 91cb3c5..ab063a9 100644
--- a/docs/examples/fifo/fifo.sby
+++ b/docs/examples/fifo/fifo.sby
@@ -1,6 +1,9 @@
 [tasks]
-cover
-prove
+prove_oss prove oss
+prove_tabby prove tabby
+cover_oss cover oss
+cover_tabby cover tabby
+prove_oss cover_oss : default
 
 [options]
 cover:
@@ -16,6 +19,7 @@ prove: abc pdr
 
 [script]
 read -sv fifo.sv
+tabby: read -define USE_VERIFIC=1
 read -formal top.sv
 prep -top fifo
 
diff --git a/docs/examples/fifo/top.sv b/docs/examples/fifo/top.sv
index 3e12601..f9ba475 100644
--- a/docs/examples/fifo/top.sv
+++ b/docs/examples/fifo/top.sv
@@ -108,14 +108,6 @@ module fifo (
                             || 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 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);
             w_full:  cover  (wen && !ren && count == MAX_DATA-1);
@@ -123,9 +115,7 @@ module fifo (
             w_empty: cover  (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
@@ -137,13 +127,36 @@ module fifo (
         end
     end
 
-    // assumptions
+`ifdef USE_VERIFIC
+    // if we have verific we can also do the following additional tests
     always @(posedge clk) begin
-        // data will change when writing (and only when writing) so we can line up reads with writes
-        assume ((wen && wdata != $past(wdata)) || (!wen && wdata == $past(wdata)));
-        // assume property (wen |=> wdata != $past(wdata));
-        // assume property (!wen |=> wdata == $past(wdata));
+        if (rst_n) begin
+            // read/write enables enable
+            ap_raddr2: assert property (ren |=> $changed(raddr));
+            ap_waddr2: assert property (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?
+            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
+            assume property (wen |=> $changed(wdata));
+            assume property (!wen |=> $stable(wdata));
+        end
     end
-`endif
+`else // !USE_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)));
+    end
+`endif // USE_VERIFIC
+
+`endif // FORMAL
 
 endmodule