formality verify failed

atlandis

我在论坛下的formality Version L-2016.03-SP1 64bit，比较RTL和加密后的RTL，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也没法确定是咋回事

atlandis

回复 2# 南宫恨


这个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

atlandis

回复 2# 南宫恨


   
我debug其中一个 fail point，这两个寄存器的的输入，SL，SD也无法找到driver

atlandis

对应的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;

yangyang。

请问楼主的问题解决了吗，，我现在出现的问题是SL的值不一样，，r是0；i是1

zhaoyan0900

quizhu