sem_psl_verification_unit: cannot handle IIR_KIND_PSL_DECLARATION #1889
Description
Description
Seems to happen whenever I try to declare a property or sequence in PSL.
The output I get looks like this:
SBY 9:52:51 [shiftMux2_bmc] base: sem_psl_verification_unit: cannot handle IIR_KIND_PSL_DECLARATION (shiftMux2.psl:7:4)
Expected behaviour
I suppose it should either work or give me a better error message?
How to reproduce?
seem like trying to declare almost any property or sequence breaks it.
I've tried to simplify it to this;
library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
entity shiftMux2 is
Port (
clk : in std_logic;
--inputA
inputA : in std_logic;
outputB : out std_logic
);
end shiftMux2;
architecture Rtl of shiftMux2 is
begin
process (clk) is
begin
if rising_edge(clk) then
outputB <= inputA;
end if;
end process;
end Rtl;vunit i_t1(shiftMux2(rtl))
{
-- set all declarations to run on clk
default clock is rising_edge(clk);
--it breaks on this line:
sequence s1 is {inputA };
sequence s2 is {inputB };
assert always (s1) |=> (s2);
--this works:
--assert always {inputA } |=> {outputB};
}
[tasks]
bmc
[options]
bmc: mode bmc
bmc: depth 16
[engines]
smtbmc
[script]
ghdl --std=08 shiftMux2.vhd shiftMux2.psl -e shiftMux2
prep -top shiftMux2
[files]
shiftMux2.psl
shiftMux2.vhd
Then execute with:
$ sby --yosys "yosys -m ghdl" -f shiftMux2.sby
Context
Please, provide the following information:
- OS: Debian 10
- Origin:
- Package manager:
? - Released binaries:
? - Built from sources:
2.0.0-dev (1.0.0.r822.g3486a9d3)(I built from master branch)
- Package manager:
If a GHDL Bug occurred block is shown in the log, please paste it here:
*SBY 9:55:13 [shiftMux2_bmc] base: ******************** GHDL Bug occurred ***************************
SBY 9:55:13 [shiftMux2_bmc] base: Please report this bug on https://github.com/ghdl/ghdl/issues
SBY 9:55:13 [shiftMux2_bmc] base: GHDL release: 2.0.0-dev (1.0.0.r822.g3486a9d3) [Dunoon edition]
SBY 9:55:13 [shiftMux2_bmc] base: Compiled with unknown compiler version
SBY 9:55:13 [shiftMux2_bmc] base: Target: x86_64-linux-gnu
SBY 9:55:13 [shiftMux2_bmc] base: /home/heinrich/Formal/test3/shiftMux2_bmc/src/
SBY 9:55:13 [shiftMux2_bmc] base: Command line:
SBY 9:55:13 [shiftMux2_bmc] base: Exception TYPES.INTERNAL_ERROR raised
SBY 9:55:13 [shiftMux2_bmc] base: Exception information:
SBY 9:55:13 [shiftMux2_bmc] base: raised TYPES.INTERNAL_ERROR : vhdl-errors.adb:30
SBY 9:55:13 [shiftMux2_bmc] base: ******************************************************************
If I compile from the v1.0.0 tag I get this one:
SBY 10:06:01 [shiftMux2_bmc] base: ******************** GHDL Bug occurred ***************************
SBY 10:06:01 [shiftMux2_bmc] base: Please report this bug on https://github.com/ghdl/ghdl/issues
SBY 10:06:01 [shiftMux2_bmc] base: GHDL release: 1.0.0 (1.0.0.r0.g2fb2384d) [Dunoon edition]
SBY 10:06:01 [shiftMux2_bmc] base: Compiled with unknown compiler version
SBY 10:06:01 [shiftMux2_bmc] base: Target: x86_64-linux-gnu
SBY 10:06:01 [shiftMux2_bmc] base: /home/heinrich/Formal/test3/shiftMux2_bmc/src/
SBY 10:06:01 [shiftMux2_bmc] base: Command line:
SBY 10:06:01 [shiftMux2_bmc] base: Exception TYPES.INTERNAL_ERROR raised
SBY 10:06:01 [shiftMux2_bmc] base: Exception information:
SBY 10:06:01 [shiftMux2_bmc] base: raised TYPES.INTERNAL_ERROR : vhdl-errors.adb:30
SBY 10:06:01 [shiftMux2_bmc] base: ******************************************************************
Additional context
I'm still learning PSL so maybe I should not be doing it this way?
But I can't seem to figure out any way to make a property or sequence statement work.