diff options
-rw-r--r-- | tests/sva/.gitignore | 5 | ||||
-rw-r--r-- | tests/sva/Makefile | 13 | ||||
-rw-r--r-- | tests/sva/basic00.sv | 5 | ||||
-rw-r--r-- | tests/sva/basic01.sv | 4 | ||||
-rw-r--r-- | tests/sva/basic02.sv | 4 | ||||
-rw-r--r-- | tests/sva/basic03.sv | 8 | ||||
-rw-r--r-- | tests/sva/basic04.sv | 4 | ||||
-rw-r--r-- | tests/sva/basic04.vhd | 6 | ||||
-rw-r--r-- | tests/sva/basic05.sv | 4 | ||||
-rw-r--r-- | tests/sva/basic05.vhd | 6 | ||||
-rw-r--r-- | tests/sva/runtest.sh | 60 |
11 files changed, 110 insertions, 9 deletions
diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore new file mode 100644 index 000000000..254013047 --- /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 index 000000000..c2ee5e9d8 --- /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 387f3deef..30c37f5f1 100644 --- 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 596e48db0..74ab93430 100644 --- 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 cf2d72ae7..b34f3aff3 100644 --- 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 a15f3f3a4..8018de4ca 100644 --- 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 6f02f3c19..bc46be9f6 100644 --- 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 889bef0d2..f2ec305ec 100644 --- 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 03854aaac..816ee1da7 100644 --- 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 930f1ba22..8d42f71e8 100644 --- 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 index 000000000..004a172ba --- /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 + |