( ESNUG 371 Item 7 ) -------------------------------------------- [05/23/01]
From: Menno Spijker <menno_spijker@Mitel.COM>
Subject: Formality Can't Handle 2D Arrays -- How About Other Formal Tools?
Hi John,
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
|
|
