testsuite/gna/ticket24/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
27
28
29
30

entity psl is
end;

architecture behav of psl is
  signal a, b, c : bit;
  signal clk : bit;
  subtype wf_type is bit_vector (0 to 7);
  constant wave_a : wf_type := "10010100";
  constant wave_b : wf_type := "01001010";
  constant wave_c : wf_type := "00100101";
begin
  process
  begin
    for i in wf_type'range loop
      clk <= '0';
      wait for 1 ns;
      a <= wave_a (i);
      b <= wave_b (i);
      c <= wave_c (i);
      clk <= '1';
      wait for 1 ns;
    end loop;
    wait;
  end process;
  
  -- psl default clock is (clk'event and clk = '1');
  -- psl a1: assert always a |=> b;
  -- psl a2: assert always a -> eventually! c;
  -- psl c1: cover {a;b;c};
end behav;