64 bits slicing problem

[Martoni]

Hello,

I have a problem using ghdl in conjonction with yosys smtbmc solver.

The module is slicing input to smaller output as follow :

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

entity slice_bug is
  generic(
    INPUT_WIDTH : natural := 64;
    OUTPUT_WIDTH: natural := 32;
    MAX_DIV : natural := 16
  );
  port (
    clock_i : in std_logic;
    divindex  : in std_logic_vector(31 downto 0);
    indata : in std_logic_vector(INPUT_WIDTH-1 downto 0);
    outdata : out std_logic_vector(OUTPUT_WIDTH-1 downto 0)
  );
end entity slice_bug;

architecture rtl of slice_bug is

  signal div_index : natural range 0 to MAX_DIV; 

  signal indata_tready_s : std_logic;

  signal output_re_s : std_logic_vector((OUTPUT_WIDTH/2)-1 downto 0);
  signal output_im_s : std_logic_vector((OUTPUT_WIDTH/2)-1 downto 0);

  signal output_tmp : std_logic_vector((INPUT_WIDTH/2)-1 downto 0);

begin

  div_index <= to_integer(unsigned(divindex));

  output_re_s <= indata((OUTPUT_WIDTH/2)+div_index-1 downto div_index);

--  output_tmp <= indata(INPUT_WIDTH-1 downto OUTPUT_WIDTH);
--  output_im_s <= output_tmp((OUTPUT_WIDTH/2)+div_index-1 downto div_index);
  output_im_s <= indata((OUTPUT_WIDTH/2)+(INPUT_WIDTH/2) + div_index-1 downto
                 div_index + (INPUT_WIDTH/2));

  outdata <= output_im_s & output_re_s;

end architecture rtl;

If I test it with a pure vhdl testbench it's working well :

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use std.env.finish;

entity slice_bug_tb is
end entity;

architecture test of slice_bug_tb is

  signal divindex : std_logic_vector(31 downto 0);
  signal indata : std_logic_vector(63 downto 0);
  signal outdata : std_logic_vector(31 downto 0);

begin

slice_bug_p: entity work.slice_bug(rtl)
port map (
  clock_i => '0', 
  divindex => divindex,
  indata => indata,
  outdata => outdata);

stimulus: process
begin

  divindex <= std_logic_vector(to_unsigned(12, 32));
  indata <= x"0BEBE0000CACA000";
  wait for 1 ns;
  assert outdata = x"BEBECACA" report "Wrong output data" severity error;
  finish;

end process stimulus;
end architecture test;

But if I convert it with Yosys to do formal prove, it doesn't works.

PSL assertion are as follow:

vunit i_slice_bug(slice_bug(rtl))
{

  default clock is rising_edge(clock_i);

  fassert : assert always
    {divindex = x"0000000C" and indata = x"0BEBE0000CACA000"}
    |-> {outdata = x"BEBECACA"};

  ----------------
  -- cover
  fcov_value : cover {
        indata = x"0BEBE0000CACA000"
    and outdata = x"BEBECACA"};

}

SBY script I'm using :

[tasks]
bmc
cover
prove

[options]
bmc: mode bmc
bmc: depth 40

prove: mode prove
prove: depth 40

cover: mode cover
cover: depth 40

[engines]
smtbmc z3

[script]
ghdl --std=08 slice_bug.vhd slice_bug.psl -e slice_bug
prep -top slice_bug

[files]
slice_bug.vhd
slice_bug.psl

# to run it :
# sby --yosys "yosys -m /opt/ghdl-yosys-plugin/ghdl.so" -f slice_bug.sby

Cover statement is not reached and assert fail.

If I look at traces, the inputs divindex=12 (0xC) and indata=0x"0BEBE0000CACA000" give 0xCACACACA and not BEBECACA.

I managed to make it works changing these lines :

  output_im_s <= indata((OUTPUT_WIDTH/2)+(INPUT_WIDTH/2) + div_index-1 downto
                 div_index + (INPUT_WIDTH/2));

To

output_tmp <= indata(INPUT_WIDTH-1 downto OUTPUT_WIDTH);    
output_im_s <= output_tmp((OUTPUT_WIDTH/2)+div_index-1 downto div_index);    

The problem seems to be in Yosys because simulation works with GHDL. But maybe it's a plugin issue ?

[tgingold]

It's an issue in synthesis. I am testing a fix.

Thank you for the issue.

[Martoni]

Ho great, Thanks for this fast response.