代码之家 › 专栏 › 技术社区 › Jim bim

将pyverilog AST转换为Z3解算器的输入

z3py smt verilog python

0

Jim bim · 技术社区 · 7 年前

我已经将我的verilog文件转换为AST(abstrct语法树),但同时还有外部约束,如电路的输出和AST将被提供给Z3/SMT求解器,它应该为我们提供电路的输入,但我不知道如何将AST作为Z3/SM T求解器的输入。

提前谢谢。

1 回复 | 直到 7 年前

1

0

alias 7 年前

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

paper 由Z3的两位主要作者(尼古拉和莱昂纳多)撰写的文章对这种方法进行了很好的调查。这本书很好,有很多有用的参考资料。从这一点开始,至少可以让你了解其中所涉及的内容。

我应该补充一点,Verilog设计的验证是一个具有工业应用的主题,并且有供应商支持的工具(不便宜!)在Verilog级别进行验证。这个 Jasper Gold Synopsys 还有一个类似的工具。

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