5.2 PSL implementation

GHDL understands embedded PSL annotations in VHDL files, but in separate files.

As PSL annotations are embedded within comments, you must analyze and elaborate your design with option -fpsl to enable PSL annotations.

A PSL assertion statement must appear within a comment that starts with the psl keyword. The keyword must be followed (on the same line) by a PSL keyword such as assert or default. To continue a PSL statement on the next line, just start a new comment.

A PSL statement is considered as a concurrent statement, and therefore is allowed only where processes are.

All PSL assertions must be clocked (GHDL doesn't support unclocked assertion). Furthermore only one clock per assertion is allowed.

You can either use a default clock like this:

       -- psl default clock is rising_edge (CLK);
       -- psl assert always
       --   a -> eventually! b;

or use a clocked expression (note the use of parenthesis):

       -- psl assert (always a -> next[3](b)) @rising_edge (clk);

Of course only the simple subset of PSL is allowed.

Currently the built-in functions are not implemented.