将我的 pyverilog AST 转换为 Z3 求解器的输入答案

【问题标题】：Convert my pyverilog AST to input for Z3 solver将我的 pyverilog AST 转换为 Z3 求解器的输入
【发布时间】：2017-07-01 15:17:39
【问题描述】：

我已将我的 verilog 文件转换为 AST（abstrct 语法树），但还有外部约束，例如电路的输出，AST 将提供给 Z3/SMT 求解器，它应该为我们提供电路的输入，但是我不知道如何将 AST 作为 Z3/SMT 求解器的输入。

提前致谢。

【问题讨论】：

这似乎与您之前的问题非常相似：stackoverflow.com/questions/44582189/… Christoph 关于遵循 SMTLib 教程的建议是否没有产生任何见解？
我仍然对将我的文件链接到 Z3 求解器感到困惑。

标签： python verilog smt z3py

【解决方案1】：

这样的任务通常相当于遍历您的 AST 并象征性地执行它，并为 SMT 求解器生成跟踪。 说起来容易做起来难，不幸的是： 进行这种转换有很多方面，即使完全完成，求解器也很难验证相应的属性。对于完整的 Verilog，您必须基本上实现一个可以处理符号值的 Verilog 模拟器。虽然这可能是一项非常大的任务，但如果您的输入足够“简单”，也许您可以使用更少的功能集。如果不了解 Verilog 的结构，真的很难说什么。

paper 由 Z3 的两位主要作者（Nikolaj 和 Leonardo）撰写，对这种方法进行了很好的调查。这是一本很好的读物，有许多有用的参考资料。从它开始至少可以让您了解所涉及的内容。

我应该补充一点，Verilog 设计的验证是一个具有工业应用的主题，并且有供应商支持的工具（不便宜！）可以在 Verilog 级别进行验证。 Cadence 的Jasper Gold 工具就是这样一个例子。 Synopsys 也有类似的工具。

您似乎对测试用例生成感兴趣。这将对应于编写一个典型的“封面”属性，并将值读取到导致这种设置中的封面场景的主要输入。此类属性通常以 SVA 格式编写，此类工具可以理解这种格式。

【讨论】：