testsuite/gna/issue1371/incr_psl.vhdl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
use IEEE.NUMERIC_STD.ALL;

-- This could be combinational but GHDL does not support @(True) PSL yet
entity incr_psl is
    Port (
        clk: in STD_LOGIC;
        in_val: in UNSIGNED(7 downto 0);
        out_val: out UNSIGNED(7 downto 0)
    );
end entity;

architecture Behavioral of incr_psl is
    signal out_val_internal: UNSIGNED(7 downto 0);
begin
    out_val_internal <= in_val + 1;
    out_val <= out_val_internal;
    -- psl default clock is rising_edge(clk);

    -- The combination of the two below work
    -- psl assert always (in_val = 0 -> out_val_internal = 1);
    -- psl assert always (out_val_internal = 1 -> in_val = 0);
    -- This causes an error
    -- psl assert always (in_val = 0 <-> out_val_internal = 1);
end Behavioral;