( ESNUG 372 Item 8 ) -------------------------------------------- [05/31/01]
Subject: ( ESNUG 371 #7 ) Oops, Actually Formality Can Handle 2D Arrays!
> I'm using in my VHDL code 2 dimensional arrays. For example:
>
> type t_array is array(natural range <>) of std_logic_vector(7 downto 0);
> signal s_array : t_array(15 downto 0);
>
> Our formal verification tool, Formality, has a hard time with signals like
> this. Our support guy from Synopsys rewrote the 2D arrays to a 1D array:
>
> std_logic_vector(127 downto 0)
>
> Now Formality can handle the design. He recommended not to use 2D arrays
> in future designs, either in Verilog or VHDL.
>
> I find that some Synopsys tools are not that great on VHDL. DC and
> Formality still don't support all of VHDL-93. Further, some VHDL-93
> constructs that are supported by DC are not supported by Formality. So
> that makes me wonder what peoples experience is with other formal
> verification tools with respect to 2D array's.
>
> - Menno Spijker
> Mitel Semiconductor Ottawa, Canada
From: [ A Formality CAE ]
Hi, John,
Menno's code is, in fact, supported by Formality.
Here is an example that uses the VHDL type and signal exactly as submitted.
This example is fully supported in Formality:
library ieee;
use ieee.std_logic_1164.all;
USE IEEE.std_logic_unsigned.all;
entity regarray is
port( a : in std_logic_vector (7 downto 0);
clk : in std_logic;
index : in std_logic_vector(3 downto 0);
dout : out std_logic_vector (7 downto 0));
end regarray;
architecture one of regarray is
type t_array is array(natural range <>) of std_logic_vector(7 downto 0);
signal s_array : t_array(15 downto 0);
begin
process(clk)
begin
if(clk'event and clk='1') then
s_array(conv_integer(index)) <= a;
end if;
end process;
dout <= s_array(conv_integer(index));
end one;
There are however, multiple ways to code arrays in VHDL. Maybe Menno just
gave the wrong example. Currently, neither DC (2000.11) nor Formality
support the following syntax for multidimensional arrays:
type m_array is array(15 downto 0, 7 downto 0) of std_logic ;
In addition, VHDL93 support (same subset as DC) will be available with the
Formality 2001.08 release in August.
- [ A Formality CAE ]
---- ---- ---- ---- ---- ---- ----
From: Raimund Soenning <raimund.soenning@philips.com>
Dear John,
In January, while still at my former company, I made an evaluation of 3
formal verification tools (Avanti Design Verifyer, Verplex Tuxedo, Mentor
FormalPro). None of them could actually resolve the 2-D array problem
either but only when DC transformed them into 1-D arrays during synthesis.
On the other hand the problem is very easy to overcome by writing some
nice mapping rules - just one line per array. This applied for all 3 tools.
- Raimund Soenning
Philips Semiconductor Starnberg, Germany
|
|
