Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PSL assert never with custom clocking logic crashes #1116

Open
Blebowski opened this issue Jan 3, 2025 · 0 comments
Open

PSL assert never with custom clocking logic crashes #1116

Blebowski opened this issue Jan 3, 2025 · 0 comments
Labels

Comments

@Blebowski
Copy link
Contributor

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.

@nickg nickg added the psl label Jan 5, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants