Improve SVA tests, add Makefile and scripts

diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore
new file mode 100644 (file)
index 0000000..2540130
--- /dev/null
+++ b/tests/sva/.gitignore
@@ -0,0 +1,5 @@
+/*_pass.sby
+/*_fail.sby
+/*_pass
+/*_fail
+/*.ok

diff --git a/tests/sva/Makefile b/tests/sva/Makefile
new file mode 100644 (file)
index 0000000..c2ee5e9
--- /dev/null
+++ b/tests/sva/Makefile
@@ -0,0 +1,13 @@
+
+TESTS = $(basename $(wildcard *.sv))
+
+all: $(addsuffix .ok,$(TESTS))
+
+%.ok: %.sv
+       bash runtest.sh $<
+
+clean:
+       rm -rf $(addsuffix .ok,$(TESTS))
+       rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS))
+       rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS))
+

diff --git a/tests/sva/basic00.sv b/tests/sva/basic00.sv
index 387f3deef6ca6b80bcadeaa0859e7e73c110eac9..30c37f5f1af5333894eb9468a1c729ab42529ac3 100644 (file)
--- a/tests/sva/basic00.sv
+++ b/tests/sva/basic00.sv
@@ -2,6 +2,11 @@ module top (input clk, reset, antecedent, output reg consequent);
        always @(posedge clk)
                consequent <= reset ? 0 : antecedent;
 
+`ifdef FAIL
        test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |-> consequent )
                        else $error("Failed with consequent = ", $sampled(consequent));
+`else
+       test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |=> consequent )
+                       else $error("Failed with consequent = ", $sampled(consequent));
+`endif
 endmodule

diff --git a/tests/sva/basic01.sv b/tests/sva/basic01.sv
index 596e48db0a100fe9e91ab9ce4638b1b814fdea50..74ab9343035d8e7dea13ae521a05e9e476021e86 100644 (file)
--- a/tests/sva/basic01.sv
+++ b/tests/sva/basic01.sv
@@ -8,5 +8,9 @@ module top (input logic clock, ctrl);
        end
        
        a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
        a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+       a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule

diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv
index cf2d72ae7dd85d68720f14e8be6e8700eb7bc7d3..b34f3aff3138b3a526bf494ca8edfad02387fd73 100644 (file)
--- a/tests/sva/basic02.sv
+++ b/tests/sva/basic02.sv
@@ -10,7 +10,11 @@ endmodule
 
 module top_properties (input logic clock, read, write, ready);
        a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
        a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+       a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule
 
 bind top top_properties properties_inst (.*);

diff --git a/tests/sva/basic03.sv b/tests/sva/basic03.sv
index a15f3f3a4d148501d71afd1079b3cb13a55c69ed..8018de4ca9410ca890522ed1c8f6683b610e515e 100644 (file)
--- a/tests/sva/basic03.sv
+++ b/tests/sva/basic03.sv
@@ -4,7 +4,9 @@ module top (input logic clk, input logic selA, selB, QA, QB, output logic Q);
                if (selB) Q <= QB;
        end
 
-       check_selA: assert property ( @(posedge clk) selA|=> Q == $past(QA) );
-       check_selB: assert property ( @(posedge clk) selB|=> Q == $past(QB) );
-       assume_not_11: assume property ( @(posedge clk) !(selA& selB) );
+       check_selA: assert property ( @(posedge clk) selA |=> Q == $past(QA) );
+       check_selB: assert property ( @(posedge clk) selB |=> Q == $past(QB) );
+`ifndef FAIL
+       assume_not_11: assume property ( @(posedge clk) !(selA & selB) );
+`endif
 endmodule

diff --git a/tests/sva/basic04.sv b/tests/sva/basic04.sv
index 6f02f3c19eb9403885f8d97492383cc2d1311672..bc46be9f689e3c1902beb1eb78413bde4379bdf1 100644 (file)
--- a/tests/sva/basic04.sv
+++ b/tests/sva/basic04.sv
@@ -1,6 +1,10 @@
 module top_properties (input logic clock, read, write, ready);
        a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
        a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+       a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule
 
 bind top top_properties properties_inst (.*);

diff --git a/tests/sva/basic04.vhd b/tests/sva/basic04.vhd
index 889bef0d2d1f16abe840071e2cfbc075c3358bcb..f2ec305ecdbef76bd194e870f649346d8d8834a2 100644 (file)
--- a/tests/sva/basic04.vhd
+++ b/tests/sva/basic04.vhd
@@ -10,9 +10,9 @@ entity top is
 end entity;
 
 architecture rtl of top is
-       signal read : std_logic;
-       signal write : std_logic;
-       signal ready : std_logic;
+       signal read : std_logic := '0';
+       signal write : std_logic := '0';
+       signal ready : std_logic := '0';
 begin
        process (clock) begin
                if (rising_edge(clock)) then

diff --git a/tests/sva/basic05.sv b/tests/sva/basic05.sv
index 03854aaac32aab4f89ebda2b38b900a359705e03..816ee1da700b4cbc926ae42822c0cc208286261a 100644 (file)
--- a/tests/sva/basic05.sv
+++ b/tests/sva/basic05.sv
@@ -11,5 +11,9 @@ module top (input logic clock, ctrl);
        assign ready = uut.ready;
 
        a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
        a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+       a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule

diff --git a/tests/sva/basic05.vhd b/tests/sva/basic05.vhd
index 930f1ba22456b1e030f81cc19e47defb821e33ad..8d42f71e849b1b322952916480f3692b51388ea1 100644 (file)
--- a/tests/sva/basic05.vhd
+++ b/tests/sva/basic05.vhd
@@ -10,9 +10,9 @@ entity demo is
 end entity;
 
 architecture rtl of demo is
-       signal read : std_logic;
-       signal write : std_logic;
-       signal ready : std_logic;
+       signal read : std_logic := '0';
+       signal write : std_logic := '0';
+       signal ready : std_logic := '0';
 begin
        process (clock) begin
                if (rising_edge(clock)) then

diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
new file mode 100644 (file)
index 0000000..004a172
--- /dev/null
+++ b/tests/sva/runtest.sh
@@ -0,0 +1,60 @@
+#!/bin/bash
+
+set -ex
+
+prefix=${1%.sv}
+test -f $prefix.sv
+
+generate_sby() {
+       cat <<- EOT
+               [options]
+               mode bmc
+               depth 10
+               expect $1
+
+               [engines]
+               smtbmc yices
+
+               [script]
+       EOT
+
+       if [ "$1" = "fail" ]; then
+               echo "verific -sv ${prefix}_fail.sv"
+       else
+               echo "verific -sv $prefix.sv"
+       fi
+
+       if [ -f $prefix.vhd ]; then
+               echo "verific -vhdl2008 $prefix.vhd"
+       fi
+
+       cat <<- EOT
+               verific -import -extnets -all top
+               prep -top top
+
+               [files]
+               $prefix.sv
+       EOT
+
+       if [ -f $prefix.vhd ]; then
+               echo "$prefix.vhd"
+       fi
+
+       if [ "$1" = "fail" ]; then
+               cat <<- EOT
+
+                       [file ${prefix}_fail.sv]
+                       \`define FAIL
+                       \`include "$prefix.sv"
+               EOT
+       fi
+}
+
+generate_sby pass > ${prefix}_pass.sby
+generate_sby fail > ${prefix}_fail.sby
+
+sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby
+sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby
+
+touch $prefix.ok
+