64 bits slicing problem
Closed this issue · 2 comments
Martoni commented
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 commented
It's an issue in synthesis. I am testing a fix.
Thank you for the issue.
Martoni commented
Ho great,
Thanks for this fast response.