PSL - an option to treat analyze errors as warnings

[m-kru]

NVC capabilities of PSL parsing are limited. If the parser encounters some valid, but unsupported construct, the analysis fails and returns exit status 1. I think there should be an additional parameter allowing to turn PSL parsing errors into warnings. I am currently porting test benches to run using nvc, and it looks like it is all or nothing regarding the PSL.

[nickg]

Are you using PSL in --psl comments or directly embedded in the VHDL with --std=2008?

[m-kru]

In comments, and I use --std=2019.

   -- psl default clock is rising_edge(clk_i);
   -- psl min: assert always min_o |=> not min_o;
   -- psl max: assert always max_o |=> not max_o;
   -- psl rst: assert always rst_i |=> min_o = MIN_RESET_VALUE and max_o = MAX_RESET_VALUE and q_o = RESET_VALUE;

** Error: unexpected | while parsing assert directive, expecting one of **, union or ;
    > /home/mkru/workspace/vhdl/vhdl-simple/binary_counter/src/binary_counter.vhd:61
    |
 61 |    -- psl min: assert always min_o |=> not min_o;
    |                                    ^ this token was unexpected
** Error: unexpected | while parsing assert directive, expecting one of **, union or ;
    > /home/mkru/workspace/vhdl/vhdl-simple/binary_counter/src/binary_counter.vhd:62
    |
 62 |    -- psl max: assert always max_o |=> not max_o;
    |                                    ^ this token was unexpected
** Error: unexpected | while parsing assert directive, expecting one of **, union or ;
    > /home/mkru/workspace/vhdl/vhdl-simple/binary_counter/src/binary_counter.vhd:63
    |
 63 |    -- psl rst: assert always rst_i |=> min_o = MIN_RESET_VALUE and max_o = MAX_RESET_VALUE and q_o = RESET_VALUE;
    |                                    ^ this token was unexpected
nvc::analyze: /home/mkru/workspace/vhdl/vhdl-simple/binary_counter/src/binary_counter.vhd analysis failed with exit status 1

[nickg]

You're passing the --psl analysis option as well right? If you don't pass that is should just ignore the PSL entirely.

[m-kru]

Yes, I pass --psl argument. However, I still would like to run the test bench, even though some PSL constructs are not yet supported by nvc. I see 2 options. Ignore all PSL formulas within a file if at least one cannot be parsed. Ignore all PSL formulas that cannot be parsed correctly, but make the ones correctly parsed work as expected. This would require additional command line parameter, as the default behavior is probably what user expects.

[nickg]

I think the problem here is really that it advertises the --psl option when PSL support is not complete. I've removed that for now.