mirror of https://github.com/YosysHQ/yosys.git
Add more SVA test cases for future Verific work
This commit is contained in:
parent
5be535517c
commit
84f15260b5
|
@ -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 (.*);
|
||||
|
|
|
@ -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 (.*);
|
|
@ -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;
|
|
@ -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
|
|
@ -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;
|
Loading…
Reference in New Issue