| |
| 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:00:42 2013 |
| |
| Loading db file '/opt/eda/iac/tools/fm/2009_06/libraries/syn/gtech.db' |
| set hdlin_ignore_full_case false |
| false |
| set hdlin_ignore_parallel_case false |
| false |
| set svf_ignore_unqualified_fsm_information true |
| true |
| set hdlin_warn_on_mismatch_message "FMR_ELAB-115 FMR_VLOG-079 FMR_VLOG-091" |
| FMR_ELAB-115 FMR_VLOG-079 FMR_VLOG-091 |
| read_verilog -container r -libname WORK -01 rtl/omsp_alu.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_alu.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Current container set to 'r' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_and_gate.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_and_gate.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_clock_gate.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_clock_gate.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_clock_module.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_clock_module.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_clock_mux.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_clock_mux.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_dbg_hwbrk.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_dbg_hwbrk.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_dbg_uart.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_dbg_uart.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_dbg.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_dbg.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_execution_unit.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_execution_unit.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_frontend.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_frontend.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_mem_backbone.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_mem_backbone.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_multiplier.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_multiplier.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_register_file.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_register_file.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_scan_mux.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_scan_mux.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_sfr.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_sfr.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_sync_cell.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_sync_cell.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_sync_reset.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_sync_reset.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_wakeup_cell.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_wakeup_cell.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/omsp_watchdog.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/omsp_watchdog.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| read_verilog -container r -libname WORK -01 rtl/openMSP430.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_defines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| Loading include file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/rtl/openMSP430_undefines.v' |
| 1 |
| set_top r:/WORK/openMSP430 |
| Setting top design to 'r:/WORK/openMSP430' |
| Status: Elaborating design openMSP430 ... |
| Status: Elaborating design omsp_clock_module ... |
| Status: Elaborating design omsp_sync_cell ... |
| Status: Elaborating design omsp_sync_reset ... |
| Status: Elaborating design omsp_frontend ... |
| Status: Elaborating design omsp_execution_unit ... |
| Status: Elaborating design omsp_register_file ... |
| Status: Elaborating design omsp_alu ... |
| Status: Elaborating design omsp_mem_backbone ... |
| Status: Elaborating design omsp_sfr ... |
| Status: Elaborating design omsp_watchdog ... |
| Status: Elaborating design omsp_multiplier ... |
| Status: Elaborating design omsp_dbg ... |
| Status: Elaborating design omsp_dbg_uart ... |
| Status: Implementing inferred operators... |
| Top design successfully set to 'r:/WORK/openMSP430' |
| Reference design set to 'r:/WORK/openMSP430' |
| 1 |
| read_verilog -container i -libname WORK -01 output/synth.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/openmsp430/output/synth.v' |
| Current container set to 'i' |
| 1 |
| read_verilog -container i -technology_library -libname TECH_WORK -01 ../scripts/sim_mul.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/scripts/sim_mul.v' |
| Building primitive models ... |
| No primitive models found. |
| 1 |
| read_verilog -container i -technology_library -libname TECH_WORK -01 ../scripts/sim_stdcells.v |
| Loading verilog file '/home/lva/vhdl/vhdl1/yosys-tests/scripts/sim_stdcells.v' |
| Building primitive models ... |
| No primitive models found. |
| 1 |
| set_top i:/WORK/openMSP430 |
| Setting top design to 'i:/WORK/openMSP430' |
| Status: Elaborating design openMSP430 ... |
| Status: Elaborating design $_OR_ ... |
| Status: Elaborating design omsp_clock_module ... |
| Status: Elaborating design $_INV_ ... |
| Status: Elaborating design $_AND_ ... |
| Status: Elaborating design $_MUX_ ... |
| Status: Elaborating design $_XOR_ ... |
| Status: Elaborating design $_DFF_PP0_ ... |
| Status: Elaborating design $_DFF_PP1_ ... |
| Status: Elaborating design omsp_sync_cell ... |
| Status: Elaborating design omsp_sync_reset ... |
| Status: Elaborating design omsp_dbg ... |
| Status: Elaborating design omsp_dbg_uart ... |
| Status: Elaborating design omsp_execution_unit ... |
| Status: Elaborating design omsp_alu ... |
| Status: Elaborating design omsp_register_file ... |
| Status: Elaborating design omsp_frontend ... |
| Status: Elaborating design omsp_mem_backbone ... |
| Status: Elaborating design omsp_multiplier ... |
| Status: Elaborating design $mul A_SIGNED=1, A_WIDTH=17, B_SIGNED=1, B_WIDTH=9, Y_WIDTH=26 ... |
| Status: Elaborating design omsp_sfr ... |
| Status: Elaborating design omsp_watchdog ... |
| Status: Implementing inferred operators... |
| Top design successfully set to 'i:/WORK/openMSP430' |
| Implementation design set to 'i:/WORK/openMSP430' |
| 1 |
| source output/fsm_info.txt |
| s0 2#00 s1 2#10 s2 2#01 s3 2#11 |
| s0 2#000 s1 2#001 s2 2#010 s3 2#100 |
| s0 2#000 s1 2#100 s2 2#010 s3 2#001 s4 2#101 s5 2#011 |
| s0 2#00000 s1 2#00001 s2 2#00010 s3 2#00100 s4 2#01000 s5 2#10000 |
| s0 2#000 s1 2#100 s2 2#010 s3 2#001 s4 2#101 s5 2#011 |
| s0 2#00000 s1 2#00001 s2 2#00010 s3 2#00100 s4 2#01000 s5 2#10000 |
| 1 |
| verify |
| Reference design is 'r:/WORK/openMSP430' |
| Implementation design is 'i:/WORK/openMSP430' |
| Status: Checking designs... |
| Status: Building verification models... |
| Status: Generating datapath components ... |
| Status: Qualifying datapath components ... |
| Status: Datapath qualification complete. |
| Status: Re-encoding block r:/WORK/openMSP430/frontend_0 (/WORK/omsp_frontend)... |
| Status: Re-encoding block r:/WORK/openMSP430/dbg_0/dbg_uart_0 (/WORK/omsp_dbg_uart)... |
| Status: Generating datapath components ... |
| Status: Qualifying datapath components ... |
| Status: Datapath qualification complete. |
| Status: Re-encoding block r:/WORK/openMSP430/dbg_0 (/WORK/omsp_dbg)... |
| Status: Generating datapath components ... |
| Status: Qualifying datapath components ... |
| Status: Datapath qualification complete. |
| Status: Matching... |
| |
| *********************************** Matching Results *********************************** |
| 744 Compare points matched by name |
| 57 Compare points matched by signature analysis |
| 0 Compare points matched by topology |
| 69 Matched primary inputs, black-box outputs |
| 7(0) Unmatched reference(implementation) compare points |
| 0(0) Unmatched reference(implementation) primary inputs, black-box outputs |
| 132(0) Unmatched reference(implementation) unread points |
| ---------------------------------------------------------------------------------------- |
| Unmatched Objects REF IMPL |
| ---------------------------------------------------------------------------------------- |
| Registers 7 0 |
| Constrained 0X 7 0 |
| **************************************************************************************** |
| |
| Info: Formality Guide Files (SVF) can improve matching performance and success by automating setup. |
| Status: Verifying... |
| |
| ********************************* Verification Results ********************************* |
| Verification SUCCEEDED |
| ---------------------- |
| Reference design: r:/WORK/openMSP430 |
| Implementation design: i:/WORK/openMSP430 |
| 801 Passing compare points |
| ---------------------------------------------------------------------------------------- |
| Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL |
| ---------------------------------------------------------------------------------------- |
| Passing (equivalent) 0 0 0 0 113 688 0 801 |
| Failing (not equivalent) 0 0 0 0 0 0 0 0 |
| Not Compared |
| Constant reg 18 0 18 |
| Unread 0 0 0 0 0 1 0 1 |
| **************************************************************************************** |
| 1 |
| # start_gui |
| exit |
| |
| Maximum memory usage for this session: 146292 KB |
| CPU usage for this session: 35.15 seconds |
| |
| Thank you for using Formality (R)! |
