采用二元CSP引擎求解RTL数据通路的可满足性

• 作者: 吴为民
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 寄存器传输级 数据通路 可满足性 约束满足问题 模型检验
• 年，卷（期）: 2009,（4）
• 所属期刊栏目: VLSI设计与测试及电子设计自动化
• 页码范围: 442-447
• 页数: 6页
• 分类号: TP391.7
• 字数: 4799字
• 语种: 中文

摘要

针对寄存器传输级(RTL)验证和测试过程中非常重要的数据通路可满足性求解问题,提出一种基于二元约束满足问题(CSP)的求解方法,包括数据通路提取、二元CSP建模和搜索求解3个步骤.数据通路提取通过对接口布尔变量和某些字变量赋值,为各个数据通路器件建立环境;二元CSP建模则根据该环境和各个数据通路器件的功能,将数据通路的可满足性问题转化为二元CSP描述;该二元CSP问题的描述被送入到二元CSP引擎,并采用冲突引导的回跳搜索策略进行求解,获得有解的例证或无解的判定.实验结果表明,即使在没有采取很多优化策略的条件下,该方法仍有较好的性能,并优于基于线性规划(LP)的求解方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴为民	北京交通大学计算机与信息技术学院	4	54	2.0	4.0