首页 | 本学科首页   官方微博 | 高级检索  
     

采用二元CSP引擎求解RTL数据通路的可满足性
引用本文:吴为民.采用二元CSP引擎求解RTL数据通路的可满足性[J].计算机辅助设计与图形学学报,2009,21(4).
作者姓名:吴为民
作者单位:北京交通大学计算机与信息技术学院,北京,100044
基金项目:国家自然科学基金,北京交通大学科技基金 
摘    要:针对寄存器传输级(RTL)验证和测试过程中非常重要的数据通路可满足性求解问题,提出一种基于二元约束满足问题(CSP)的求解方法,包括数据通路提取、二元CSP建模和搜索求解3个步骤.数据通路提取通过对接口布尔变量和某些字变量赋值,为各个数据通路器件建立环境;二元CSP建模则根据该环境和各个数据通路器件的功能,将数据通路的可满足性问题转化为二元CSP描述;该二元CSP问题的描述被送入到二元CSP引擎,并采用冲突引导的回跳搜索策略进行求解,获得有解的例证或无解的判定.实验结果表明,即使在没有采取很多优化策略的条件下,该方法仍有较好的性能,并优于基于线性规划(LP)的求解方法.

关 键 词:寄存器传输级  数据通路  可满足性  约束满足问题  模型检验

RTL Datapath Satisfiability Solving Using a Binary CSP Engine
Wu Weimin.RTL Datapath Satisfiability Solving Using a Binary CSP Engine[J].Journal of Computer-Aided Design & Computer Graphics,2009,21(4).
Authors:Wu Weimin
Affiliation:School of Computer and Information Technology;Beijing Jiaotong University;Beijing 100044
Abstract:We propose a binary constraint satisfaction problem (CSP) based approach to the satisfiability problem of register-transfer level (RTL) datapaths,which is a critical issue in RTL verification and testing. The approach consists of three steps:datapath extraction,binary CSP modeling,and solution searching. In datapath extraction,we build the environments for all datapath units by making assignments to the Boolean interface variables and some word variables. Binary CSP modeling then translates the RTL datapath...
Keywords:register-transfer level  datapath  satisfiability  constraint satisfaction problem  model checking  
本文献已被 CNKI 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号