SVIncCompil/Testcases/YosysOldTests/usb_phy/cache/formality.log

                            Formality (R)
                Version C-2009.06-SP3 -- Oct 19, 2009
              Copyright (c) 1988-2013 by Synopsys, Inc.
                         ALL RIGHTS RESERVED

This program is proprietary and confidential information of Synopsys, Inc.
and may be used and disclosed only as authorized in a license agreement
controlling such use and disclosure.

  ** Highlights of Formality 2009.06 **
   - DC Ultra 2009.06 optimization support
   - Debugging guidance for failing and aborted points (new command: analyze_points)
   - Power domain color highlighting for logic cone and schematic views

   * Please refer to the Formality Release Notes for details and additional enhancements

Hostname: morpheus5 (amd64)
Current time: Fri May 17 15:08:18 2013

Loading db file '/opt/eda/iac/tools/fm/2009_06/libraries/syn/gtech.db'
set hdlin_ignore_full_case false
false
set hdlin_warn_on_mismatch_message "FMR_ELAB-115 FMR_ELAB-146 FMR_ELAB-147"
FMR_ELAB-115 FMR_ELAB-146 FMR_ELAB-147
read_verilog -container r -libname WORK -01 { rtl/usb_phy.v rtl/usb_rx_phy.v rtl/usb_tx_phy.v }
Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/usb_phy.v'
Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/timescale.v'
Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/usb_rx_phy.v'
Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/timescale.v'
Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/usb_tx_phy.v'
Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/timescale.v'
Current container set to 'r'
1
set_top r:/WORK/usb_phy
Setting top design to 'r:/WORK/usb_phy'
Status:   Elaborating design usb_phy   ...  
Status:   Elaborating design usb_tx_phy   ...  
Warning: You are using the full_case directive but not all cases are covered. (File: /home/lva/vhdl/vhdl1/yosys-tests/usb_phy/rtl/usb_tx_phy.v Line: 427)  (FMR_ELAB-115)
Status:   Elaborating design usb_rx_phy   ...  
Status:  Implementing inferred operators...
Top design set to 'r:/WORK/usb_phy' with warnings
   ATTENTION: RTL interpretation messages were produced during link.
              Verification results may disagree with a logic simulator.

************ RTL Interpretation Summary ************
************ Design: r:/WORK/usb_phy
full_case interpreted (4 total, 1 with unspecified cases)
4 FMR_ELAB-115 messages interpreted    (full case interpretation)

Please refer to the Formality log file for more details,
or execute report_hdlin_mismatches.
****************************************************

Reference design set to 'r:/WORK/usb_phy'
1
read_verilog -container i -libname WORK -01 output/synth.v
Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/usb_phy/output/synth.v'
Current container set to 'i'
1
set_top i:/WORK/usb_phy
Setting top design to 'i:/WORK/usb_phy'
Status:   Elaborating design usb_phy   ...  
Status:   Elaborating design usb_rx_phy   ...  
Status:   Elaborating design usb_tx_phy   ...  
Status:  Implementing inferred operators...
Top design successfully set to 'i:/WORK/usb_phy'
Implementation design set to 'i:/WORK/usb_phy'
1
verify
Reference design is 'r:/WORK/usb_phy'
Implementation design is 'i:/WORK/usb_phy'
Status:  Checking designs...
Status:  Building verification models...
Status:  Generating datapath components ...
Status:  Qualifying datapath components ...
Status:  Datapath qualification complete.
Status:  Matching...
    
*********************************** Matching Results ***********************************    
 103 Compare points matched by name    
 13 Compare points matched by signature analysis    
 0 Compare points matched by topology    
 15 Matched primary inputs, black-box outputs    
 0(0) Unmatched reference(implementation) compare points    
 0(0) Unmatched reference(implementation) primary inputs, black-box outputs    
****************************************************************************************

    Info:  Formality Guide Files (SVF) can improve matching performance and success by automating setup.
Status:  Verifying...

************ RTL Interpretation Summary ************
************ Design: r:/WORK/usb_phy
full_case interpreted (4 total, 1 with unspecified cases)
4 FMR_ELAB-115 messages interpreted    (full case interpretation)

Please refer to the Formality log file for more details,
or execute report_hdlin_mismatches.
****************************************************


********************************* Verification Results *********************************
Verification SUCCEEDED
   ATTENTION: RTL interpretation messages were produced during link
              of reference design.
              Verification results may disagree with a logic simulator.
-----------------------------------------------------------------------
 Reference design: r:/WORK/usb_phy
 Implementation design: i:/WORK/usb_phy
 116 Passing compare points
----------------------------------------------------------------------------------------
Matched Compare Points     BBPin    Loop   BBNet     Cut    Port     DFF     LAT   TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent)           0       0       0       0      18      98       0     116
Failing (not equivalent)       0       0       0       0       0       0       0       0
****************************************************************************************
1
exit

Maximum memory usage for this session: 19652 KB
CPU usage for this session: 0.87 seconds

Thank you for using Formality (R)!