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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
entity top5 is
end entity;
architecture a of top5 is
signal a,b,c,d : std_logic := '0';
signal clk_sys, clk1, clk2 : std_logic;
begin
-- Following throws bug occured with:
-- "psl.sem_property: cannot handle N_CLOCKED_SER"
-- Clocked SERE shall be allowed according to 6.1.1.1 of PSL LRM 2003
-- psl my_seq : assert never {a;b;c} @ rising_edge(clk_sys);
-- Following throws bug occured with: "build_sere_fa: cannot handle N_IMP_SEQ"
-- This is strange because with "always" this is working.
-- According to PSL LRM 2003 FL_Property production for "always" is the
-- same as for "never":
-- FL_Property ::=
-- always FL_Property
-- | always Sequence
--
-- FL_Property ::=
-- never FL_Property
-- | never Sequence
-- Therefore I think if sequence implication works with one, it shall work
-- also with other.
-- psl my_seq : assert never {a} |=> {b; c};
-- Following error is thrown: "translate_psl_expr: cannot handle N_IMP_BOOL"
-- Combination of "never" + implication is not very usefull, since
-- implication is always true apart from case where 1 -> 0, therefore it
-- will mostly fail, however, it should not crash tool (the same goes for
-- previous case too)
-- psl my_seq : assert never (a -> b);
-- Following error is thrown:
-- "top.vhd:43:28:error: operand of a 'never' operator must be a boolean
-- or a sequence"
-- While for "assert always", this works. IMHO this should work for both,
-- equally since productions for never|always are the same.
-- It is not true that operand of never must be a boolean or a sequence.
-- It can be FL_property or sequence, which is much wider set.
-- psl my_seq : assert never (a) -> eventually! (b);
-- Following error is thrown:
-- "top.vhd:43:58:error: left-hand side operand of logical '->' must be
-- a boolean"
-- This is not true, LHS and RHS of implication shall be FL_Property, not
-- just boolean (6.2.1.6.1)
-- psl my_seq : assert always (a -> next b -> next c -> next d);
end;
|
