问题标签 [model-checking]

如何手动或使用（开源）工具自动将 PSL 或 SVA 活性断言翻译成 verilog？我可以做简单的安全属性，但我对活性属性一无所知。我知道一些商业工具有这个功能来检查 Verilog 设计，但我无权访问它们。

例如，我想将 PSL 中的活性断言翻译assert always req -> eventually! ack;成等效的 Verilog 电路，以便我可以使用一些工具来模型检查该属性是否存在。

• 进行了编辑，将“是否可以翻译...”改写为“我如何翻译”，谢谢 ira！

到目前为止，我知道 UPPAAL 中的选择是如何工作的。您可以使用例如 i : int[2,42] 之类的语句选择 2 到 42 之间的所有数字。

现在我有一个由 n 个自动机组成的网络（每个都有一个不同的 id）和一个二维的、预先初始化的整数数组 n * k，所以每个自动机都有一个 k 长的整数行。如何从这个数组中进行选择？就像是：

我：我的数组[id]

那么每个自动机都从它的 k 个预定义数字中进行选择？

最好的，帕维尔

我正在努力想出一个更好的解决方案来声明 CBMC（C 有界模型检查器）中的“恰好一次”属性。我的意思是一行中的一个元素位置应该具有值 1（或任何可以检查为布尔值 true 的正数），其余的必须全为零。

对于 M = 4

对于比这更大的 M，这是一个巨大的问题。可以说 M = 8 我必须做类似的事情：

检查一次的违规很容易，但说明它看起来很重要。我可能还有一个选择：将二维数组问题表述为一维位向量问题，然后进行一些智能异或。但我目前不确定。

有人对这个问题有更好的解决方案吗？

我正在使用 SPIN 模型检查器 GUI - iSPIN。GUI 带有一个不错的自动机视图生成器，但是为了看到完整的自动机，我需要放大/缩小。如果可能的话，我还想将该自动机保存在一个漂亮的图像中（避免使用打印屏幕）。有没有办法从 SPIN 或其他可以基于 Promela 模型生成自动机的工具中保存生成的自动机图像？

PS 下面是一张图片，显示了我想保存的生成的 Automaton 图像。显然，我无法仅通过打印屏幕重新创建它。

我想知道如何编写代表 proctype 的所有实例的 never 声明。例如，如果我有以下命题：

现在，如果我实例化 5 个实例，camera_node我如何创建一个原子命题检查start_publishing所有这 5 个实例是否等于零？

我正在寻找一种适当的形式主义（即时间逻辑）来模拟以下情况

1. 可能会有事件发生在离散的事件中（取决于下面详述的条件）。
2. 有状态。这种状态不能用固定数量的变量来表达。但是，可以用线性列表/数组来表示它，其中每个条目由有限数量的变量组成。
3. 在任何事件发生之前，状态是固定的。
4. 在任何时间点，事件都是可能的。它们具有固定的结构（带有一些变量）。可能的事件受当前状态的约束。
5. 事件将导致状态立即改变。
6. 事件也可能导致持续的状态变化。例如，一个变量（上述数组的条目之一）在一段时间内（立即或在指定延迟后）将其值从 0 更改为 1。
7. 还应该可以以“事件E之后某个条件C成立的最早时间点”的形式指定离散的时间点，并在该点开始连续的状态改变。

是否有现有的时间逻辑来模拟这样的事情？

还应该可以表达所需的条件，如下所示：

1. 参考某个时间点：数组所有条目的某个特定变量的总和不能超过某个阈值。
2. 提到随时间的变化：对于所有可能的时间间隔，某个变量的值（同样，来自所述数组的每个条目）[实际上，而不是为每个条目计算的某个算术表达式]的变化不得快于给定阈值。

应该有一个模型检查器，可以检查所有可能的场景是否满足所有条件。如果不是这种情况，它应该打印一个可能的场景并告诉我哪个条件不满足。换句话说，它应该区分描述可能场景的条件和在这些场景中必须满足的条件，而不仅仅是告诉我“不可能”。

我正在尝试在 NuSMV 中创建一个交通灯系统实现。现在我有 6 个布尔值用于 NS/EW 红色、黄色、绿色。但是，当我指定它们在未来状态下始终为真时，它会返回为假。如果有人在我的代码中看到任何错误，我将不胜感激。谢谢。

当我使用 NuSMV 工具验证我的 CTL 是否正确时，我遇到了一个让我很困惑的问题。

我的模型是

这是NuSMV代码：

我的 CTL 公式如下：

1. "AG( A1 -> AX ( A [ B1 U ( D1 -> EX ( F1) ) ] ) )"
2. "AG( A1 -> AX ( A [ B1 U ( F1 -> EX ( C1) ) ] ) )"
3. "AG( A1 -> AX ( A [ M1 U ( F1 -> EX ( C1) ) ] ) )"

NuSMV 验证了上述三个公式，所有这些都证明是正确的。

所以我的问题是，为什么公式 2 和公式 3 是正确的？

我想在 windows7-64 上使用 SPIN 模型检查器，并且我已经安装了它的所有先决条件。以下是我如何做到的程序

1. 我用 cygwin 安装了 gcc 编译器 .. 用命令提示符检查了更新的路径，它显示版本 4.9.2
2. 安装 Active Tcl .. 更新路径 .. 当我打开 ispin 时工作正常。
3. 更新了 ispin 目录的路径。
4. 只是一点技巧，还可以通过在 ispin 文件中给出 gcc.exe 的确切路径来检查。但是错误仍然相同。

但是当我尝试编译预先包含的示例文件（例如leader.pml）时，它给了我错误

有人可以告诉我我做错了什么和/或错过了什么吗？我该如何解决这个问题？

谢谢。

我在 ubuntu 机器上安装了 NuSMV 2.5.4。当我使用命令 NuSMV -int first.smv 在交互模式下运行它时，我得到以下响应无法打开输入文件 first.smv。这是为什么？我已将我的 smv 文件（first.smv）放在 bin 文件夹中。