📄 00886.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN">
<html>
<head>
<title>附录H 并发断言的形式语义</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', '00886.html');" onmousedown="onBodyMouseDown();">
<!-- Begin Popups -->
<div class="Element801" id="popup00838">
<div class="Element800">
<div class="Element14">
链接</div>
<div class="Element11">
<div class="Element10">
<a href="01046.html" target="topic">主题</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, 'popup00838');"><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="00810.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><img src="btn_up_d.gif" border="0" alt="Up" title="Up"><a href="00811.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 并发断言的形式语义</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="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">
<div class="Element212">
<div class="TableDiv">
<table cellspacing="0" class="Table0">
<tr>
<td class="Element200" valign="top" width="50%">
<div class="Element201">
主题 </div></td><td class="Element204" valign="top" width="50%">
<div class="Element205">
描述 </div></td></tr><tr>
<td class="Element202" valign="top" width="50%">
<div class="Element203">
<a href="00811.html" target="topic">H.1 简介</a> </div></td><td class="Element206" valign="top" width="50%">
<div class="Element207">
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,... <a href="00811.html" target="topic">more</a> </div></td></tr><tr>
<td class="Element202" valign="top" width="50%">
<div class="Element203">
<a href="00812.html" target="topic">H.2 抽象语法</a> </div></td><td class="Element206" valign="top" width="50%">
<div class="Element207">
</div></td></tr><tr>
<td class="Element202" valign="top" width="50%">
<div class="Element203">
<a href="00821.html" target="topic">H.3 语义</a> </div></td><td class="Element206" valign="top" width="50%">
<div class="Element207">
Let P be the set of atomic propositions.<br>The semantics of assertions and properties is defined via a relation of satisfaction by empty, finite, and infinite<br>words over the alphabet Σ = 2P U {T, ⊥}. Such a word is an empty, finite, or infinite sequence of elements of Σ.<br>The number of elements in the sequence is called the length of the word, and the length of word w is denoted<br>|w|. Note that |w| is either a non-negative integer or infinity.<br>The sequence elements of a word are called its letters and are assumed to be indexed consecutively... <a href="00821.html" target="topic">more</a> </div></td></tr><tr>
<td class="Element202" valign="top" width="50%">
<div class="Element203">
<a href="00832.html" target="topic">H.4 Extended Expressions</a> </div></td><td class="Element206" valign="top" width="50%">
<div class="Element207">
This section describes the semantics of several constructs that are used like expressions, but whose meaning at a point in a word can depend both on the letter at that point and on previous letters in the word. By abuse of notation, the meanings of these extended expressions are defined for letters denoted “w j” even” though they depend also on letters w i for i < j. The reason for this abuse is to make clear the way these definitions should be used in combination with those in preceding sections. </div></td></tr><tr>
<td class="Element202" valign="top" width="50%">
<div class="Element203">
<a href="00835.html" target="topic">H.5 Recursive Properties</a> </div></td><td class="Element206" valign="top" width="50%">
<div class="Element207">
This section defines the neutral semantics of instances of recursive properties in terms of the neutral semantics of instances of non-recursive properties. The latter can be expanded to properties in the abstract syntax by appropriate substitutions, and so their semantics is assumed to be understood.<br><br>According to Restriction 1 in Section 17.11.3, it is understood below that the negation operator not cannot be applied to any property expression that instantiates a recursive property. Restriction 2 in Section 17.11.3 is not represented here because disable iff is treated as a general property-building operator in this appendix. A precise version of Restriction... <a href="00835.html" target="topic">more</a> </div></td></tr></table></div></div>
</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="01046.html" target="topic">主题</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 + -