《基于二元csp的rtl数据通路可满足性求解方法》由会员分享，可在线阅读，更多相关《基于二元csp的rtl数据通路可满足性求解方法（4页珍藏版）》请在金锄头文库上搜索。
1、一2 9 0 一第五届中国测试学术会议论文集中国苏州2 0 0 8 年5 月 基于二元C S P 的R T L 数据通路可满足性求解方法 吴为民 北京交通大学计算机与信息技术学院，北京1 0 0 0 4 4 ，中国 摘要：基于可满足性( S A T ) 的模裂检验技术已逐渐成为主流的形式验证技术。在R T L ，S A T 问题的复杂性表现在 位( b i t ) 和字( w o r d ) 数据类型并存和多样化的约束关系。其中，对数据通路酶约束求解龙为关键。本文提出采用二元C S P 来求解R T L 数据通路的可满足性问题，井给出了算法的流程以及流程中每个步骤的实现方法。我们初步实现了算法
2、， 并对实验进行了设计。实验结果表明，即使是在没有采取很多优化策略的条件下，基于C S P 的方法仍有较好的性能。 这说明了本文方法的可行性和进一步研究的价值。 关键 司： 寄存器传输级( 1 u L ) ；数据通路( d a t a p a t h ) ；可满足性( s a t i s 6 a b i I i t y ) ；约束满足问题( c s P ) ；模型检验 R T L D a t a p a t hS a t i s f i a b i l i t yS o l v i n gB a s e do nB i n a r yC S P W uW e _ M i n S c h o o
3、 lo fC o m p u t e ra n dI n f o r m a t i o nT e c h n o l o g y , B e i j i n gJ i a o t o n gU n i v e r s i t y , B e i j i n g1 0 0 0 4 4 ，C h i n a A b s t r a c t ：M o d e lc h e c k i n gb a s e dO ns a t i s f i a b i l i t ys o l v i n gh a sb e c o m et h em a i n s t r e a mf o r m a lv
4、e r i f i c a t i o nt e c h n i q u e A tR T L t h ep r o b l e m e x h i b i t ss p e c i a lc o m p l e x i t yi nb o t hb i t w o r dc o e x i s t e n c ea n dv a r i e t yo fc o n s t r a i n tt y p e s ，w h e r ec o n s t r a i n ts o l v i n gi nd a t a p a t hi st h ek e yi s s u e T h i sp
5、a p e rp r o p o s et Os o l v eR T L d a t a p a t hs a t i s f i a b i l i t ) 7p r o b l e mb yb i n a r yC S P ( c o n s t r a i n ts a t i s f a c t i o np r o b l e m ) T h ef l o wo fs t e p sa sw e l la s i m p l e m e n l a l i o nm e t h o d sa te a c hs t e pa r eg i v e n W ed e s i g ne
6、 x p e r i m e n t sa n ds h o wt h a te v e l lw i t h o u tm a n yo p t i m i z a t i o ns t r a t e g i e se x e r t e d t h e C S P b a s e dm e t h o ds t i l lw o r k sf a i r l yw e l li np e r f o r m a n c e ，w h i c hd e m o n s t r a t e st h a tt h ep r o p o s e dm e t h o di sv a l i d
7、 i t ya n dd e s e r v e sf u r t h e r r e s e a r c he f r o r t K e yW o r d s ：R e g i s t e r - T r a n s f e rL e v e l ( R T L ) ，d a t a p a t h ，s a t i s f i a b i l i t y , C o n s t r a i n tS a t i s f a c t i o nP r o b l e m ( C S P ) ，M o d e lC h e c k i n g 1 引言 基于可满足性( S A T ) 的模型
8、检验目前已经成为形 式验证的主流技术。柑应地，对于S A T 求解方法和工 具的研究就成为近几年的研究热点。传统的S A T 问题 是指布尔S A T ，是对一个布尔表达式( 通常表示为合取 范式( C N F ) ) 求解可满足性。然而，在寄存器传输级 ( R T L ) ，S A T 问题存在特殊的复杂性，表现在： ( 1 ) 数据类型非单一。既有布尔变量，还有字变 量( 位向量1 。其中，布尔变量主要来自f - R T L 的控制 器，而宁变量来自于数据通路。 ( 2 ) 约束多样性。既有与( A N D ) 、或( O R ) 、- I E ( N O T ) 等操作符，也有i J t
9、 I ( A D D ) 、比较( C M P ) 、多路选择 ( M U X ) 等较复杂的约束。 可以将R T L 求解看作是两个域的求解问题，即位 域和字域，并将决策形成的约束在两个域之I 、口J 进行传 播f l j 2 】。两个域各有适合的求解技术。适合于位域的 求解技术是B D D 、布尔S A T 和布尔A T P G 3 4 】，而适 合于字域的求解技术，目前可候选的主要是线性规划 ( L P ) 5 I ( I 】、字级决策罔( W L D D ) 6 ，以及多值逻辑求 解器 7 】等。当然，也可以将适合某个域的方法进行某 种扩展来解决整个R T L 的可满足性问题【8 【9
10、 】。 在两个域的求解中，字域的求解趋关键，也是需 要研究特殊技术的地方。迄今所采用的方法都有其优 缺点。L P 5 】、O m e g a J 测试等方法基本上还足作为黑 箱工具来使用，还不能做针对问题的优化。多值逻辑 求解器如C A M A 难以处理人规模的问题【7 】，因而实际 上也没有真正运用到R T L 求解中。W L D D 虽然比B D D 做了改进，但对乘法器件等仍有效率问题6 1 。 本文将采用约束满足问题( c s P ) 的求解技术来解 决R T L 数据通路的可满足性问题。采用C S P 方法的优 势足：首先，C S P 与R T L 数据通路的可满足性问题有 自然的对
11、应关系。数据通路器件的约柬很易于描述成 C S P 问题。其次，迄今C S P 问题己得到相当多的研究， 有很多高效的求解策略，可以根据实际情况应用这些 策略。正如F B a c c h u s 所认为的，C S P 给S A T 问题加 入了“结构”，使得其更易于对问题建模和提高求解速 度【1 0 】。虽然基于C S P 的R T L 求解技术目前研究得还 很少，但我们相信C S P 技术凭借其优势，可以更好地 解决问题。 2 问题背景和定义 R T L 电路由控制器和数据通路两部分构成。控制 器是山与、或、非等逻辑门构成的有限状念自动机 ( F S M ) ，而数据通路则是由加法器( A
12、D D ) 、乘法f f S ：( M U L ) 等运算器件和比较器( C M P ) 、多路选择器( M U x l 等接E l 器件所构成的功能部件。在图1 的简单电路中，分界 线左侧部分是数据通路，右侧部分则是控制器。接E l 器件既包含位变量又包含字变量，如图中的h lI Y 和 C M P 。与数据通路器件连接的位变量称兰 如6 J 6 2 。 基金项目：国家自然科学基金资助项H ( 6 0 6 7 3 0 3 4 ) ，北京交通大学科技基金项H ( 2 0 0 7 X M 0 1 1 ，2 0 0 8 R C 0 0 2 ) 作者简介：吴为民( 1 9 6 6 - ) ，男，博士
13、，副教授，E - m a i l ：w m w u b j t u e d u c n 第五届中国测试学术会议论文集中国苏州2 0 0 8 年5 月 一2 9 1 一 圈1 盯L 电路示意圈 数据通路的可满足性定义为：在R T L 电路中的布 尔变量以及某些要求的字变晕都得到赋值的条件下， 寻找其它字变晕的赋值，使得电路无矛盾。在图1 中， 若设b l = O ，b 2 = l ，则左侧的数据通路的可满足性问题 就是寻找w l ，w 2 ，w 3 ，w 4 的值，使得电路无矛盾。 C S P 问题定义为【1 1 】：给定一组变量X = x l ， 妇x m ，每个变量x f 都有一个相应的取值
14、范闱D f ， 以及一组用来限制变量取值的约束条件C = c 1 c 2 c n ，寻找对每个变晕的一个合法赋值，使得 所有约束都被满足。上面数据通路的C S P 问题就是： X = b l ，b 2 ，w l ，w 2 ，w 3 ，w 4 ，C = w 霉= ? - w 2 + b l w 彩，b 2 = 一J = = w 矽) 。 二元C S P ：若对于C 中的任何约束c f ，仅涉及一、 两个变量，则该C S P 就是二元C S P 。置b l = 0 ，b 2 = 1 ，则 上面的C S P 问题就成为二元C S P 问题：X = w l ，w 2 ， w 4 ，C = w 4 =
15、= w 2 ，w l = = w 4 。 3 求解方法 3 1 求解流程 1 提取出R T L 的数据通路部分。为便于构造二 元C S P 问题，还要对运算器件的某个变量赋值，对于 接口器件，还要对接口位变量赋值。这部分在后面的 实验设计中详述。 2 根据提取出的数据通路，构建二元C S P 问题。 3 搜索求解，给出满足约束的字变量的赋值，或 者给出无解的判断。 3 2 构建二元C S P 问题 二元C S P 问题町用一个四维约束矩阵 C O N S T R ( i 】0 1 l p 】( q 1 莱表示，其寺0 = i 。j M 0 = P q K ，M 是电路中字变量的个数，K = 2
16、 彬，W 是电路 中字的最大宽度。假设字变量序列为 哪聊，则 C O N S T R i 删脚= l 当且仅当V M i 取P 值、V M j 取P 值时，满足电路的所有约束要求。构建二元C S P 问题就是根据提取出的数据通路及其某些初始赋值， 再加上各个数据通路器件本身所蕴涵的约束，向约束 矩阵C O N S T R A 添加0 或1 ，使之准确地表达电路的约 束要求。 各个数据通路器件的约束方式不同，向C 嬲乃醒 添加数据的方式也不同。图2 给出了针对M U X 的添 加过程( 采用了C 语言的语法) 。 严根据M U X ( c ，H ，1 2 ，0 ) 添加C O N S T R 。器件的功能是：若c = 0 ，则O = H ，否则O = 2 。 A d d C o N S T R ( M U X ( c ，仃，1 2 ，D ) ，C C )
