3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-13 16:48:44 +00:00

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.
This commit is contained in:
KrystalDelusion 2022-08-09 11:29:19 +12:00
parent ad8730fa44
commit 1d4716a5f9
4 changed files with 8 additions and 2 deletions

View file

@ -2,6 +2,7 @@
basic bmc basic bmc
nofullskip prove nofullskip prove
cover cover
noverific cover
basic cover : default basic cover : default
[options] [options]
@ -20,6 +21,7 @@ smtbmc boolector
[script] [script]
nofullskip: read -define NO_FULL_SKIP=1 nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv read -formal fifo.sv
prep -top fifo prep -top fifo

View file

@ -1,6 +1,6 @@
#!/bin/bash #!/bin/bash
python3 $SBY_MAIN -f fifo.sby python3 $SBY_MAIN -f fifo.sby basic cover noverific
if [[ $? -ne 0 ]] ; then if [[ $? -ne 0 ]] ; then
exit 1 exit 1

View file

@ -2,6 +2,7 @@
basic bmc basic bmc
nofullskip prove nofullskip prove
cover cover
noverific cover
bigtest cover bigtest cover
[options] [options]
@ -23,6 +24,7 @@ smtbmc boolector
[script] [script]
nofullskip: read -define NO_FULL_SKIP=1 nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv 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 100 -chparam ADDR_BITS 7
~bigtest: hierarchy -check -top fifo -chparam MAX_DATA 5 -chparam ADDR_BITS 3 ~bigtest: hierarchy -check -top fifo -chparam MAX_DATA 5 -chparam ADDR_BITS 3

View file

@ -114,6 +114,7 @@ verification.
**cover** **cover**
Cover mode (testing cover statements). Cover mode (testing cover statements).
The use of the ``:default`` tag indicates that by default, basic and cover 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. 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 .. 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: ## Reached cover statement at w_underfill in step 2.
SBY [fifo_cover] engine_0: ## Writing trace to VCD file: engine_0/trace4.vcd 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] [script]
nofullskip: read -define NO_FULL_SKIP=1 nofullskip: read -define NO_FULL_SKIP=1
noverific: read -noverific
read -formal fifo.sv read -formal fifo.sv
hierarchy -check -top fifo -chparam MAX_DATA 17 hierarchy -check -top fifo -chparam MAX_DATA 17
prep -top fifo prep -top fifo