返回介绍
文江博客 开发文档 IEEE SystemVerilog 3.1a 语言参考手册 文章详情

H.3.3 Satisfaction without local variables

发布于 2020-09-09 22:56:16 字数 1441 浏览 849 评论 0 收藏 0

主题

描述

H.3.3.1 Neutral satisfaction

w denotes a non-empty finite or infinite word over Σ. Assume that all properties, sequences, and unclocked
property fragments do not involve local variables.
Neutral satisfaction of assertions:
For the definition of neutral satisfaction of assertions, b denotes the boolean expression representing the
enabling condition for the assertion. Intuitively, b is derived from the conditions in the context of a procedural
assertion, while b is “1” for a declarative assertion.
? w, b always @(c) assert property P iff for every 0 < i < |w| such that w i c and w i b,
w i.. @(c) P.
?... more

H.3.3.2 Weak and strong satisfaction by finite words

This subsection defines weak and strong satisfaction, denoted – and + (respectively) of an assertion A by
a finite (possibly empty) word w over Σ. These relations are defined in terms of the relation of neutral satisfaction
by infinite words as follows:
? w – A iff w Tω A.
? w + A iff w⊥ω A.
A tool checking for satisfaction of A by the finite word w should return:
? “holds strongly” if w + A.
? “fails” if w A.
? “holds (but does not hold strongly)” if w A and w + A.
? “pending” if... more

如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论， 你可以免费 注册 一个本站的账号。
列表为空，暂无数据
    我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站，即表示您同意使用 Cookies 和您的相关数据。
    原文