基于二元CSP的RTL数据通路可满足性求解方法
基于可满足性(SAT)的模型检验技术已逐渐成为主流的形式验证技术.在RTL,SAT问题的复杂性表现在位(bit)和字(word)数据类型并存和多样化的约束关系。其中,对数据通路的约束求解尤为关键.本文提出采用二元CSP来求解RTL数据通路的可满足性问题,并给出了算法的流程以及流程中每个步骤的实现方法。我们初步实现了算法,并对实验进行了设计.实验结果表明,即使是在没有采取很多优化策略的条件下,基于CSP的方法仍有较好的性能.这说明了本文方法的可行性和进一步研究的价值.
寄存器传输级 数据通路 可满足性 约束满足问题 模型检验 形式验证 算法流程
吴为民
北京交通大学计算机与信息技术学院,中国 北京 100044
国内会议
苏州
中文
290-293
2008-05-21（万方平台首次上网日期，不代表论文的发表时间）