Ghdl: assertion failure in synthesis without the report message

[rodrigomelo9]

The following example, from ISE, reports the message and aborts with ISE and is ignored by Vivado. In GHDL aborts, which is great, but without the message and is a desired feature for formal verification.

library ieee;
use ieee.std_logic_1164.all;

entity SINGLE_SRL is
    generic (SRL_WIDTH : integer := 24);
    port (
        clk : in std_logic;
        inp : in std_logic;
        outp : out std_logic);
end SINGLE_SRL;

architecture beh of SINGLE_SRL is
    signal shift_reg : std_logic_vector (SRL_WIDTH-1 downto 0);
begin
    assert SRL_WIDTH <= 17
    report "The size of Shift Register exceeds the size of a single SRL"
    severity FAILURE;

    process (clk)
    begin
        if rising_edge(clk) then
            shift_reg <= shift_reg (SRL_WIDTH-2 downto 0) & inp;
        end if;
    end process;

    outp <= shift_reg(SRL_WIDTH-1);
end beh;

library ieee;
use ieee.std_logic_1164.all;

entity TOP is
    port (
        clk : in std_logic;
        inp1, inp2 : in std_logic;
        outp1, outp2 : out std_logic);
end TOP;

architecture beh of TOP is
    component SINGLE_SRL is
        generic (SRL_WIDTH : integer := 16);
        port(
            clk : in std_logic;
            inp : in std_logic;
            outp : out std_logic);
     end component;
begin
    inst1: SINGLE_SRL
        generic map (SRL_WIDTH => 13)
        port map(
            clk => clk,
            inp => inp1,
            outp => outp1 );
    inst2: SINGLE_SRL
        generic map (SRL_WIDTH => 18)
        port map(
            clk => clk,
            inp => inp2,
            outp => outp2 );
end beh;

$ docker run --rm -t -v $(pwd):/src -w /src ghdl/synth:beta ghdl --synth examples/ise/VHDL_Language_Support/asserts/asserts_1.vhd -e
ghdl:note: top entity is "top"
examples/ise/VHDL_Language_Support/asserts/asserts_1.vhd:21:5:error: assertion failure

The ISE message is:

Elaborating entity <SINGLE_SRL> (architecture <beh>) with generics from library <work>.
ERROR:HDLCompiler:1242 - "/home/ram/repos/yosys-versus/xilinx/examples/ise/VHDL_Language_Support/asserts/asserts_1.vhd" Line 21: "The size of Shift Register exceeds the size of a single SRL": 
Netlist SINGLE_SRL(18)(beh) remains a blackbox, due to errors in its contents

[tmeissner]

What do you mean with formal verification? You only can formal verify designs which can be synthesized without errors. Each formal tool I know works on synthesized netlists. Your design can't be formally verified becuase it can't be synthesized.

[rodrigomelo9]

First, it was only an example. There exist synthesizable code which has asserts. You can ignore them, or you can evaluate them. GHDL is evaluating the assert (I changed 17 by 27 in the assertion and the description was synthesized). So, if assertion are supported, I think that It could be good to support also the report, to know why it failed.

What do you mean with formal verification?

When you check the correctness of your design, for example, based on assertions.

[tmeissner]

I know what formal verification is, as I'm doing such stuff since quite a time :-)

For example: libvhdl or formal_hw_verification

I only meant that only synthesisable designs can be verified with formal tools, as the solvers are working on synthesized netlists.

So in case of the upper assertion, either the assertion is fullfilled or the synthesis tool would have to ignore it to get a netlist. I think the first way is the better, maybe with supporting the printig of the report string.

[eine]

I think the first way is the better, maybe with supporting the printig of the report string.

I believe this is the enhancement request that @rodrigomelo9 is doing with this issue.