问题标签 [formal-verification]

以下代码有一个奇怪的行为

在向我展示 eq.symm 的类型时，我希望 check 不会考虑不相关的隐式变量 toto。这真的是故意的吗？

我正在正式验证大设计中的小模块。

我已经分析并详细说明了设计（使用 Jaspergold -fpv）。

我写了一个非常简单的封面属性（SVA）：

找到封面大约需要 5300 秒。我注意到“Bound”是143。

那么为什么生成封面需要这么长时间，这意味着什么（所用时间和限制）？

是否因为该工具必须深入研究设计状态才能生成封面并且 COI 很大？还是其他什么原因？

谢谢你的帮助。

给定一个系统及其完整的状态空间，我可以说该状态空间是该系统行为的正式规范吗？

我在这里更清楚地改变了我的问题。有两种不同的模型，一种是发送者模型，一种是接收者模型。我想检查发送的消息与接收者接收的消息不同的属性。

LTLSPEC (G(state=receiver -> messageTransmited != messageReceived))

我是一个基于断言的验证新手，试图了解它应该如何正确完成。我已经找到了很多关于 systemverilog + 断言的结构和技术细节的信息，但我仍然没有找到某种关于在现实世界中如何真正完成事情的“食谱”材料。

问题和限制：

• 设计有一个带有数据、有效和id输入的数据输入总线
• 一个数据“包”是3个样本
• 在通道n之后，总会有来自通道n+1的数据
  • 频道 ID 将在最大 ID 发送后回绕
• 数据字节之间可以有任意数量的 clk 滴答声

• 下面是带有通道 ID 的简单且希望正确的时序图：

  

那么如何用最少的代码做到这一点呢？干净整洁。以前我已经构建了虚拟 verilog 模块来驱动数据。但是可以肯定的是，可以只使用一些假设属性来限制通道 ID，否则可以腾出手来让正式工具尝试破坏我的设计？

初学者的简单模板可以是：

我想问题是像上面这样的假设/断言往往会在每个数据样本上触发并创建时间重叠的并行线程。

我想写一个断言，它说 req 应该在下一次完成后 4 个周期变高。对我来说，重置完成已经很高了。我怎样才能在下一次完成时提出更高的要求。assert property {$rose(done) |-> ##4 req}但我不知道为什么它不起作用。有人可以帮忙吗？

我见过的最强后置谓词转换器的每个公式都呈现如下分配规则：

我想知道，为什么上述规则中需要存在（以及存在量化的变量“v”）？在我看来，最强的后置条件谓词转换器几乎与符号评估相同，因为您维护一个状态（从变量到值的映射）和一个路径条件（一个谓词，在程序中的特定点必须为真）。然而，符号评估并不依赖于存在量词。

所以，我想我一定在这里遗漏了一些东西。任何帮助表示赞赏！

合金新手在这里。

我真的很喜欢在 Alloy 中创建约束并让分析器根据约束检查模型是否有效。

但我问自己，“这些约束定义仅仅是心理体操，还是有助于构建更好的软件？”</p>

让我们举一个具体的例子。在电子邮件客户端地址簿的模型中，可以定义此约束以将新条目添加到地址簿中：

新书 b' 中的地址映射与旧书 b 中的地址映射相同，但增加了从名称到地址的链接。该约束在合金中表示为： b'.addr = b.addr + n->a

那个好漂亮。

但是当在代码中实现添加操作时，我很难看到它的相关性。例如，我在 Common Lisp 中实现了add操作：

用文字来说：“这是一个名为add的函数的定义，它具有三个参数：b、n和a（书、姓名、地址）。使用 Common Lisp 集合函数adjoin将列表 ( na ) 添加到b。”</p>

该函数似乎正确地实现了一个简单的添加函数。我如何处理我在 Alloy 中定义的约束？我应该编写额外的代码来表达约束吗？在伪代码中：[1]

编写这样的代码似乎需要做很多工作，而且没有明显的好处。

所以我的问题是：在代码中实现合金模型时，我应该如何处理合金中定义的约束？

此外，是否有描述如何将合金模型转换为代码的教程，包括如何在代码中使用合金约束定义的描述？

谢谢你。

[1] 注意：我意识到 Common Lisp 中有一个名为 Screamer 的语言扩展，用于约束编程

我怎样才能证明这两个陈述是相等的：

1. Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d

2. Val.shru (Val.and a (Vint b)) (Vint c) <> d

这个概念非常简单，但停留在寻找解决它的正确策略上。这实际上是我要证明的引理：

谢谢，

我在证明列表中存在变量时遇到问题。我怎样才能证明这样的事情：

我有另一个问题。如何对列表中的值进行案例分析（如果它存在于列表的这一部分中）？这是我要证明的主要引理。任何帮助表示赞赏：

谢谢，