PSL assert never with custom clocking logic crashes

[Blebowski]

Hi, I came across yet another PSL issue. If I have locally clocked PSL assertion in never, NVC does not accept it:

entity psl18 is
end entity;

architecture tb of psl18 is

    signal a,b,c : bit;

begin

    -- Covered at 3ns
    -- psl one: assert never (a = b) @rising_edge(c);

end architecture;

I get:

nvc -a --psl ../../../nvc/test/regress/psl18.vhd -e psl18 -r
** Error: sorry, clock expressions are only supported at the outermost level of a property
    > ../../../nvc/test/regress/psl18.vhd:11
    |
 11 |     -- psl one: assert never (a = b) @rising_edge(c);
    |                              ^^^^^^^^^^^^^^^^^^^^^^^
** Error: property is not in the simple subset as the operand of never is not a Boolean or Sequence
    > ../../../nvc/test/regress/psl18.vhd:11
    |
 11 |     -- psl one: assert never (a = b) @rising_edge(c);
    |                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
** Error: sorry, unclocked properties are not supported
    > ../../../nvc/test/regress/psl18.vhd:11
    |
 11 |     -- psl one: assert never (a = b) @rising_edge(c);
    |                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = Note: there is no default clock declaration in this design unit

This worked in GHDL and VCS too.

When I brace the never and use the clocking expression on outermost level as the error indicates:

-- psl one: assert (never (a = b)) @rising_edge(c);

the code analyses fine, but it crashes during elaboration:

 nvc -a --psl ../../../nvc/test/regress/psl18.vhd -e psl18 -r psl18
nvc: ../src/psl/psl-lower.c:311: psl_lower_directive: Assertion `psl_has_ref(top)' failed.

*** Caught signal 6 (SIGABRT) ***

[0x414168] ../src/util.c:897 signal_handler
[0x7f48b3eb1d1f] (/usr/lib64/libpthread-2.28.so) 
[0x7f48aba9952f] (/usr/lib64/libc-2.28.so) raise
[0x7f48aba6ce64] (/usr/lib64/libc-2.28.so) abort
[0x7f48aba6cd38] (/usr/lib64/libc-2.28.so) __assert_fail_base.cold.0
[0x7f48aba91e85] (/usr/lib64/libc-2.28.so) __assert_fail
[0x4f06c2] ../src/psl/psl-lower.c:311 psl_lower_directive
[0x45ce9b] ../src/elab.c:1947 elab_stmts
[0x45eea8] ../src/elab.c:1454 elab_architecture
[0x45f788] ../src/elab.c:2229 elab
[0x40f2f2] ../src/nvc.c:511 elaborate
[0x40f2f2] ../src/nvc.c:2210 process_command
[0x40e8ae] ../src/nvc.c:1930 cover_merge_cmd
[0x40e8ae] ../src/nvc.c:2238 process_command
[0x40c343] ../src/nvc.c:2370 main

In broader sense, it would be nice to have better support for arbitrary combination of clocking events e.g. something like:

-- psl cover {{{a;b}@rising_edge(clk_sys)} => {{c;d}@falling_edge(clk_periph)}};

It may ease things in designs with multiple asynchronous clocks. But I guess this is a lot of work.