( 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