📄 00159.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN">
<html>
<head>
<title>17.13.2 假设语句</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', '00159.html');" onmousedown="onBodyMouseDown();">
<!-- Begin Popups -->
<div class="Element801" id="popup00363">
<div class="Element800">
<div class="Element14">
链接</div>
<div class="Element11">
<div class="Element10">
<a href="00157.html" target="topic">17.13 并发断言</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, 'popup00363');"><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="00158.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="00157.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="00160.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">
17.13.2 假设语句</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">
The purpose of the assume statement is to allow properties to be considered as assumptions for formal analysis as well as for dynamic simulation tools. When a property is assumed, the tools constrain the environment so that the property holds. </p>
<p class="Element10">
</p>
<p class="Element10">
For formal analysis, there is no obligation to verify that the assumed properties hold. An assumed property can be considered as a hypothesis to prove the asserted properties. </p>
<p class="Element10">
</p>
<p class="Element10">
For simulation, the environment must be constrained such that the properties that are assumed shall hold. Like an assert property, an assumed property must be checked and reported if it fails to hold. There is no requirement on the tools to report successes of the assumed properties. </p>
<p class="Element10">
</p>
<p class="Element10">
Additionally, for random simulation, biasing on the inputs provides a way to make random choices. An expression can be associated with biasing as shown below </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00745');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00745"><pre class="Element12">expression dist { dist_list } ; // from Annex A.1.9</pre></div></div>
<p class="Element10">
Distribution sets and the dist operator are explained in Section 12.4.4. </p>
<p class="Element10">
</p>
<p class="Element10">
The biasing feature is only useful when properties are considered as assumptions to drive random simulation. When a property with biasing is used in an assertion or coverage, the dist operator is equivalent to inside operator, and the weight specification is ignored. For example, </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00746');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00746"><pre class="Element12">a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;
property proto
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty</pre></div></div>
<p class="Element10">
This is equivalent to: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00747');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00747"><pre class="Element12">a1_assertion:assert property req inside {0, 1} ;
property proto_assertion
@(posedge clk) req |-> req[*1:$] ##0 ack;
endproperty</pre></div></div>
<p class="Element10">
In the above example, signal req is specified with distribution in assumption a1, and is converted to an equivalent assertion a1_assertion. </p>
<p class="Element10">
</p>
<p class="Element10">
It should be noted that the properties that are assumed must hold in the same way with or without biasing. When using an assume statement for random simulation, the biasing simply provides a means to select values of free variables, according to the specified weights, when there is a choice of selection at a particular time. </p>
<p class="Element10">
</p>
<p class="Element10">
Consider an example specifying a simple synchronous request - acknowledge protocol, where variable req can be raised at any time and must stay asserted until ack is asserted. In the next clock cycle both req and ack must be de-asserted. </p>
<p class="Element10">
</p>
<p class="Element10">
Properties governing req are: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00748');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00748"><pre class="Element12">property pr1;
@(posedge clk) !reset_n |-> !req; //when reset_n is asserted (0),keep req 0
endproperty
property pr2;
@(posedge clk) ack |=> !req; // one cycle after ack, req must be de-asserted
endproperty
property pr3;
@(posedge clk) req |-> req[*1:$] ##0 ack; // hold req asserted until
// and including ack asserted
endproperty</pre></div></div>
<p class="Element10">
Properties governing ack are: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00749');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00749"><pre class="Element12">property pa1;
@(posedge clk) !reset_n || !req |-> !ack;
endproperty
property pa2;
@(posedge clk) ack |=> !ack;
endproperty</pre></div></div>
<p class="Element10">
When verifying the behavior of a protocol controller which has to respond to requests on req, assertions assert_req1 and assert_req2 should be proven while assuming that statements a1, assume_ack1, assume_ack2 and assume_ack3 hold at all times. </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00750');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00750"><pre class="Element12">a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;
assume_ack1:assume property (pr1);
assume_ack2:assume property (pr2);
assume_ack3:assume property (pr3);
assert_req1:assert property (pa1)
else $display("\n ack asserted while req is still de-asserted");
assert_req2:assert property (pa2)
else $display("\n ack is extended over more than one cycle");</pre></div></div>
<p class="Element10">
Note that assume does not provide an action block, as the actions for an assumption serve no purpose.</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="00157.html" target="topic">17.13 并发断言</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="00157.html" target="topic">17.13 并发断言</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 + -