Verilog硬件仿真过程中出现的X态总结

preview
试读
34页
编程语言
需积分: 0 6 下载量 183 浏览量 更新于2024-05-23 收藏 402KB PDF 举报
### Verilog硬件仿真过程中出现的X态总结 #### 摘要 在Verilog硬件描述语言（HDL）中，“X”状态代表不确定值或未知值。这种状态可能由多种因素引起，例如信号未初始化、逻辑操作中的未知输入等。在RTL级（寄存器传输级）仿真中，“X”状态可能会导致仿真结果与实际硬件行为不一致，隐藏潜在的设计缺陷。“X”状态的问题在于它们可以被仿真工具忽略或误处理，从而导致仿真通过但实际上存在错误的情况。本文将深入探讨“X”状态对Verilog设计的影响，并提供解决这些问题的方法。 #### 一、引言 ##### 1.1 目标：语义严谨的IP设计 随着集成电路设计复杂度的不断增加，确保设计的正确性变得尤为重要。语义严谨的IP（知识产权）设计意味着设计能够准确地反映其预期功能，并且能够在不同的仿真环境中表现一致。然而，“X”状态的存在往往成为这一目标实现的障碍。 ##### 1.2 如何阅读本文 本文旨在为读者提供关于“X”状态的基础知识、问题案例以及应对策略。文章首先介绍“X”状态的基本概念及其对设计带来的影响，随后通过具体示例说明如何识别和避免这些陷阱，并给出实用的编码建议和工具配置指南。 #### 二、“X”状态的概念与危害 “X”状态是Verilog HDL中的一种特殊值，通常表示信号或变量的值未知或不确定。它可能出现在以下几个场景中： 1. **信号未初始化**：如果一个信号没有被明确初始化，则默认为“X”。 2. **逻辑运算中的未知输入**：当逻辑运算的某个输入为“X”时，输出也可能变为“X”。 3. **非确定性条件下的计算**：在条件语句中，如果某个条件无法确定，则可能产生“X”状态。 ##### “X”状态的危害 1. **模拟结果不准确**：“X”状态可能导致仿真结果与实际硬件行为不符。 2. **错误的验证结论**：由于“X”状态的存在，即使设计中有错误，仿真也可能报告成功。 3. **难以追踪的问题**：由于“X”状态在设计流程中的传播特性，问题的根源很难定位。 #### 三、“X”状态的案例分析 本文通过几个典型的案例来展示“X”状态如何在设计中产生并导致问题： 1. **案例1：信号未初始化** - 描述：在一个简单的组合逻辑电路中，假设有一个信号`a`未被初始化。 - 结果：当使用该信号进行逻辑运算时，结果可能会变成“X”，即使其他输入均为已知值。 2. **案例2：逻辑运算中的未知输入** - 描述：考虑一个与门，其中一个输入始终为“X”。 - 结果：不论另一个输入为何值，输出都将被认定为“X”。 #### 四、解决策略 针对“X”状态的问题，本文提出了以下几种解决方案： 1. **编码规范**： - 明确初始化所有信号。 - 使用条件语句确保在所有情况下都有定义。 2. **工具配置**： - 修改仿真工具的设置，使其能检测到“X”状态。 - 在形式化验证工具中配置检查规则，以便于发现潜在的“X”状态问题。 3. **设计审查**： - 定期进行代码审查，确保符合编码规范。 - 使用静态分析工具辅助查找潜在的“X”状态。 #### 五、结语 在现代EDA工具的支持下，尽管“X”状态的处理变得更加复杂，但通过遵循良好的编码实践、合理配置工具参数以及实施严格的设计审查机制，我们仍然可以有效地管理这一挑战。对于所有依赖EDA工具进行仿真、代码覆盖率分析、综合及形式化验证的工程师而言，了解并掌握如何处理“X”状态至关重要。
The Dangers of Living with an X
(bugs hidden in your Verilog)
Version 1.1 (14
th
October, 2003)
Mike Turpin
Principal Verification Engineer
ARM Ltd., Cambridge, UK
Mike.Turpin@arm.com
ABSTRACT
The semantics of X in Verilog RTL are extremely dangerous as RTL bugs can be masked, allowing
RTL simulations to incorrectly pass where netlist simulations can fail. Such X-bugs are often missed
because formal equivalence checkers are configured to ignore them, which is a particular concern given
that equivalence checking is fast replacing netlist simulations. This paper gives examples of such
problems in order to raise awareness of X issues in many different parts of the design flow, which are
often poorly understood by RTL designers and EDA vendors alike. It gives practical advice on how to
overcome X issues in new designs (including good coding styles) and techniques to investigate them in
existing designs (including automated formal proofs). New terminology is introduced to differentiate
subtle interpretations of X by EDA tools, along with recommendations to avoid problems. In particular,
this paper describes how to change the default settings of equivalence checkers to find hidden bugs (that
are otherwise far too sneaky to detect). In short, if you are using EDA tools for simulation, code-
coverage, synthesis or equivalence checking, you must be aware of the problems and solutions
described in this paper.
Version 1.1 (14
th
October 2003) The Dangers of Living with an X 2
Table of Contents
1 INTRODUCTION ...................................................................................................................................................................4
1.1 GOAL: SEMANTICALLY-RIGOROUS IP.........................................................................................................................4
1.2 HOW TO READ THIS PAPER..........................................................................................................................................5
1.3 HISTORY OF THIS PAPER...............................................................................................................................................5
2 WHAT DOES X MEAN?.......................................................................................................................................................5
2.1 SYNTHESIS SEMANTICS: DON’T-CARE........................................................................................................................5
2.2 SIMULATION SEMANTICS: UNKNOWN .........................................................................................................................6
2.3 SIMULATION SEMANTICS: WILDCARD FOR CASEX AND CASEZ..............................................................................7
2.4 EQUIVALENCE CHECKING: 2-STATE CONSISTENCY OR STRICT 2-STATE EQUALITY.............................................8
2.5 FORMAL PROPERTY CHECKING: 2-STATE SEQUENTIAL...........................................................................................9
3 WHY ARE X’S USED? ........................................................................................................................................................10
3.1 IMPROVED SYNTHESIS (DON’T-CARES FOR MINIMIZATION)................................................................................10
3.2 IMPROVED VERIFICATION (X-INSERTION AND X-PROPAGATION)......................................................................10
4 WHY ARE X’S DANGEROUS?.........................................................................................................................................10
4.1 BUGS MISSED BY RTL SIMULATIONS........................................................................................................................10
4.2 BUGS MISSED BY EQUIVALENCE CHECKING............................................................................................................14
4.3 MISLEADING CODE COVERAGE..................................................................................................................................19
5 WHY ARE X’S INEFFICIENT?..........................................................................................................................................20
5.1 UNNECESSARY X’S IN NETLIST SIMULATIONS.......................................................................................................20
5.2 NON-MINIMAL SYNTHESIS OF DON’T-CARES.........................................................................................................21
5.3 LIMITED SPEEDUP WITH 2-STATE SIMULATION..................................................................................................24
5.4 SLOWER FORMAL VERIFICATION.............................................................................................................................24
6 HOW TO FIND DANGEROUS X’S ..................................................................................................................................25
6.1 ADDITIONAL SIMULATIONS......................................................................................................................................25
6.2 RTL CODE INSPECTION ...............................................................................................................................................26
6.3 DETECTING X’S WITH ASSERTIONS..........................................................................................................................26
6.4 CHANGE DEFAULT SETTINGS OF EQUIVALENCE CHECKERS ...............................................................................27
6.5 AUTOMATIC FORMAL PROOFS OF UNREACHABLE (DEADCODE) ASSIGNMENTS.............................................27
6.6 INTERACTIVE FORMAL PROPERTY CHECKING.......................................................................................................28
6.7 NETLIST SIMULATIONS...............................................................................................................................................29
7 HOW TO AVOID DANGEROUS X’S ..............................................................................................................................29
7.1 GOOD RTL CODING PRACTICE ...................................................................................................................................29
Version 1.1 (14
th
October 2003) The Dangers of Living with an X 3
7.2 REMOVING REACHABLE DON'T-CARE X-ASSIGNMENTS........................................................................................30
7.3 REPLACING X-INSERTION WITH ASSERTIONS........................................................................................................30
7.4 ENABLING X-PROPAGATION......................................................................................................................................30
7.5 AVOIDING UN-INITIALIZED REGISTERS...................................................................................................................30
7.6 FUTURE: SYSTEM VERILOG AND VERILOG 2XXX ...................................................................................................31
8 CONCLUSIONS ...................................................................................................................................................................31
9 TOP-TEN RECOMMENDATIONS ...................................................................................................................................32
10 ACKNOWLEDGEMENTS ..............................................................................................................................................33
11 REFERENCES ...................................................................................................................................................................34
Version 1.1 (14
th
October 2003) The Dangers of Living with an X 4
1 Introduction
The aim of this paper is to raise awareness of dangerous X issues in Verilog RTL and introduce techniques to analyze
otherwise undetected bugs in RTL designs. New terminology is used to distinguish subtle X semantic problems,
illustrated with simple examples that accurately reflect our experience of real problems found by ARM.
Some of these issues have already been raised by Bening [Bening 99], Galbi [Galbi 02], Foster [Foster 03] and other
references in section 11. What’s new in this paper is the revelation that you can actually find most hidden X-bugs
with equivalence checkers, providing you configure them to be sensitive to X issues. This paper also describes how
to use formal property checking to determine which X’s are safe and which are dangerous (and should therefore be
removed from your RTL). For X-bugs that cannot be found by formal verification, RTL coding guidelines are given.
Many engineers have polarized views on X’s, some seeing them as a good thing (e.g. for synthesis or X-
propagation) and others believing them to be an intrinsically bad idea, since they can mask real design bugs, and
should never be used. This paper argues against the widespread use of X’s, particularly for don’t-cares, but also
shows how selective use of X’s can improve design and verification (e.g. it recommends that every case default
assigns X).
Understanding problems caused by X semantics is extremely important. Many designers are blissfully unaware of the
issues around X, which can have devastating effects on many different parts of the design flow including:
1. RTL Simulation: X semantics in RTL can mask bugs - expensive validation tests can pass because they are
not being used effectively to stress the design.
2. Code Coverage: X semantics in RTL can give both optimistic results (i.e. claims a branch is covered when
it’s unreachable) and pessimistic results (i.e. claims a coverage hole when it’s reachable)
3. Equivalence Checking: all too often, equivalence checkers will miss differences in RTL and netlist
simulations caused by subtle X semantics (normally due to incorrect usage, even with default behavior)
4. Synthesis: designers often rely on don’t-cares to produce efficient logic, but can be disappointed with their
non-minimal results and long critical paths
Often due to limited understanding of X issues, bugs can be missed and left in the shipped product (discovery then
is far more expensive) or left dormant - only to reappear when a new version of your synthesis tool chooses a
different logic minimization!
As verification is 70% of the work, the risk of adding an undetected bug (which could result in a costly silicon re-
spin) should outweigh any general improvement to logic minimization. Time saved from verification can be used to
help improve any critical paths in the synthesis by careful consideration of the RTL (especially as adding don’t-cares
will not necessarily improve things as you may expect).
1.1 Goal: Semantically-Rigorous IP
ARM is keen to promote good coding styles and techniques to ensure semantically rigorous designs i.e. identical
semantics throughout the design flow. ARM has recently undertaken a lot of work in this area, including extensive
use of formal verification techniques, to avoid such problems on the latest ARM1136J(F)-S
TM
core. ARM’s IP is
integrated into many different designs so the impact of our RTL quality is magnified many times – as highlighted by a
quote from Harry Foster [Foster 03]:
“What about restricting the designer’s coding style to ensure semantic consistency? Although this would
be the ideal situation, … many of today’s designs involve integrating other organizations’ intellectual
property (IP) cores, as well as existing legacy code. … All it takes to ruin your semantically consistent
coded RTL is for someone else’s IP to drive an X value into your pure RTL.”
This paper has therefore been written to promote awareness of X-issues both internally at ARM and externally (for
designers and EDA vendors). It gives a detailed account of many lessons learned, and provides guidance on how to
design semantically rigorous RTL. Simple examples are given to illustrate sometimes complex problems, but each is
Version 1.1 (14
th
October 2003) The Dangers of Living with an X 5
based on our experience of real problems. This paper contains recommended practice that will be new to most
engineers, e.g. how many people change the default X-settings of formal equivalence checkers to avoid missing
bugs?
1.2 How to Read this Paper
As this paper covers a lot of material, some readers may prefer to start by reading the ten recommendations in section
9. If you’re already following these then you’re done and your RTL should be tolerant of X’s. However, most RTL
designs contain reachable X-assignments and so the majority of readers will have an incentive to read the other
sections too (at least as reference material). The formal techniques described in section 6.5 will be new to most
readers, but these should not be daunting in any way (if you can run an RTL linter you can run these automatic
proofs). There is some repetition in the paper, so that each section can be read in isolation as reference material.
1.3 History of this Paper
Version 1.0 (12
th
August 2003). Technical Committee Award winning paper at Boston SNUG (8
th
September 2003).
Version 1.1 (14
th
October 2003). Added section 4.1.1 (Latch Behavior in RTL Simulation), improved RTL coding rules
in section 7.1, and made some corrections and improvements from feedback at SNUG.
2 What Does X Mean?
This section explains the Verilog semantics of X for different parts of the design flow. The most worrying thing is that
there are different semantics!
Engineers are taught about two X-semantics, don’t-care for synthesis and unknown for simulation. The overloading
of X in Verilog to cover different concepts often causes misunderstandings and can lead to hidden bugs in your RTL,
as detailed in section 4. To help understand subtle X-semantic issues, this paper uses the terminology below to
compare and contrast different semantics of X.
1. Don’t-Care: Synthesis semantics (not important if assignment is 0 or 1, allowing better minimization)
2. Unknown: Simulation semantics (not known if value is 0 or 1, but evaluation will take just one path)
3. Wildcard: Simulation semantics (specific to casex and casez statements in Verilog RTL)
4. 2-State Consistency/Equality: Equivalence Checking semantics (try both X=0 and X=1 paths for every X)
5. 2-State Sequential: Property Checking semantics (try both X=0 and X=1 paths and sequences for every X)
Formal tools will try and fail the design by stressing every X with both 0 and 1, so a pass is an exhaustive verification
of all possible 2-state (i.e. 0 or 1) settings of X’s (see Figure 2 for an illustration of this). Equivalence checking is a
purely combinatorial verification of two designs, whereas property checking is a sequential verification of one
design (e.g. it can consider the effects of an X stored in a register).
Equivalence checkers compare two designs, and can be set up to treat X’s differently in each design. There are two
sensible configurations, which gives rise to the Consistency and Equality terminology (see section 2.4). This
terminology is similar to that used by the Synopsys Formality equivalence-checker (e.g. see “Design Consistency” in
the Formality User Guide [Synopsys 02]), but is applicable to other equivalence checkers.
2.1 Synthesis Semantics: Don’t-Care
The simplest semantics for X is treating it as a don’t-care assignment, allowing synthesis to choose a 0 or 1 to
improve the logic minimization. Note that a single X-assignment (e.g. default of a case) can in fact represent
multiple don’t-cares, each of which can be assigned to different values.
Synthesis tools tend to have two separate phases:
1. Minimization: producing minimal Boolean expressions for logic functions (using any don’t-cares)

剩余33页未读，继续阅读

身份认证 购VIP最低享 7 折!
30元优惠券
资源推荐
资源评论
墨鱼yy
  • 粉丝: 85
上传资源 快速赚钱
voice
center-task 前往需求广场，查看用户热搜

最新资源