将pyverilog AST转换为z3s的输入

Question

我已经把我的verilog文件转换成AST（abstrct语法树），但是随着外部约束，比如电路的输出，AST将被提供给Z3/SMT解算器，它应该给我们电路的输入，但是我不知道如何将AST作为Z3/SMT解算器的输入。在

提前谢谢。在

Answer 1

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

这篇由Z3的两位主要作者（尼古拉吉和莱昂纳多）撰写的这篇文章对这种方法进行了很好的综述。这是一本很好的读物，里面有许多有用的参考资料。从这个开始至少可以让你知道其中涉及到什么。在

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

您似乎对测试用例生成感兴趣。这相当于编写一个典型的“cover”属性，并将值读入主输入，从而在这样的设置中导致cover场景。这类属性通常是以SVA格式编写的，这类工具可以理解这种格式。在