00148.html

这是一本关于verilog编程语言的教程,对学习verilog语言有帮助

&nbsp;</p>
<p class="Element10">
Here is an example of an illegal property declaration that violates Restriction 3: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00699');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00699"><pre class="Element12">property illegal_recursion_4(p);
    p and (1’b1 |-&gt; illegal_recursion_4(p));
endproperty</pre></div></div>
<p class="Element10">
If this form were legal, the recursion would be stuck in time, checking p over and over again at the same cycle.&nbsp;</p>
<p class="Element10">
&nbsp;</p>
<p class="Element10">
Recursive properties can represent complicated requirements, such as those associated with varying numbers of data beats, out-of-order completions, retries, etc. Here is an example of using a recursive property to check complicated conditions of this kind.&nbsp;</p>
<p class="Element10">
&nbsp;</p>
<p class="Element10">
EXAMPLE: Suppose that write data must be checked according to the following conditions:
<ul class="Element632">
<li class="Element602">Acknowledgment of a write request is indicated by the signal write_request together with write_request_ack. When a write request is acknowledged, it gets a 4-bit tag, indicated by signal write_reqest_ack_tag. The tag is used to distinguish data beats for multiple write transactions in flight at the same time.</li>
<li class="Element602">It is understood that distinct write transactions in flight at the same time must be given distinct tags. For simplicity, this condition is not a part of what is checked in this example.</li>
<li class="Element602">Each write transaction can have between 1 and 16 data beats, and each data beat is 8 bits. There is a model of the expected write data that is available at acknowledgment of a write request. The model is a 128-bit vector. The most significant group of 8 bits represents the expected data for the first beat, the next group of 8 bits represents the expected data for the second beat (if there is a second beat), and so forth.</li>
<li class="Element602">Data transfer for a write transaction occurs after acknowledgment of the write request and, barring retry, ends with the last data beat. The data beats for a single write transaction occur in order.</li>
<li class="Element602">A data beat is indicated by the data_valid signal together with the signal data_valid_tag to determine the relevant write transaction. The signal data is valid with data_valid and carries the data for that beat. The data for each beat must be correct according to the model of the expected write data.</li>
<li class="Element602">The last data beat is indicated by signal last_data_valid together with data_valid and data_valid_tag. For simplicity, this example does not represent the number of data beats and does not check that last_data_valid is signaled at the correct beat.</li>
<li class="Element602">At any time after acknowledgement of the write request, but not later than the cycle after the last data beat, a write transaction can be forced to retry. Retry is indicated by the signal retry together with signal retry_tag to identify the relevant write transaction. If a write transaction is forced to retry, then its current data transfer is aborted and the entire data transfer must be repeated. The transaction does not rerequest and its tag does not change.</li>
<li class="Element602">There is no limit on the number of times a write transaction can be forced to retry.</li>
<li class="Element602">A write transaction completes the cycle after the last data beat provided it is not forced to retry in that cycle.</li>
</ul>Here is code to check these conditions: </p><div class="Element170">
<a href="#" onclick="CopyElementToClipboard('code00700');">Copy Code</a></div>
<div class="Element13"><div class="Element12" id="code00700"><pre class="Element12">property check_write;
    logic [0:127] expected_data; // local variable to sample model data
    logic [3:0] tag; // local variable to sample tag

    disable iff (reset)
    (
        write_request &amp;&amp; write_request_ack,
        expected_data = model_data,
        tag = write_request_ack_tag
    )
    |=&gt;
        check_write_data_beat(expected_data, tag, 4’h0);
endproperty

property check_write_data_beat
(
    expected_data, // [0:127]
    tag, // [3:0]
    i // [3:0]
);

    first_match
    (
        ##[0:$]
        (
            (data_valid &amp;&amp; (data_valid_tag == tag))
            ||
            (retry &amp;&amp; (retry_tag == tag))
        )
    )
    |-&gt;
    (
       (
           (data_valid &amp;&amp; (data_valid_tag == tag))
           |-&gt;
           (data == expected_data[i*8+:8])
       )
       and
       (
           if (retry &amp;&amp; (retry_tag == tag))
           (
               1’b1 |=&gt; check_write_data_beat(tag, expected_data, 4’h0)
           )
           else if (!last_data_valid)
           (
               1’b1 |=&gt; check_write_data_beat(tag, expected_data, i+4’h1)
           )
           else
           (
               ##1 (retry &amp;&amp; (retry_tag == tag))
               |=&gt;
               check_write_data_beat(tag, expected_data, 4’h0)
           )
       )
    );
endproperty</pre></div></div>
</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="00145.html" target="topic">17.11 声明特性</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="00145.html" target="topic">17.11 声明特性</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="&#x6211;&#x8981;&#x5566;&#x514D;&#x8D39;&#x7EDF;&#x8BA1;" 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>