From 1d4716a5f9e701814dad0d928b753b7d752f83b6 Mon Sep 17 00:00:00 2001
From: KrystalDelusion <krystinedawn@yosyshq.com>
Date: Tue, 9 Aug 2022 11:29:19 +1200
Subject: [PATCH] Add noverific task to test the non verific code

Mostly for CI to ensure fallback code still functions as intended.a
Also reverted the change in the grep command to 1 line after.
---
 docs/examples/fifo/fifo.sby        | 2 ++
 docs/examples/fifo/fifo.sh         | 2 +-
 docs/examples/fifo/golden/fifo.sby | 2 ++
 docs/source/newstart.rst           | 4 +++-
 4 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/docs/examples/fifo/fifo.sby b/docs/examples/fifo/fifo.sby
index 22ebcdd..4ca4bc6 100644
--- a/docs/examples/fifo/fifo.sby
+++ b/docs/examples/fifo/fifo.sby
@@ -2,6 +2,7 @@
 basic bmc
 nofullskip prove
 cover
+noverific cover
 basic cover : default
 
 [options]
@@ -20,6 +21,7 @@ smtbmc boolector
 
 [script]
 nofullskip: read -define NO_FULL_SKIP=1
+noverific: read -noverific
 read -formal fifo.sv
 prep -top fifo
 
diff --git a/docs/examples/fifo/fifo.sh b/docs/examples/fifo/fifo.sh
index 74f05c1..1024222 100644
--- a/docs/examples/fifo/fifo.sh
+++ b/docs/examples/fifo/fifo.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-python3 $SBY_MAIN -f fifo.sby
+python3 $SBY_MAIN -f fifo.sby basic cover noverific
 
 if [[ $? -ne 0 ]] ; then
     exit 1
diff --git a/docs/examples/fifo/golden/fifo.sby b/docs/examples/fifo/golden/fifo.sby
index 824f359..10f2d85 100644
--- a/docs/examples/fifo/golden/fifo.sby
+++ b/docs/examples/fifo/golden/fifo.sby
@@ -2,6 +2,7 @@
 basic bmc
 nofullskip prove
 cover
+noverific cover
 bigtest cover
 
 [options]
@@ -23,6 +24,7 @@ smtbmc boolector
 
 [script]
 nofullskip: read -define NO_FULL_SKIP=1
+noverific: read -noverific
 read -formal fifo.sv
 bigtest: hierarchy -check -top fifo -chparam MAX_DATA 100 -chparam ADDR_BITS 7
 ~bigtest: hierarchy -check -top fifo -chparam MAX_DATA 5 -chparam ADDR_BITS 3
diff --git a/docs/source/newstart.rst b/docs/source/newstart.rst
index 79604f7..9792bd8 100644
--- a/docs/source/newstart.rst
+++ b/docs/source/newstart.rst
@@ -114,6 +114,7 @@ verification.
 **cover**
     Cover mode (testing cover statements).
 
+
 The use of the ``:default`` tag indicates that by default, basic and cover
 should be run if no tasks are specified, such as when running the command below.
 
@@ -188,7 +189,7 @@ Searching the file for ``w_underfill`` will reveal the below.
 
 .. code-block:: text
 
-    $ grep "w_underfill" fifo_cover/logfile.txt -A 2
+    $ grep "w_underfill" fifo_cover/logfile.txt -A 1
     SBY [fifo_cover] engine_0: ##  Reached cover statement at w_underfill in step 2.
     SBY [fifo_cover] engine_0: ##  Writing trace to VCD file: engine_0/trace4.vcd
 
@@ -210,6 +211,7 @@ Adjust the ``[script]`` section of ``fifo.sby`` so that it looks like the below.
 
     [script]
     nofullskip: read -define NO_FULL_SKIP=1
+    noverific: read -noverific
     read -formal fifo.sv
     hierarchy -check -top fifo -chparam MAX_DATA 17
     prep -top fifo