diff options
author | Ruben Undheim <ruben.undheim@gmail.com> | 2018-08-30 20:46:20 +0200 |
---|---|---|
committer | Ruben Undheim <ruben.undheim@gmail.com> | 2018-08-30 20:46:20 +0200 |
commit | 5033b51947a6ef02cb785b5622e993335efa750a (patch) | |
tree | 7bed18c526bd94917fa2f08e3df12209863698a1 /tests/sva | |
parent | fefe0fc0430f4f173a25e674708aa0f4f0854b31 (diff) |
New upstream version 0.7+20180830git0b7a184
Diffstat (limited to 'tests/sva')
-rw-r--r-- | tests/sva/.gitignore | 7 | ||||
-rw-r--r-- | tests/sva/Makefile | 13 | ||||
-rw-r--r-- | tests/sva/basic00.sv | 12 | ||||
-rw-r--r-- | tests/sva/basic01.sv | 16 | ||||
-rw-r--r-- | tests/sva/basic02.sv | 20 | ||||
-rw-r--r-- | tests/sva/basic03.sv | 12 | ||||
-rw-r--r-- | tests/sva/basic04.sv | 10 | ||||
-rw-r--r-- | tests/sva/basic04.vhd | 26 | ||||
-rw-r--r-- | tests/sva/basic05.sv | 19 | ||||
-rw-r--r-- | tests/sva/basic05.vhd | 26 | ||||
-rw-r--r-- | tests/sva/counter.sv | 30 | ||||
-rw-r--r-- | tests/sva/runtest.sh | 72 | ||||
-rw-r--r-- | tests/sva/sva_not.sv | 34 | ||||
-rw-r--r-- | tests/sva/sva_range.sv | 19 | ||||
-rw-r--r-- | tests/sva/sva_throughout.sv | 19 |
15 files changed, 335 insertions, 0 deletions
diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore new file mode 100644 index 00000000..cc254049 --- /dev/null +++ b/tests/sva/.gitignore @@ -0,0 +1,7 @@ +/*_pass.sby +/*_fail.sby +/*_pass +/*_fail +/*.ok +/vhdlpsl[0-9][0-9] +/vhdlpsl[0-9][0-9].sby diff --git a/tests/sva/Makefile b/tests/sva/Makefile new file mode 100644 index 00000000..1b217f74 --- /dev/null +++ b/tests/sva/Makefile @@ -0,0 +1,13 @@ + +TESTS = $(sort $(basename $(wildcard *.sv)) $(basename $(wildcard *.vhd))) + +all: $(addsuffix .ok,$(TESTS)) + +%.ok: + bash runtest.sh $@ + +clean: + rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(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 new file mode 100644 index 00000000..30c37f5f --- /dev/null +++ b/tests/sva/basic00.sv @@ -0,0 +1,12 @@ +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 new file mode 100644 index 00000000..74ab9343 --- /dev/null +++ b/tests/sva/basic01.sv @@ -0,0 +1,16 @@ +module top (input logic clock, ctrl); + logic read = 0, write = 0, ready = 0; + + always @(posedge clock) begin + read <= !ctrl; + write <= ctrl; + ready <= write; + 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 new file mode 100644 index 00000000..b34f3aff --- /dev/null +++ b/tests/sva/basic02.sv @@ -0,0 +1,20 @@ +module top (input logic clock, ctrl); + logic read = 0, write = 0, ready = 0; + + always @(posedge clock) begin + read <= !ctrl; + write <= ctrl; + ready <= write; + end +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 new file mode 100644 index 00000000..8018de4c --- /dev/null +++ b/tests/sva/basic03.sv @@ -0,0 +1,12 @@ +module top (input logic clk, input logic selA, selB, QA, QB, output logic Q); + always @(posedge clk) begin + if (selA) Q <= QA; + 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) ); +`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 new file mode 100644 index 00000000..bc46be9f --- /dev/null +++ b/tests/sva/basic04.sv @@ -0,0 +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 new file mode 100644 index 00000000..f2ec305e --- /dev/null +++ b/tests/sva/basic04.vhd @@ -0,0 +1,26 @@ +library ieee; +use ieee.std_logic_1164.all; + +entity top is + port ( + clock : in std_logic; + ctrl : in std_logic; + x : out std_logic + ); +end entity; + +architecture rtl of top is + signal read : std_logic := '0'; + signal write : std_logic := '0'; + signal ready : std_logic := '0'; +begin + process (clock) begin + if (rising_edge(clock)) then + read <= not ctrl; + write <= ctrl; + ready <= write; + end if; + end process; + + x <= read xor write xor ready; +end architecture; diff --git a/tests/sva/basic05.sv b/tests/sva/basic05.sv new file mode 100644 index 00000000..816ee1da --- /dev/null +++ b/tests/sva/basic05.sv @@ -0,0 +1,19 @@ +module top (input logic clock, ctrl); + logic read, write, ready; + + demo uut ( + .clock(clock), + .ctrl(ctrl) + ); + + assign read = uut.read; + assign write = uut.write; + 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 new file mode 100644 index 00000000..8d42f71e --- /dev/null +++ b/tests/sva/basic05.vhd @@ -0,0 +1,26 @@ +library ieee; +use ieee.std_logic_1164.all; + +entity demo is + port ( + clock : in std_logic; + ctrl : in std_logic; + x : out std_logic + ); +end entity; + +architecture rtl of demo is + signal read : std_logic := '0'; + signal write : std_logic := '0'; + signal ready : std_logic := '0'; +begin + process (clock) begin + if (rising_edge(clock)) then + read <= not ctrl; + write <= ctrl; + ready <= write; + end if; + end process; + + x <= read xor write xor ready; +end architecture; diff --git a/tests/sva/counter.sv b/tests/sva/counter.sv new file mode 100644 index 00000000..4f949115 --- /dev/null +++ b/tests/sva/counter.sv @@ -0,0 +1,30 @@ +module top (input clk, reset, up, down, output reg [7:0] cnt); + always @(posedge clk) begin + if (reset) + cnt <= 0; + else if (up) + cnt <= cnt + 1; + else if (down) + cnt <= cnt - 1; + end + + default clocking @(posedge clk); endclocking + default disable iff (reset); + + assert property (up |=> cnt == $past(cnt) + 8'd 1); + assert property (up [*2] |=> cnt == $past(cnt, 2) + 8'd 2); + assert property (up ##1 up |=> cnt == $past(cnt, 2) + 8'd 2); + +`ifndef FAIL + assume property (down |-> !up); +`endif + assert property (up ##1 down |=> cnt == $past(cnt, 2)); + assert property (down |=> cnt == $past(cnt) - 8'd 1); + + property down_n(n); + down [*n] |=> cnt == $past(cnt, n) - n; + endproperty + + assert property (down_n(8'd 3)); + assert property (down_n(8'd 5)); +endmodule diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh new file mode 100644 index 00000000..1b65ca9c --- /dev/null +++ b/tests/sva/runtest.sh @@ -0,0 +1,72 @@ +#!/bin/bash + +set -ex + +prefix=${1%.ok} +prefix=${prefix%.sv} +prefix=${prefix%.vhd} +test -f $prefix.sv -o -f $prefix.vhd + +generate_sby() { + cat <<- EOT + [options] + mode bmc + depth 10 + expect $1 + + [engines] + smtbmc yices + + [script] + EOT + + if [ -f $prefix.sv ]; then + if [ "$1" = "fail" ]; then + echo "verific -sv ${prefix}_fail.sv" + else + echo "verific -sv $prefix.sv" + fi + fi + + if [ -f $prefix.vhd ]; then + echo "verific -vhdl $prefix.vhd" + fi + + cat <<- EOT + verific -import -extnets -all top + prep -top top + chformal -early -assume + + [files] + EOT + + if [ -f $prefix.sv ]; then + echo "$prefix.sv" + fi + + 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 +} + +if [ -f $prefix.sv ]; then + 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 +else + generate_sby pass > ${prefix}.sby + sby --yosys $PWD/../../yosys -f ${prefix}.sby +fi + +touch $prefix.ok + diff --git a/tests/sva/sva_not.sv b/tests/sva/sva_not.sv new file mode 100644 index 00000000..d81a4865 --- /dev/null +++ b/tests/sva/sva_not.sv @@ -0,0 +1,34 @@ +module top ( + input clk, + input reset, + input ping, + input [1:0] cfg, + output reg pong +); + reg [2:0] cnt; + localparam integer maxdelay = 8; + + always @(posedge clk) begin + if (reset) begin + cnt <= 0; + pong <= 0; + end else begin + cnt <= cnt - |cnt; + pong <= cnt == 1; + if (ping) cnt <= 4 + cfg; + end + end + + assert property ( + @(posedge clk) + disable iff (reset) + not (ping ##1 !pong [*maxdelay]) + ); + +`ifndef FAIL + assume property ( + @(posedge clk) + not (cnt && ping) + ); +`endif +endmodule diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv new file mode 100644 index 00000000..d1569fc8 --- /dev/null +++ b/tests/sva/sva_range.sv @@ -0,0 +1,19 @@ +module top ( + input clk, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + + assert property ( + a ##[*] b |=> c until d + ); + +`ifndef FAIL + assume property ( + b |=> ##5 d + ); + assume property ( + b || (c && !d) |=> c + ); +`endif +endmodule diff --git a/tests/sva/sva_throughout.sv b/tests/sva/sva_throughout.sv new file mode 100644 index 00000000..7e036a06 --- /dev/null +++ b/tests/sva/sva_throughout.sv @@ -0,0 +1,19 @@ +module top ( + input clk, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + + assert property ( + a |=> b throughout (c ##1 d) + ); + +`ifndef FAIL + assume property ( + a |=> b && c + ); + assume property ( + b && c |=> b && d + ); +`endif +endmodule |