cancel
Showing results for 
Show  only  | Search instead for 
Did you mean: 
Highlighted
Observer
Observer
4,757 Views
Registered: ‎09-21-2011

Netgen and Formality for formal verification

Jump to solution

Hello,

 

I'm trying to use Netgen to formally verify a design synthesized with Xilinx tools in Synopsys Formality.  I have taken a sample design and run it through Translate and passed the resulting .ngd file through Netgen with the command:

 

netgen -ecn formality design.ngd

The resulting verilog file references the Unisim library with instances of X_XOR2, X_FF, etc.  How do I get this library into Formality?  I can't find an option to compile the library for Synopsys in any format Formality will accept and grabbing the simulation source from the Xilinx install location fails to compile in Formality.

 

 

Thanks,

JoRyTe

 

 

 

1 Solution

Accepted Solutions
Highlighted
Observer
Observer
5,528 Views
Registered: ‎09-21-2011

For others' benefit, here is the solution.

 

Verilog source files for the Unisims/Simprims libraries is available with the Xilinx install for >=12.1 at "%Xilinx%/verilog/xeclib/".

 

These files are not synthesizable and can only be interpreted as a technology library.  Synopsys Library Compiler can read these files to generate a .db technology library, if you have a Library Compiler license.

 

In Synopsys Formality, the verilog files can be loaded into your container by adding all of the source files as a "technology library" instead of into your source library "work" ("Read Design Files" tab -> "Options..." button -> "Library type" tab -> "Read technology library files into library:" radio button).  The library source files will not successfully compile as a source library but they are accepted fine as a technology library.  Since you can only load files to one library at a time, you have to load the files for each technology/source library in a seperate transaction.

 

 

 

 

JoRyTe

 

View solution in original post

1 Reply
Highlighted
Observer
Observer
5,529 Views
Registered: ‎09-21-2011

For others' benefit, here is the solution.

 

Verilog source files for the Unisims/Simprims libraries is available with the Xilinx install for >=12.1 at "%Xilinx%/verilog/xeclib/".

 

These files are not synthesizable and can only be interpreted as a technology library.  Synopsys Library Compiler can read these files to generate a .db technology library, if you have a Library Compiler license.

 

In Synopsys Formality, the verilog files can be loaded into your container by adding all of the source files as a "technology library" instead of into your source library "work" ("Read Design Files" tab -> "Options..." button -> "Library type" tab -> "Read technology library files into library:" radio button).  The library source files will not successfully compile as a source library but they are accepted fine as a technology library.  Since you can only load files to one library at a time, you have to load the files for each technology/source library in a seperate transaction.

 

 

 

 

JoRyTe

 

View solution in original post