Formal Verification 
Author Message
 Formal Verification

Hi,

We are currently in the process of evaluating Synopsys Formality and
Verplex Tuxedo-LEC for the formal verification effort.  Is there anybody
who has used
these tools and could recommend one or the other ?

Thanks
Mike



Sat, 31 Jan 2004 23:13:16 GMT  
 Formal Verification
Quote:

> Hi,

> We are currently in the process of evaluating Synopsys Formality and
> Verplex Tuxedo-LEC for the formal verification effort.  Is there anybody
> who has used
> these tools and could recommend one or the other ?

Isn't formality only an equivalence checker?

Greetings!
Volker
--
They laughed at Galileo.  They laughed at Copernicus.  They laughed at
Columbus. But remember, they also laughed at Bozo the Clown.



Sun, 01 Feb 2004 01:07:40 GMT  
 Formal Verification
Hi,
I am using both Tuxedo-LEC and DV (by Avanti, formerly Chrysalis).  Never
used formality before, and
since I verify results generated by Synopsys synthesis tools, i prefer to
use an independent verification
tool.
As for the ones I use, Tuxedo-LEC is 10x faster than DV. However, if it
comes to complex arithmetics and
messy tristate logic, both of these tools may encounter situations where
they cannot complete
verification. Tuxedo-LEC is also more expensice than DV.
Robert


Quote:
> Hi,

> We are currently in the process of evaluating Synopsys Formality and
> Verplex Tuxedo-LEC for the formal verification effort.  Is there anybody
> who has used
> these tools and could recommend one or the other ?

> Thanks
> Mike



Fri, 06 Feb 2004 20:47:16 GMT  
 Formal Verification
Hi,

I have two questions about Tuxedo-LEC. Can anyone clarify them for me?

(1) What library formats (.v, .lib, .db) does Tuxedo-LEC support?  I
know Formality can support all of them.
(2) I have a mixed Verilog/VHDL RTL design, i.e. some parts of the
design are coded in Verilog, other parts are coded in VHDL.  Can
Tuxedo-LEC read in this design to compare with its gate-level netlist?
 How to do this?

Thanks,

Quote:

> Hi,
> I am using both Tuxedo-LEC and DV (by Avanti, formerly Chrysalis).  Never
> used formality before, and
> since I verify results generated by Synopsys synthesis tools, i prefer to
> use an independent verification
> tool.
> As for the ones I use, Tuxedo-LEC is 10x faster than DV. However, if it
> comes to complex arithmetics and
> messy tristate logic, both of these tools may encounter situations where
> they cannot complete
> verification. Tuxedo-LEC is also more expensice than DV.
> Robert



> > Hi,

> > We are currently in the process of evaluating Synopsys Formality and
> > Verplex Tuxedo-LEC for the formal verification effort.  Is there anybody
> > who has used
> > these tools and could recommend one or the other ?

> > Thanks
> > Mike



Sat, 07 Feb 2004 09:31:01 GMT  
 Formal Verification

Quote:

> Hi,

> I have two questions about Tuxedo-LEC. Can anyone clarify them for me?

> (1) What library formats (.v, .lib, .db) does Tuxedo-LEC support?  I
> know Formality can support all of them.

Tuxedo-LEC supports .v,.lib. It does not support .db format for libraries.

Regards,
Vikas



Sat, 07 Feb 2004 13:00:41 GMT  
 Formal Verification

Quote:


> > Verplex Tuxedo-LEC for the formal verification effort.  Is there anybody
> > who has used
> > these tools and could recommend one or the other ?
> Isn't formality only an equivalence checker?

Formality claims to be a bit more than only equivalence check, but is
not realy model checker.

Formal verification is not only model checking. Model checking is only a
subset, of fv, as well as equivalence checking and sequentiell checking.

bye Thomas

--
Thomas Stanka      
Bosch SatCom GmbH           UC-RA/EMD4 s/UC-RA/BC
Gerberstr. 49              Tel. +49 7191 930-1690
Zi. 10/528                Fax. +49 7191 930-21690      



Sat, 07 Feb 2004 16:43:55 GMT  
 Formal Verification
Hi,

Mentor's FormalPro can handle mixed Verilog/VHDL RTL designs and will allow
you to do your RTL<>gate checking
(http://www.mentor.com/press_releases/jul01/formalpro_mixed_hdl_pr.html)

It supports .v, .lib and fastscan libraries.

For more info have a look at
http://www.mentor.com/formalpro/

regards

Nigel Elliot
Mentor Graphics (UK)


Quote:
> Hi,

> I have two questions about Tuxedo-LEC. Can anyone clarify them for me?

> (1) What library formats (.v, .lib, .db) does Tuxedo-LEC support?  I
> know Formality can support all of them.
> (2) I have a mixed Verilog/VHDL RTL design, i.e. some parts of the
> design are coded in Verilog, other parts are coded in VHDL.  Can
> Tuxedo-LEC read in this design to compare with its gate-level netlist?
>  How to do this?

> Thanks,




Quote:
> > Hi,
> > I am using both Tuxedo-LEC and DV (by Avanti, formerly Chrysalis).
Never
> > used formality before, and
> > since I verify results generated by Synopsys synthesis tools, i prefer
to
> > use an independent verification
> > tool.
> > As for the ones I use, Tuxedo-LEC is 10x faster than DV. However, if it
> > comes to complex arithmetics and
> > messy tristate logic, both of these tools may encounter situations where
> > they cannot complete
> > verification. Tuxedo-LEC is also more expensice than DV.
> > Robert



> > > Hi,

> > > We are currently in the process of evaluating Synopsys Formality and
> > > Verplex Tuxedo-LEC for the formal verification effort.  Is there
anybody
> > > who has used
> > > these tools and could recommend one or the other ?

> > > Thanks
> > > Mike



Sun, 08 Feb 2004 16:52:45 GMT  
 Formal Verification
Your comment concerning independence is frequently expressed in
relation to the Formality product, but it is a misconception. When
Formality was first released, a snapshot of the DC RTL Reader was
used. However, in 1999 the Formality team created a new, completely
independent Verilog reader for a truly autonomous solution. Synopsys
has also focused development on performance and capacity improvements.
I look forward to Mike's posting of the results.

Robert Vallelunga
Synopsys

Quote:

> Hi,
> I am using both Tuxedo-LEC and DV (by Avanti, formerly Chrysalis).  Never
> used formality before, and
> since I verify results generated by Synopsys synthesis tools, i prefer to
> use an independent verification
> tool.
> As for the ones I use, Tuxedo-LEC is 10x faster than DV. However, if it
> comes to complex arithmetics and
> messy tristate logic, both of these tools may encounter situations where
> they cannot complete
> verification. Tuxedo-LEC is also more expensice than DV.
> Robert



> > Hi,

> > We are currently in the process of evaluating Synopsys Formality and
> > Verplex Tuxedo-LEC for the formal verification effort.  Is there anybody
> > who has used
> > these tools and could recommend one or the other ?

> > Thanks
> > Mike



Sat, 14 Feb 2004 07:25:42 GMT  
 Formal Verification

Quote:
> (2) I have a mixed Verilog/VHDL RTL design, i.e. some parts of the
> design are coded in Verilog, other parts are coded in VHDL.  Can
> Tuxedo-LEC read in this design to compare with its gate-level netlist?
>  How to do this?

Yes. LEC handles mixed language designs easily.  It is just part of
reading the design.


Wed, 24 Mar 2004 12:31:03 GMT  
 Formal Verification

Quote:

> > (2) I have a mixed Verilog/VHDL RTL design, i.e. some parts of the
> > design are coded in Verilog, other parts are coded in VHDL.  Can
> > Tuxedo-LEC read in this design to compare with its gate-level netlist?
> >  How to do this?
> Yes. LEC handles mixed language designs easily.  It is just part of
> reading the design.

In Verplex-LEC, if you want to read mixed level, VHDL & Verilog
designs use the -noelaborate switch while reading in each of the
type of files (verilog or vhdl). Finally, after you have read all
of the designs in; type "elaborate design" to build the complete
design.


information on how to do this.

Regards

Central Apps Engineering Manager
Verplex Systems Inc



Thu, 25 Mar 2004 04:21:56 GMT  
 
 [ 10 post ] 

 Relevant Pages 

1. BACUP meeting: Formal Verification, Physical Verification; SourceLink

2. BACUP meeting: Formal Verification, Physical Verification; SourceLink

3. Formal verification methods for OOPS

4. Functional programming languages & formal verification

5. IBM/Israel: Open Positions in Functional Formal Verification

6. Formal verification of one-hot state machine.

7. Formal verification

8. Formal verification and Static Timing

9. Advertisement: EDA Jobs (Formal Verification)

10. MA - Employment - Formal Verification

11. Formal verification

12. Formal verification

 

 
Powered by phpBB® Forum Software