| |
| 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:07:51 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/aes.v rtl/byte_mixcolum.v rtl/keysched.v rtl/mixcolum.v rtl/sbox.v rtl/subbytes.v rtl/word_mixcolum.v } |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/aes.v' |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/byte_mixcolum.v' |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/keysched.v' |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/mixcolum.v' |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/sbox.v' |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/subbytes.v' |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/word_mixcolum.v' |
| Current container set to 'r' |
| 1 |
| set_top r:/WORK/aes |
| Setting top design to 'r:/WORK/aes' |
| Status: Elaborating design aes ... |
| Status: Elaborating design sbox ... |
| Status: Elaborating design subbytes ... |
| Warning: Index may take values outside array bound, may cause simulation mismatch .. (File: /home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/subbytes.v Line: 246) (FMR_ELAB-147) |
| Warning: Out of range write possible, may cause simulation and synthesis mismatch. (File: /home/lva/vhdl/vhdl1/yosys-tests/systemcaes/rtl/subbytes.v Line: 247) (FMR_ELAB-146) |
| Status: Elaborating design mixcolum ... |
| Status: Elaborating design word_mixcolum ... |
| Status: Elaborating design byte_mixcolum ... |
| Status: Elaborating design keysched ... |
| Status: Implementing inferred operators... |
| Top design set to 'r:/WORK/aes' with warnings |
| ATTENTION: RTL interpretation messages were produced during link. |
| Verification results may disagree with a logic simulator. |
| |
| ************ RTL Interpretation Summary ************ |
| ************ Design: r:/WORK/aes |
| 1 FMR_ELAB-147 message produced |
| |
| Please refer to the Formality log file for more details, |
| or execute report_hdlin_mismatches. |
| **************************************************** |
| |
| Reference design set to 'r:/WORK/aes' |
| 1 |
| read_verilog -container i -libname WORK -01 output/synth.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/systemcaes/output/synth.v' |
| Current container set to 'i' |
| 1 |
| set_top i:/WORK/aes |
| Setting top design to 'i:/WORK/aes' |
| Status: Elaborating design aes ... |
| Status: Elaborating design keysched ... |
| Status: Elaborating design mixcolum ... |
| Status: Elaborating design word_mixcolum ... |
| Status: Elaborating design byte_mixcolum ... |
| Status: Elaborating design sbox ... |
| Status: Elaborating design subbytes ... |
| Status: Implementing inferred operators... |
| Top design successfully set to 'i:/WORK/aes' |
| Implementation design set to 'i:/WORK/aes' |
| 1 |
| verify |
| Reference design is 'r:/WORK/aes' |
| Implementation design is 'i:/WORK/aes' |
| Status: Checking designs... |
| Status: Building verification models... |
| Status: Generating datapath components ... |
| Status: Qualifying datapath components ... |
| Status: Datapath qualification complete. |
| Status: Matching... |
| |
| *********************************** Matching Results *********************************** |
| 443 Compare points matched by name |
| 356 Compare points matched by signature analysis |
| 0 Compare points matched by topology |
| 260 Matched primary inputs, black-box outputs |
| 0(0) Unmatched reference(implementation) compare points |
| 0(0) Unmatched reference(implementation) primary inputs, black-box outputs |
| 639(0) Unmatched reference(implementation) unread points |
| **************************************************************************************** |
| |
| Info: Formality Guide Files (SVF) can improve matching performance and success by automating setup. |
| Status: Verifying... |
| |
| ************ RTL Interpretation Summary ************ |
| ************ Design: r:/WORK/aes |
| 1 FMR_ELAB-147 message produced |
| |
| 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/aes |
| Implementation design: i:/WORK/aes |
| 799 Passing compare points |
| ---------------------------------------------------------------------------------------- |
| Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL |
| ---------------------------------------------------------------------------------------- |
| Passing (equivalent) 0 0 0 0 129 670 0 799 |
| Failing (not equivalent) 0 0 0 0 0 0 0 0 |
| Not Compared |
| Unread 0 0 0 0 0 8 0 8 |
| **************************************************************************************** |
| 1 |
| exit |
| |
| Maximum memory usage for this session: 134532 KB |
| CPU usage for this session: 26.69 seconds |
| |
| Thank you for using Formality (R)! |