PSL various crashes of built-in functions

[Blebowski]

Some of the PSL built-in functions crash. E.g. rose and fell crash:

FELL_5_a : assert never (fell(b));

crashes with:

make psl_fell
nvc --std=08 --work=lib_psl_fell -a  ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd
nvc --std=08 --work=lib_psl_fell -a --psl ../src/psl_fell.vhd
** Fatal: tree kind T_PSL does not have item I_PORTS
[0x40a559] ../src/object.c:255 object_lookup_failed
[0x40b365] ../src/tree.c:598 tree_ports
[0x40b365] ../src/tree.c:596 tree_ports.cold.146
[0x4c2c49] ../src/simp.c:51 simp_call_args
[0x4c31c5] ../src/simp.c:239 simp_fcall
[0x4c31c5] ../src/simp.c:1575 simp_tree.lto_priv.562
[0x4b1e83] ../src/object.c:715 object_rewrite_iter
[0x4b1bdc] ../src/object.c:815 object_rewrite
[0x4b1c3e] ../src/object.c:779 object_rewrite
[0x4b1c3e] ../src/object.c:779 object_rewrite
[0x4b1c3e] ../src/object.c:779 object_rewrite
[0x4b1c3e] ../src/object.c:779 object_rewrite
[0x4b1d81] ../src/object.c:790 object_rewrite
[0x4de8e6] ../src/tree.c:1310 tree_rewrite
[0x4b9063] ../src/simp.c:1710 analyse_file
[0x512a87] ../src/nvc.c:249 analyse
[0x512a87] ../src/nvc.c:2113 process_command.lto_priv.839
[0x40d3a7] ../src/nvc.c:2257 main

nvc 1.14.0 (1.13.0.r160.g4cb3822b) (Using LLVM 17.0.6) [x86_64-pc-linux-gnu]

Please report this bug at https://github.com/nickg/nvc/issues

make: *** [Makefile:14: psl_fell] Error 1

Almost equal crash occurs with rose.

When I try isunknown but pass only argument of std_logic type, I get slightly different crash:

FELL_5_a : assert never (isunknown(b));

with the crash:

make psl_fell
nvc --std=08 --work=lib_psl_fell -a  ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd
nvc --std=08 --work=lib_psl_fell -a --psl ../src/psl_fell.vhd
nvc --std=08 --work=lib_psl_fell -a tb_tops/psl_fell/testbench.vhd
nvc --std=08 --work=lib_psl_fell -e --cover tb_psl_fell
nvc --std=08 --work=lib_psl_fell -r tb_psl_fell --wave=psl_fell

*** Caught signal 11 (SEGV_MAPERR) [address=0x2, ip=0x7f99ddd0d9db] ***

[0x50b11c] ../src/util.c:872 signal_handler
[0x7f99f075fd1f] (/usr/lib64/libpthread-2.28.so) 
[0x7f99ddd0d9db] (/usr/local/lib/nvc/preload08.so) NVC.PSL_SUPPORT.ISUNKNOWN(Y)B
[0x7f99dd5fb25d] (/home/oille/psl_with_ghdl/sim/lib_psl_fell/_LIB_PSL_FELL.TB_PSL_FELL.elab.so) LIB_PSL_FELL.TB_PSL_FELL.DUT.FELL_5_A
[0x45c46d] ../src/jit/jit-core.c:666 jit_try_vcall.lto_priv.194
[0x45c949] ../src/jit/jit-core.c:760 jit_fastcall
[0x45c9eb] ../src/rt/model.c:2462 update_property
[0x45c9eb] ../src/rt/model.c:2718 async_update_property
[0x45fa2f] ../src/rt/model.c:390 deferq_run.isra.25.lto_priv.842
[0x5152df] ../src/rt/model.c:3306 model_run
[0x5152df] ../src/rt/model.c:857 run_cmd.lto_priv.812
[0x511a7c] ../src/nvc.c:2117 process_command.lto_priv.839
[0x40d3a7] ../src/nvc.c:2257 main

nvc 1.14.0 (1.13.0.r160.g4cb3822b) (Using LLVM 17.0.6) [x86_64-pc-linux-gnu]

Please report this bug at https://github.com/nickg/nvc/issues

make: *** [Makefile:17: psl_fell] Error 2

with argument of std_logic_vector, the isunknown seems to work correctly. I think parser should reject this at analysis time, since isunknown is defined only for BitCector type in PSL LRM. NVC behaves that-way for onehot function, e.g.:

FELL_5_a : assert never (isunknown(b));

and returns correct error:

** Error: no matching subprogram ONEHOT [STD_LOGIC return BOOLEAN | BIT | STD_ULOGIC]
    > ../src/psl_fell.vhd:33
    |
 33 |   FELL_5_a : assert never (onehot(b));
    |                            ^^^^^^^^^
make: *** [Makefile:14: psl_fell] Error 1

TO reproduce is the same repo as other issues with:

1. GIT hash: 9024a2cdc3d134904ae784781d8a62278b8baf6d
2. make psl_fell

[Blebowski]

@nickg I can try to have a look at some of the PSL issues, but I need to know what to deal with so that we will not have conflicts, or work on the same stuff...

[tmeissner]

I think VHDL std_logic_vector also "maps" on PSL bitvector, so it should be legal. AFAIR I had this discussion with Tristan already during testing or implementing PSL stuff in GHDL. I try to find the exact wording in the PSL LRM.

[Blebowski]

I maybe was not precise:

• PSL BitVector definitely maps to std_logic_vector.
• PSL BitVector does not map to std_logic and IMHO should return the same error as onehot when called with argument of std_logic type.

[tmeissner]

PSL standard (IEEE 1850-2010):

5.1.2:

In VHDL, type STD.Standard.Bit, and type IEEE.Std_Logic_1164.std_ulogic, as well as subtypes thereof, are Bit types.

5.1.3:

In VHDL and GDL, any type that is a one-dimensional array of a Bit type is interpretable as a BitVector type.

[tmeissner]

I maybe was not precise:

* PSL `BitVector` definitely maps to `std_logic_vector`.

* PSL `BitVector` does not map to `std_logic` and IMHO should return the same error as `onehot` when called with argument of `std_logic` type.

Ah, okay. So you mean is_unknown() should not work on Bit and std_logic.

[Blebowski]

Yes, that is it.