📄 00162.html
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN">
<html>
<head>
<title>17.13.5 在过程化代码中嵌入并发断言</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', '00162.html');" onmousedown="onBodyMouseDown();">
<!-- Begin Popups -->
<div class="Element801" id="popup00366">
<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, 'popup00366');"><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="00161.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="00163.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.5 在过程化代码中嵌入并发断言</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">
A concurrent assertion statement can also be embedded in a procedural block. For example: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00756');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00756"><pre class="Element12">property rule;
a ##1 b ##1 c;
endproperty
always @(posedge clk) begin
<statements>
assert property (rule);
end</pre></div></div>
<p class="Element10">
If the statement appears in an always block, the property is always monitored. If the statement appears in an initial block, then the monitoring is performed only on the first clock tick. </p>
<p class="Element10">
</p>
<p class="Element10">
Two inferences are made from the procedural context: clock from the event control of an always block, and the enabling conditions. </p>
<p class="Element10">
</p>
<p class="Element10">
A clock is inferred if the statement is placed in an always or initial block with an event control abiding by the following rules:
<ul class="Element632">
<li class="Element602">The clock to be inferred must be placed as the first term of the event control as an edge specifier (posedge expression or negedge expression).</li>
<li class="Element602">The variables in expression must not be used anywhere in the always or initial block.</li>
</ul>For example: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00757');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00757"><pre class="Element12">property r1;
q != d;
endproperty
always @(posedge mclk) begin
q <= d1;
r1_p: assert property (r1);
end</pre></div></div>
<p class="Element10">
The above property can be checked by writing statement r1_p outside the always block, and declaring the property with the clock as: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00758');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00758"><pre class="Element12">property r1;
@(posedge mclk)q != d;
endproperty
always @(posedge mclk) begin
q <= d1;
end
r1p: assert property (r1);</pre></div></div>
<p class="Element10">
If the clock is explicitly specified with a property, then it must be identical to the inferred clock, as shown below: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00759');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00759"><pre class="Element12">property r2;
@(posedge mclk)(q != d);
endproperty
always @(posedge mclk) begin
q <= d1;
r2_p: assert property (r2);
end</pre></div></div>
<p class="Element10">
In the above example, (posedge mclk) is the clock for property r2. </p>
<p class="Element10">
</p>
<p class="Element10">
Another inference made from the context is the enabling condition for a property. Such derivation takes place when a property is placed in an if...else block or a case block. The enabling condition assumed from the context is used as the antecedent of the property. </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00760');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00760"><pre class="Element12">property r3;
@(posedge mclk)(q != d);
endproperty
always @(posedge mclk) begin
if (a) begin
q <= d1;
r3_p: assert property (r3);
end
end</pre></div></div>
<p class="Element10">
The above example is equivalent to: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00761');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00761"><pre class="Element12">property r3;
@(posedge mclk)a |-> (q != d);
endproperty
r3_p: assert property (r3);
always @(posedge mclk) begin
if (a) begin
q <= d1;
end
end</pre></div></div>
<p class="Element10">
Similarly, the enabling condition is also inferred from case statements. </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00762');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00762"><pre class="Element12">property r4;
@(posedge mclk)(q != d);
endproperty
always @(posedge mclk) begin
case (a)
1: begin q <= d1;
r4p: assert property (r4);
end
default: q1 <= d1;
endcase
end</pre></div></div>
<p class="Element10">
The above example is equivalent to: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00763');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00763"><pre class="Element12">property r4;
@(posedge mclk)(a==1) |-> (q != d);
endproperty
r4_p: assert property (r4);
always @(posedge mclk) begin
case (a)
1: begin q <= d1;
end
default: q1 <= d1;
endcase
end</pre></div></div>
<p class="Element10">
The enabling condition is inferred from procedural code inside an always or initial block, with the following restrictions:
<ol class="Element632">
<li value="1" class="Element602">There must not be a preceding statement with a timing control.</li>
<li value="2" class="Element602">A preceding statement shall not invoke a task call which contains a timing control on any statement.</li>
<li value="3" class="Element602">The concurrent assertion statement shall not be placed in a looping statement, immediately, or in any nested scope of the looping statement.</li>
</ol></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 + -