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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
// DESCRIPTION: Verilator: Verilog Test module
//
//
// This file ONLY is placed into the Public Domain, for any use,
// without warranty, 2005 by Wilson Snyder.
// verilator metacomment preserved
/**/
/*verilator metacomment also_preserved*/
Hello in t_preproc_psl.v
// Psl capitalized not relevant
// Double commented ignored // psl not ok
// You can't have multiple statements on one // psl line.
// Inline /*cmt*/ comments not allowed inside psl comments
// psl default clock = (posedge clk);
// psl fails1: cover {cyc==10};
// psl assert always cyc!=10;
// psl assert always cyc==3 -> mask==8'h2;
// psl failsx: cover {cyc==3 && mask==8'h1};
/* psl fails2:
cover {
cyc==3 && mask==8'h9};
// Ignore this comment-in-between-statements (however not legal inside a statement)
fails3: always assert {
cyc==3 && mask==8'h10 };
*/
`__LINE__
// Note the PSL statement can be on a unique line
// There can also be multiple "psl" keywords per line.
/*
psl
fails_ml:
assert always
cyc==3 -> mask==8'h21;
psl
fails_mlalso: assert always cyc==3 -> mask==8'h21;
*/
`__LINE__
// psl assert never (cyc==1 && reset_l);
// psl fails3: assert always
// cyc==3 -> mask==8'h21;
// syntax_error, not_part_of_above_stmt;
// We need to count { and ( when looking for ; that terminate a PSL expression
// psl assert always
// {[*]; cyc==3;
// cyc==4; cyc==6};
// syntax_error, not_part_of_above_stmt;
// However /**/ pairs can't be split as above.
`ifdef NEVER
// psl ifdefs have precedence;
`endif
// Macros are expanded...
`define define_sig cyc
// psl assert always `define_sig!=10;
`ifdef verilator
`psl
psl assert always sig!=90;
`verilog
`endif
// Did we end up right?
`__LINE__
|
