Add more SVA test cases for future Verific work

diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv
index 6100c50aebe9c1c0cd3db9bbecc9c5bee3427bbc..cf2d72ae7dd85d68720f14e8be6e8700eb7bc7d3 100644 (file)
--- 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 (file)
index 0000000..6f02f3c
--- /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 (file)
index 0000000..889bef0
--- /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 (file)
index 0000000..03854aa
--- /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 (file)
index 0000000..930f1ba
--- /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;