DC综合问题

新手上路哈哈哈

inout端口如何进行时序约束，这样对吗

set_input_delay -max 5 -clock clk [remove_from_collection [all_inputs] [get_ports clk]]

set_input_delay -min 2 -clock clk [remove_from_collection [all_inputs] [get_ports clk]]

set_output_delay -max 5 -clock clk [all_outputs]

set_output_delay -min 2 -clock clk [all_outputs]

这样的话，我在形式验证时，有双向端口错误。

如果不对，应该如何设置这个约束

nirvana_pear

formal过不了和约束无关

flyskyseu

形式验证和约束没有关系。
形式验证的双向端口错误是什么？是不等吗？

Lotusy

数字有双向端口吗

新手上路哈哈哈

flyskyseu 发表于 2023-12-11 17:51
形式验证和约束没有关系。
形式验证的双向端口错误是什么？是不等吗？

Status:  Verifying...
Compare point sd_BO failed (is not equivalent)
Compare point sd_DI failed (is not equivalent)

********************************* Verification Results *********************************
Verification FAILED
   ATTENTION: 2 failing compare points have unmatched undriven signals in their
                reference fan-in.  To report such failing points, use
                "report_failing_points -inputs unmatched -inputs undriven".
              To read about undriven signal handling, use
                "man verification_set_undriven_signals".
----------------------------------------------------------------------------------------
Reference design: r:/WORK/top
Implementation design: i:/WORK/top
623 Passing compare points
2 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       2       0       9     612       0     623
Failing (not equivalent)       0       0       0       0       2       0       0       2
****************************************************************************************
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.
0
显示是这个错误

新手上路哈哈哈

nirvana_pear 发表于 2023-12-11 09:23
formal过不了和约束无关

Status:  Verifying...
Compare point sd_BO failed (is not equivalent)
Compare point sd_DI failed (is not equivalent)

********************************* Verification Results *********************************
Verification FAILED
   ATTENTION: 2 failing compare points have unmatched undriven signals in their
                reference fan-in.  To report such failing points, use
                "report_failing_points -inputs unmatched -inputs undriven".
              To read about undriven signal handling, use
                "man verification_set_undriven_signals".
----------------------------------------------------------------------------------------
Reference design: r:/WORK/top
Implementation design: i:/WORK/top
623 Passing compare points
2 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       2       0       9     612       0     623
Failing (not equivalent)       0       0       0       0       2       0       0       2
****************************************************************************************
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.
0
显示是这个错误

新手上路哈哈哈

Status:  Verifying...
Compare point sd_BO failed (is not equivalent)
Compare point sd_DI failed (is not equivalent)

********************************* Verification Results *********************************
Verification FAILED
   ATTENTION: 2 failing compare points have unmatched undriven signals in their
                reference fan-in.  To report such failing points, use
                "report_failing_points -inputs unmatched -inputs undriven".
              To read about undriven signal handling, use
                "man verification_set_undriven_signals".
----------------------------------------------------------------------------------------
Reference design: r:/WORK/top
Implementation design: i:/WORK/top
623 Passing compare points
2 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       2       0       9     612       0     623
Failing (not equivalent)       0       0       0       0       2       0       0       2
****************************************************************************************
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.
0
显示是这个错误

新手上路哈哈哈

flyskyseu 发表于 2023-12-11 17:51
形式验证和约束没有关系。
形式验证的双向端口错误是什么？是不等吗？

我用这条命令就可以了

flyskyseu

你用的是BINARY:X还是0？

新手上路哈哈哈

flyskyseu 发表于 2023-12-18 11:41
你用的是BINARY:X还是0？

我用的是0