📄 00811.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN">
<html>
<head>
<title>H.1 简介</title>
<meta http-equiv="Content-Type" content="text/html; charset=GB2312" />
<meta name="generator" content="Doc-O-Matic" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<link rel="STYLESHEET" href="default.css" type="text/css" />
<script type="text/javascript" src="scripts.js"></script>
</head>
<body class="Element700" onload="onBodyLoadEx('systemverilog31a.html', 'topic', '00811.html');" onmousedown="onBodyMouseDown();">
<!-- Begin Popups -->
<div class="Element801" id="popup00839">
<div class="Element800">
<div class="Element14">
链接</div>
<div class="Element11">
<div class="Element10">
<a href="00886.html" target="topic">附录H 并发断言的形式语义</a></div>
</div>
</div>
</div>
<!-- End Popups -->
<!-- Begin Page Header -->
<div class="Element710" id="areafixed">
<div class="Element92">
<table width="100%" cellspacing="0" cellpadding="0">
<tr><td width="33%">
<div class="Element1">
<a href="#" onmousedown="showPopup(this, 'popup00839');"><img src="seealsolink.png" border="0" alt="" title=""></a> SystemVerilog 3.1a语言参考手册</div>
</td><td width="34%">
<div class="Element2">
</div>
</td><td width="33%">
<div class="Element90">
<a href="00886.html" target="topic"><img src="btn_prev_lightblue.gif" border="0" alt="Previous" title="Previous" onmouseover="switchImage(this, 'btn_prev_lightblue_hover.gif');" onmouseout="switchImage(this, 'btn_prev_lightblue.gif');"></a><a href="00886.html" target="topic"><img src="btn_up_lightblue.gif" border="0" alt="Up" title="Up" onmouseover="switchImage(this, 'btn_up_lightblue_hover.gif');" onmouseout="switchImage(this, 'btn_up_lightblue.gif');"></a><a href="00812.html" target="topic"><img src="btn_next_lightblue.gif" border="0" alt="Next" title="Next" onmouseover="switchImage(this, 'btn_next_lightblue_hover.gif');" onmouseout="switchImage(this, 'btn_next_lightblue.gif');"></a></div>
</td></tr></table><div class="Element5">
H.1 简介</div>
</div>
</div>
<!-- End Page Header -->
<!-- Begin Client Area -->
<div class="Element720" id="areascroll">
<div class="Element721">
<!-- Begin Page Content -->
<div class="Element58">
<a name="描述"></a><div class="Element11">
<div class="Element10">
<p class="Element10">
This appendix presents a formal semantics for SystemVerilog concurrent assertions. Immediate assertions and coverage statements are not discussed here. Throughout this appendix, “assertion” is used to mean “concurrent assertion”. The semantics is defined by a relation that determines when a finite or infinite word (i.e., trace) satisfies an assertion. Intuitively, such a word represents a sequence of valuations of SystemVerilog variables sampled at the finest relevant granularity of time (e.g., at the granularity of simulator cycles). The process by which such words are produced is closely related to the SystemVerilog scheduling semantics and is not defined here. In this appendix, words are assumed to be sequences of elements, each element being either a set of atomic propositions or one of two special symbols used as placeholders when extending finite words. The atomic propositions are not further defined. The meaning of satisfaction of a SystemVerilog boolean expression by a set of atomic propositions is assumed to be understood. </p>
<p class="Element10">
</p>
<p class="Element10">
The semantics is based on an abstract syntax for SystemVerilog assertions. There are several advantages to using the abstract syntax rather than the full SystemVerilog Assertions BNF.
<ol class="Element630">
<li value="1" class="Element600">The abstract syntax facilitates separation of derived operators from basic operators. The satisfaction relation is defined explicitly only for assertions built from basic operators.</li>
<li value="2" class="Element600">The abstract syntax avoids reliance on operator precedence, associativity, and auxiliary rules for resolving syntactic and semantic ambiguities.</li>
<li value="3" class="Element600">The abstract syntax simplifies the assertion language by eliminating some features that tend to encumber the definition of the formal semantics.
<ul class="Element630">
<li class="Element600">The abstract syntax eliminates local variable declarations. The semantics of local variables is written with implicit types.</li>
<li class="Element600">The abstract syntax eliminates instantiation of sequences and properties. The semantics of an assertion with an instance of a sequence or non-recursive property is the same as the semantics of a related assertion obtained by replacing the sequence or non-recursive property instance with an explicitly written sequence or property. The explicit sequence or property is obtained from the body of the associated declaration by substituting actual arguments for formal arguments. A separate section defines the semantics of instances of recursive properties in terms of the semantics of instances of nonrecursive properties.</li>
<li class="Element600">The abstract syntax does not allow implicit clocks. Clocking event controls must be applied explicitly in the abstract syntax.</li>
<li class="Element600">The abstract syntax does not allow explicit procedural enabling conditions for assertions. Procedural enabling conditions are utilized in the semantics definition (see Subsection 3.3.1), but the method for extracting such conditions is not defined in this appendix.</li>
</ul></li>
<li value="4" class="Element600">The abstract syntax eliminates the distinction between property_expr and property_spec from the full BNF. Without the distinction, disable iff is a general, nestable property-building operator, while in the full BNF disable iff can be attached only at the top level of a property. Semantically, there is no need for this restriction on the placement of disable iff. The abstract syntax thus eliminates an unnecessary semantic layer while maintaining the simple inductive form for the definition of the semantics of properties. As a result, semantics are given for some properties that do not correspond to forms from the full BNF, but this does not degrade the definitions for the properties that do correspond to forms from the full BNF.</li>
</ol> </p>
<p class="Element10">
In order to use this appendix to determine the semantics of a SystemVerilog assertion, the assertion must first be transformed into an enabling condition together with an assertion in the abstract syntax. For assertions that do not involve recursive properties, this transformation involves eliminating sequence and non-recursive property instances by substitution, eliminating local variable declarations, introducing parentheses, determining the enabling condition, determining implicit or inferred clocking event controls, and eliminating redundant clocking event controls. For example, the following SystemVerilog assertion </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code01112');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code01112"><pre class="Element12">sequence s(x,y); x ##1 y; endsequence
sequence t(z); @(c) z[*1:2] ##1 B; endsequence
always @(c) if (b) assert property (s(A,B) |=> t(A));</pre></div></div>
<p class="Element10">
is transformed into the enabling condition “b” together with the assertion </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code01113');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code01113"><pre class="Element12">always @(c) assert property ((A ##1 B) |=> (A[*1:2] ##1 B))</pre></div></div>
<p class="Element10">
in the abstract syntax. </p>
<p class="Element10">
</p>
<p class="Element10">
If the SystemVerilog assertion involves instances of recursive properties, then the transformation replaces these instances with placeholder functions of the actual arguments. The semantics of an instance of a recursive property is defined in terms of associated non-recursive properties in Section H.5. Once the semantics of the recursive property instances are understood, the placeholder functions are treated as properties with these semantics. Then the ordinary definitions can be applied to the transformed assertion in the abstract syntax together with placeholder functions.</p></div>
</div>
<a name="Group"></a><div class="Element14">
<a onclick="toggleVisibilityStored('Group');" class="a_Element14"><img src="sectionminus.png" border="0" alt="" title="" id="imgGroup">Group</a></div>
<div id="divGroup">
<div class="Element11">
<div class="Element10">
<p class="Element10">
<a href="00886.html" target="topic">附录H 并发断言的形式语义</a></p></div>
</div>
</div>
<a name="Links"></a><div class="Element14">
<a onclick="toggleVisibilityStored('链接');" class="a_Element14"><img src="sectionminus.png" border="0" alt="" title="" id="img链接">链接</a></div>
<div id="div链接">
<div class="Element11">
<div class="Element10">
<a href="00886.html" target="topic">附录H 并发断言的形式语义</a></div>
</div>
</div>
</div>
<!-- End Page Content -->
<!-- Begin Page Footer -->
<hr width="98%" align="center" size="1" color="#CCCCCC" />
<table align="center" cellpadding="0" cellspacing="0" border="0">
<tbody>
<tr height="10">
<td></td>
</tr>
<tr align="center">
<td>
<script type="text/javascript"><!--
google_ad_client = "pub-5266859600380184";
google_ad_width = 468;
google_ad_height = 60;
google_ad_format = "468x60_as";
google_ad_type = "text_image";
google_ad_channel ="";
google_page_url = document.location;
//--></script>
<script type="text/javascript"
src="http://pagead2.googlesyndication.com/pagead/show_ads.js">
</script>
</td>
</tr>
<tr height="15">
<td></td>
</tr>
<tr align="center">
<td>
<font size=2>除非特别声明，原文版权归作者所有，如有转摘请注明原作者以及译者（<a href="http://www.fpgatech.net/" target="_blank">FPGA技术网</a>）信息。<br />
如果您对本主题有何建议或意见，请登陆<a href="http://www.fpgatech.net/forum/forumdisplay.php?fid=18" target="_blank">FPGA开发者家园</a>提交，您的参与是我们前进的动力。</font>
<script language="javascript" type="text/javascript" src="http://js.users.51.la/195685.js"></script>
<noscript><a href="http://www.51.la/?195685" target="_blank"><img alt="我要啦免费统计" src="http://img.users.51.la/195685.asp" style="border:none" /></a></noscript>
</td>
</tr>
</tbody>
</table>
<!-- End Page Footer -->
</div>
</div>
<!-- End Client Area -->
</body></html>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -