Formality: netlist vs. netlist (or RTL vs. netlist)

[ESD_UNIVR]

netlist vs netlist

Dear all,
I'd like to use Formality as follows:

RTL       DUV --> manipulation_tool --> DUV*
           (VHDL)                     (VHDL)
              |                          |
              |                          |
              v                          v
          dc_shell                   dc_shell
              |                          |
              |                          |
              v                          v
net        ~DUV~ -----> formality <---- ~DUV*~
list      (VHDL)                      (VHDL)

Where:
- DUV is my design in VHDL
- manipulation_tool is a tool which performs some RTL-description manipulation
- ~DUV~ is my synthesized design
- DUV* and ~DUV*~ are the modified design and the corresponding netlist

Can I use Formality to perform this equivalence analysis? And do you have any advices, warnings or remarks for me?

Actually I am not using the SVF file, I suppose this is the reason of some mismatches.

Our laboratory provides both 2004.12-SP1 and 2008.09-SP1 Formality version, I assume it is better the recent one. Right?

As well, we have also Design Compiler (2003.06, 2004.12, 2005.09, 2008.09-SP1 and 2008.09-SP2). Which version of DC do I have to use with the Formality? Does it not matter?

Finally, :!: very important :!: , do I have to enable/disable some specific feature of DC to use Formality safely on the generated netlists?

 

[ESD_UNIVR]

rtl and netlist

I forgot to ask if it is safe to compare netlist vs. netlist by using Formality.

 

[sunilbudumuru]

formality rtl vs rtl

Hello friend,

can u tell us more about manipulation_tool .
Will tht changes/modifies the netlist (in terms of functionality) by any means.

-Sunil B

 

[ESD_UNIVR]

netlist vs rtl

This is a simple example of manipulation

Original code

process(clock,reset)
  variable state: integer range 7 downto 0;
begin
  if reset='1' then
    stato:=a;
    outp<='0';
    overflw<='0';
  elsif clock'event and clock='1' then
    case state is
      when a =>
        if line1='1' and line2='1' then
          state:=f;
        else
          state:=b ;
        end if;
        outp <= line1 xor line2;
        overflw <= '0' ;
      when e =>
        if line1='1' and line2='1' then
          state:=f;
        else
          state:=b ;
        end if;
        outp <= line1 xor line2;
        overflw <= '1';
      ...
    end case;
  end if;
end process;

Manipulated code

vhdl_process : PROCESS(clock,reset)
  VARIABLE stato : INTEGER RANGE 7 DOWNTO 0 := 0;
BEGIN
  IF (reset = '1') THEN
    stato := a;
    outp <= '0';
    overflw <= '0';
  ELSIF clock'event and clock='1' THEN
    CASE stato IS
      WHEN a =>
        IF ((NOT (reset = '1')) AND (NOT ((line1 = '1') AND (line2 = '1')))) THEN
          stato := b;
          outp <= (line1 XOR line2);
          overflw <= '0';
        ELSIF ((NOT (reset = '1')) AND ((line1 = '1') AND (line2 = '1'))) THEN
          stato := f;
          outp <= (line1 XOR line2);
          overflw <= '0';
        END IF;
      WHEN e =>
        IF ((NOT (reset = '1')) AND (NOT ((line1 = '1') AND (line2 = '1')))) THEN
          stato := b;
          outp <= (line1 XOR line2);
          overflw <= '1';
        ELSIF ((NOT (reset = '1')) AND ((line1 = '1') AND (line2 = '1'))) THEN
          stato := f;
          outp <= (line1 XOR line2);
          overflw <= '1';
        END IF;
       ...
     END CASE;
  END IF;
END PROCESS;

As you can see the RTL core is just reorganized. But the Formality says to me that the two netlist are not equivalent. Why? Where is my error?

 

[pra]

netlist vs rtl code

The code that you shown is different when you do synthesize and it optimizes further. During this process it may change the logic to simple one....

Verplex is good to use for these kind of problem.

I prefer first do Netlist vs RTL afterwards check with Netlist vs Netlist

 

[ESD_UNIVR]

formality reset

I assume that the behavior of the code is the same, but how can I verify that?

If the netlist vs netlist fails, can I check RTL vs RTL?

RTL       DUV --> manipulation_tool --> DUV*
           (VHDL)                     (VHDL) 
             |                          |
             |                          |
             -------> formality <-------

In other words, how can I use Formality to verify the functional equivalence of two descriptions?

 

[littlebu]

rtl to netlist

maybe formality comparing netlist is care name or UPcase and downcase. you can check the name change of DFF after do manipulation_tool.