问题标签 [formal-verification]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
induction - 验证移动数组区域的 Dafny 方法
我正在使用 Dafny 制作一个删除方法，您会收到：
字符数组
line数组的长度
l一个位置
at要删除的字符数
p
首先从 at to 删除 line 的字符at + p，然后必须移动at + pto右边的所有字符at。
例如，如果您有[e][s][p][e][r][m][a], and at = 3, and p = 3, 那么最终结果应该是[e][s][p][a]
我试图证明一个有意义的后置条件，例如：
ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);
确保 at + p 右侧的所有字符都在新位置。
但是 Dafny 输出两个错误：
索引超出范围 7 53
后置条件可能不会在此返回路径上成立。19 2
formal-verification - 如何提示 Dafny 对序列进行归纳？
我想知道我需要在以下内容中添加什么以使其通过 dafny？
formal-verification - 在 Dafny 中寻找搜索和替换的终止措施？
我正在编写一个使用查找、删除和插入方法的搜索和替换方法。我在 while 循环中调用这三个方法，但我不确定应该使用哪些前置条件。
完整代码：
vhdl - 有没有办法忽略 HDL 代码中的组合循环错误？
我正在尝试在一个非常大的项目代码中正式验证一个小模块。我已经分析并详细说明了设计。我无法验证小模块，因为该工具给了我一个“找到组合循环”错误。
我很确定这个小模块不受此循环错误的影响。所以我想避免出现这个错误。甚至可能吗？
谢谢！
system-verilog - 如何在系统 verilog 断言中编写属性？
我想在 SVA 中编写一个属性来正式验证一个行为。
这是我想要的：
如何重写上述属性，以便在 sig1 下降后，它在剩余的评估周期内保持低电平？
注意：我不想将 sig1 设为禁用 iff (sig1)
verification - 评估正式工具
为了比较 3 种形式验证工具，应该考虑哪些因素？例如：Jaspergold、Onespin、Incisive。
根据我的小研究，Jaspergold 名列前茅。但我想自己做一个项目。
我记下了一些要点，例如 1.支持的语言（vhdl、sv、verilog、sva、psl 等） 2.GUI 3.能力（他们可以处理多少大型设计） 4.评估周期数 5.性能（他们找到证据或反例的速度有多快）
我可以通过哪些其他功能扩展此列表？
谢谢！
z3 - 等效于 z3 中记录的“存储”运算符
我想知道 z3 中是否有类似于数组的“存储”运算符的记录运算符。也就是说，给定一条记录，有没有办法返回一条新记录，其中我们更改了一个元素而所有其他元素都保留了它们的值？例如：
上面的最后一行是我想做的一个例子。有没有办法做到这一点？还是用户定义的构造函数是构造新记录的唯一方法？谢谢你。
functional-programming - VHDL 函数调用：外部参考仍未解决
在架构中的功能为：
我想验证这个函数的行为是否符合预期。所以我在我的 SVA 文件中写了一个类似（不精确）的函数。
但我得到一个错误：“外部参考函数仍未解决”
如何在我的断言文件中添加外部引用？
system-verilog - 如何写属性进行形式验证？
我想iff sig1=1'b1在第一个时钟周期后禁用该属性。
从高到低的转变sig1是我的触发条件。如果我这样做disable iff(sig1)触发条件将不会被满足。
throughout在正式验证器中的启用和满足序列上也无法使用。
我该怎么做？谢谢！