formality verify failed
但是我在其他的服务器上跑同样的script，formal version2010 32bit，可以通过。请问2016版有问题么?
如果formal RTL和生成的netlist则两个服务器都没有问题。
set verification_verify_unread_compare_points true
set verification_failing_point_limit 0
set_app_var synopsys_auto_setup true
set_host_options -max_cores 8
read_verilog -container r -libname WORK -01 { \
../all_src/*.v \
}
set_top r:/WORK/top
read_verilog -container i -libname WORK -01 { \
../all_src_encrypt/*.v
}
set_top i:/WORK/top
match
verify
版本差异是有可能的，但是看不到log也没法确定是咋回事
这个log也看不出什么额?
Formality (R)
Version L-2016.03-SP1 for linux64 - Apr 13, 2016
Copyright (c) 1988 - 2016 Synopsys, Inc.
This software and the associated documentation are proprietary to Synopsys,
Inc. This software may only be used in accordance with the terms and conditions
of a written license agreement with Synopsys, Inc. All other use, reproduction,
or distribution of this software is strictly prohibited.
** Highlights of Formality (R) Version L-2016.03 **
- New alternate verification strategies for resolving inconclusive verifications
- Automation for deploying alternate strategies
- New command to export the mapping of reference to implementation registers
- New capability to combine PG and low power information from db libraries with Verilog functional models
* Please refer to the Formality Release Notes for details and additional enhancements
Build: 4031317
Hostname: aerospace (RHEL64)
Current time: Thu Jan 5 09:05:14 2017
Loading db file '/eda/synopsys/FM/libraries/syn/gtech.db'
set verification_verify_unread_compare_points true
true
set verification_failing_point_limit 0
0
set_app_var synopsys_auto_setup true
true
##set_host_options -max_cores 8
read_verilog -container r -libname WORK -01 { ../all_src/*.v }
Loading verilog file '/home/hnxu/jupiter_2.0/backend/all_src/rgbwpro_a2z.v'
Loading verilog file '/home/hnxu/jupiter_2.0/backend/all_src/rgbwpro_aavg.v'
.................................
Status: Elaborating design rgbwpro_doif ... Status: Elaborating design rgbwpro_mnt ...
Status: Implementing inferred operators...
Top design successfully set to 'i:/WORK/rgbwpro_top'
Implementation design set to 'i:/WORK/rgbwpro_top'
1
match
Reference design is 'r:/WORK/rgbwpro_top'
Implementation design is 'i:/WORK/rgbwpro_top'
Status: Checking designs...
Status: Building verification models...
Status: Matching...
.......................
*********************************** Matching Results ***********************************
6311 Compare points matched by name
0 Compare points matched by signature analysis
595 Compare points matched by topology
14090 Matched primary inputs, black-box outputs
27126(27126) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
2003(2003) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Registers 27126 27126
DFF 26271 26271
Constant 0 0 807
Constrained 0X 855 48
****************************************************************************************
Info: Formality Guide Files (SVF) can improve matching performance and success by automating setup.
1
verify
Reference design is 'r:/WORK/rgbwpro_top'
Implementation design is 'i:/WORK/rgbwpro_top'
*********************************** Matching Results ***********************************
6311 Compare points matched by name
0 Compare points matched by signature analysis
595 Compare points matched by topology
14090 Matched primary inputs, black-box outputs
27126(27126) Unmatched reference(implementation) compare points
0(0) Unmatched reference(implementation) primary inputs, black-box outputs
2003(2003) Unmatched reference(implementation) unread points
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Registers 27126 27126
DFF 26271 26271
Constant 0 0 807
Constrained 0X 855 48
****************************************************************************************
Status: Verifying...
..
Compare point A_u3_rndt/u1_pl3/u02_A2Z/u2_div_us/O0_reg failed (is not equivalent)
Compare point A_u3_rndt/u1_pl3/u02_A2Z/u3_div/O0_reg failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u0_p4p/u2_stty/u0_idx0/OO_reg[0] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u0_p4p/u2_stty/u0_idx1/OO_reg[0] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u0_p4p/u3_sttx/u0_idx1/OO_reg[0] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[1] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[2] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[3] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[4] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[5] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[6] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/OOOl_reg[7] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/o11_reg[10] failed (is not equivalent)
Compare point A_u3_rndt/u6_cat/u1_pof/o11_reg[9] failed (is not equivalent)
***************************** Synopsys Auto Setup Summary ******************************
！ Synopsys Auto Setup Mode was enabled. ！
！ Verification results are valid assuming the following setup constraints: ！
### RTL Interpretation Setup
set hdlin_ignore_parallel_case false
set hdlin_ignore_full_case false
set hdlin_error_on_mismatch_message false
set hdlin_ignore_embedded_configuration true
### Undriven Signal Handling Setup
set verification_set_undriven_signals synthesis
### Test Logic Setup
set verification_verify_directly_undriven_output false
For details see report_dont_verify_points and report_constants
For further details on Synopsys Auto Setup Mode: Type man synopsys_auto_setup
****************************************************************************************
********************************* Verification Results *********************************
Verification FAILED
ATTENTION: synopsys_auto_setup mode was enabled.
See Synopsys Auto Setup Summary for details.
----------------------------------------------------------
Reference design: r:/WORK/rgbwpro_top
Implementation design: i:/WORK/rgbwpro_top
2007 Passing compare points
34028 Failing compare points
0 Aborted compare points
0 Unverified compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 854 1153 0 2007
Failing (not equivalent) 0 0 0 0 146 4753 0 4899
****************************************************************************************
Info: Try the analyze_points command to see if Formality can determine potential
causes, or suggest next steps for a FAILED or INCONCLUSIVE verification.
See the man page for analyze_points usage and options.
Info: Formality Guide Files (SVF) can improve verification success by automating setup.
0
#quit
我debug其中一个 fail point，这两个寄存器的的输入，SL，SD也无法找到driver
对应的RTL
reg [8:0] sram_addr;
always @ (posedge i_clk or negedge i_rst_n)
if (~i_rst_n)
sram_addr <= #UDLY 'h0;
else if (o_last_flag || (~i_vsync))
sram_addr <= #UDLY 'h0;
else if (o_sram_ceb)
sram_addr <= #UDLY 'h0;
else if(((~o_sram_web)|(dot_cnt[0]))&& i_m_buf_bp_n)
sram_addr <= #UDLY o_sram_addr+ 'h1;