From 84f15260b5f3d328c75ee385d2fdc2861b4e8f59 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 22 Jul 2017 16:35:46 +0200 Subject: [PATCH] Add more SVA test cases for future Verific work --- tests/sva/basic02.sv | 2 +- tests/sva/basic04.sv | 6 ++++++ tests/sva/basic04.vhd | 26 ++++++++++++++++++++++++++ tests/sva/basic05.sv | 15 +++++++++++++++ tests/sva/basic05.vhd | 26 ++++++++++++++++++++++++++ 5 files changed, 74 insertions(+), 1 deletion(-) create mode 100644 tests/sva/basic04.sv create mode 100644 tests/sva/basic04.vhd create mode 100644 tests/sva/basic05.sv create mode 100644 tests/sva/basic05.vhd diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv index 6100c50ae..cf2d72ae7 100644 --- a/tests/sva/basic02.sv +++ b/tests/sva/basic02.sv @@ -13,4 +13,4 @@ module top_properties (input logic clock, read, write, ready); a_wr: assert property ( @(posedge clock) write |-> ready ); endmodule -bind top top_properties inst (.*); +bind top top_properties properties_inst (.*); diff --git a/tests/sva/basic04.sv b/tests/sva/basic04.sv new file mode 100644 index 000000000..6f02f3c19 --- /dev/null +++ b/tests/sva/basic04.sv @@ -0,0 +1,6 @@ +module top_properties (input logic clock, read, write, ready); + a_rw: assert property ( @(posedge clock) !(read && write) ); + a_wr: assert property ( @(posedge clock) write |-> ready ); +endmodule + +bind top top_properties properties_inst (.*); diff --git a/tests/sva/basic04.vhd b/tests/sva/basic04.vhd new file mode 100644 index 000000000..889bef0d2 --- /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; + signal write : std_logic; + signal ready : std_logic; +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 000000000..03854aaac --- /dev/null +++ b/tests/sva/basic05.sv @@ -0,0 +1,15 @@ +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) ); + a_wr: assert property ( @(posedge clock) write |-> ready ); +endmodule diff --git a/tests/sva/basic05.vhd b/tests/sva/basic05.vhd new file mode 100644 index 000000000..930f1ba22 --- /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; + signal write : std_logic; + signal ready : std_logic; +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; -- 2.30.2