基于Surrogate模型的断言覆盖技术研究.pdf
《基于Surrogate模型的断言覆盖技术研究.pdf》由会员分享,可在线阅读,更多相关《基于Surrogate模型的断言覆盖技术研究.pdf(11页珍藏版)》请在咨信网上搜索。
1、 基于S u r r o g a t e模型的断言覆盖技术研究*史明川,龙巧洲,邹鸿基,李 暾(国防科技大学计算机学院,湖南 长沙 4 1 0 0 7 3)摘 要:随着集成电路设计规模不断增大,验证成为制约设计进程的瓶颈之一。目前,仿真仍是集成电路设计验证的主导方法之一,仿真的完备性通常通过各种覆盖率测度来度量。功能覆盖率是抽象层次较高的一种覆盖率,实际工程中,功能常以S y s t e mV e r i l o g断言形式呈现。目前常用的随机测试向量生成较难生成大量激活断言的测试向量;而采用约束求解的策略时,一旦覆盖条件中涉及到非初始输入信号(内部信号、输出信号),约束求解的效率将极为低下,
2、导致仍然难以覆盖目标断言。针对含非初始输入信号断言的覆盖问题,提出了一种利用S u r r o g a t e模型的断言覆盖率提升方法,主要是为非初始输入信号生成体现其与初始输入信号关系的、只包含初始输入信号的S u r r o g a t e模型,再以此S u r r o g a t e模型作为约束求解的对象,降低了约束求解的复杂度。实验结果表明,相比于随机测试向量生成,该方法在断言覆盖方面有较大提升。关键词:S y s t e mV e r i l o g断言;测试生成;S u r r o g a t e模型中图分类号:T P 3 9 9文献标志码:Ad o i:1 0.3 9 6 9/j
3、.i s s n.1 0 0 7-1 3 0 X.2 0 2 3.0 8.0 0 5A S u r r o g a t e m o d e l-b a s e d a s s e r t i o n c o v e r a g e i m p r o v e m e n t t e c h n o l o g y S H I M i n g-c h u a n,L ONG Q i a o-z h o u,Z OU H o n g-j i,L I T u n(C o l l e g e o f C o m p u t e r S c i e n c e a n d T e c h n o l o
4、 g y,N a t i o n a l U n i v e r s i t y o f D e f e n s e T e c h n o l o g y,C h a n g s h a 4 1 0 0 7 3,C h i n a)A b s t r a c t:A s t h e s c a l e o f i n t e g r a t e d c i r c u i t d e s i g n c o n t i n u e s t o i n c r e a s e,v e r i f i c a t i o n h a s b e c o m e o n e o f t h e b
5、 o t t l e n e c k s i n t h e d e s i g n p r o c e s s.C u r r e n t l y,s i m u l a t i o n i s s t i l l o n e o f t h e d o m i n a n t m e t h o d s f o r i n t e g r a t e d c i r c u i t d e s i g n v e r i f i c a t i o n,a n d t h e c o m p l e t e n e s s o f s i m u l a t i o n i s u s u
6、 a l l y m e a s u r e d b y v a r i o u s c o v e r a g e m e t r i c s.F u n c t i o n a l c o v e r a g e i s a h i g h e r l e v e l o f c o v e r a g e,a n d i n p r a c t i c a l e n g i n e e r i n g,f u n c-t i o n s a r e o f t e n p r e s e n t e d i n t h e f o r m o f S y s t e mV e r i
7、l o g a s s e r t i o n s.C u r r e n t l y,i t i s d i f f i c u l t t o g e n e r a t e a l a r g e n u m b e r o f t e s t v e c t o r s t h a t a c t i v a t e a s s e r t i o n s u s i n g c o mm o n l y u s e d r a n d o m t e s t v e c t o r g e n e r a t i o n m e t h o d s.Wh e n u s i n g
8、c o n s t r a i n t s o l v i n g s t r a t e g i e s,i f t h e c o v e r a g e c o n d i t i o n i n v o l v e s n o n-i n i t i a l i n p u t s i g n a l s(i n t e r n a l s i g n a l s,o u t p u t s i g n a l s),t h e e f f i c i e n c y o f c o n s t r a i n t s o l v i n g w i l l b e e x t r e
9、 m e l y l o w,m a k i n g i t s t i l l d i f f i c u l t t o c o v e r t h e t a r g e t a s s e r t i o n.T o a d d r e s s t h e c o v e r a g e p r o b l e m o f a s s e r t i o n s c o n-t a i n i n g n o n-i n i t i a l i n p u t s i g n a l s,t h i s p a p e r p r o p o s e s a S u r r o g a
10、 t e m o d e l-b a s e d a s s e r t i o n c o v e r a g e i m-p r o v e m e n t m e t h o d,w h i c h m a i n l y g e n e r a t e s a S u r r o g a t e m o d e l t h a t r e f l e c t s t h e r e l a t i o n s h i p b e t w e e n n o n-i n i t i a l i n p u t s i g n a l s a n d i n i t i a l i n p
11、 u t s i g n a l s a n d o n l y c o n t a i n s i n i t i a l i n p u t s i g n a l s,a n d t h e n u s e s t h i s S u r r o g a t e m o d e l a s t h e o b j e c t o f c o n s t r a i n t s o l v i n g,t h u s r e d u c i n g t h e c o m p l e x i t y o f c o n s t r a i n t s o l v i n g.E x p e
12、 r i m e n t a l r e s u l t s s h o w t h a t t h i s m e t h o d h a s a s i g n i f i c a n t i m p r o v e m e n t i n a s s e r t i o n c o v e r a g e c o m-p a r e d t o r a n d o m t e s t v e c t o r g e n e r a t i o n.*收稿日期:2 0 2 2-0 8-0 7;修回日期:2 0 2 2-1 0-2 0基金项目:国家自然科学基金(U 1 9 A 2 0 6 2
13、)通信作者:李暾(t u n l i n u d t.e d u.c n)通信地址:4 1 0 0 7 3 湖南省长沙市国防科技大学计算机学院A d d r e s s:C o l l e g e o f C o m p u t e r S c i e n c e a n d T e c h n o l o g y,N a t i o n a l U n i v e r s i t y o f D e f e n s e T e c h n o l o g y,C h a n g s h a 4 1 0 0 7 3,H u n a n,P.R.C h i n a C N 4 3-1 2 5 8
14、/T PI S S N 1 0 0 7-1 3 0 X 计算机工程与科学C o m p u t e r E n g i n e e r i n g&S c i e n c e第4 5卷第8期2 0 2 3年8月 V o l.4 5,N o.8,A u g.2 0 2 3 文章编号:1 0 0 7-1 3 0 X(2 0 2 3)0 8-1 3 6 5-1 1K e y w o r d s:S y s t e mV e r i l o g a s s e r t i o n;t e s t g e n e r a t i o n;S u r r o g a t e m o d e l1 引言在现
15、代电子设计自动化流程中,复杂性的增加和上市时间的缩短使得功能验证成为硬件设计流程中的主要瓶颈,仿真在功能验证中发挥了不可替代的作用,基于仿真的功能验证是一个关键而又耗时的步骤1。在此步骤中,工程师一般使用大量测试向量来仿真设计,并监控信号,以确定是否满足覆盖目标或功能要求。对于复杂的设计,每个输入通常跨越多个时钟周期。由于详尽的仿真对于实际设计是不切实际的,因此使用“高质量”的测试向量来充分覆盖系统在目标中的运行是极其重要的。随机测试向量生成、基于随机采样的约束求解测试向量生成2和定向测试向量生成3是仿真验证中测试向量生成最常用的方法。S y s t e mV e r i l o g引入断言机
16、制来描述电路设计的功能特性。本文将S y s t e mV e r i l o g中的断言作为覆盖目标,试图生成大量可以激活断言的测试向量。实际设计中,上述3种方法针对2类断言的一般处理方式如下所示:(1)断言的激活条件只包含设计的初始输入信号时,可使用基于随机采样的约束求解生成多个时钟周期的初始输入信号值,从而激活断言。(2)断言的激活条件中包含设计的内部信号或者输出信号时,工业界常用的随机测试向量生成,即使激活了断言,在一定时钟周期内对于断言激活的次数也较少(激活次数远远小于激活条件中信号取值的组合数),不能充分激活断言达到验证电路功能的目的;针对激活条件进行约束求解的随机采样同样不能充分
17、激活断言;基于模型检验、符号执行的定向测试向量生成由于受到电路规模的限制效率较低。在一个复杂系统中,S u r r o g a t e模型用于当输入与输出之间的实际关系未知或计算代价较高时,将输入数据映射到输出数据,常用于复杂系统的优化。而在电路设计中,常用断言描述信号之间的关系,这也可视为S u r r o g a t e模型。电路设计中断言(不变式)的自动提取工作为测试向量生成提供了新思路:依据自动提取的电路中的不变式,可以将目标断言中的非初始输入信号用只包含初始输入的不变式进行替换,本文将此不变式称为相应的非初始输入信号在测试向量生成时的S u r r o g a t e模型。本文利用此
18、S u r r o g a t e模型,将覆盖条件中的非初始输入信号转化为初始输入信号的逻辑运算表达式,降低了约束求解的复杂度。2 相关研究2.1 测试向量生成技术文献4 讨论了布尔/整数混合变量域测试向量生成的有效约束求解问题,提出了一种基于马尔可夫 链 蒙 特 卡 罗MCMC(M a r k o v C h a i n M o n t e C a r l o)方法的混合求解器。为了解决解空间不连续时的性能问题,Wu等人5 8提供了一种预处理技术,通过自适应地分割变量范围来分析解空间,并证明了各子空间的可行性。文献9 提出了一种基于约束求解的测试向量生成引擎T o g g e r,这项工作是
19、基于电路综合后的门级电路展开的。模型检验实现了定向测试的自动生成。针对模型检验,文献1 0 提出了几种有效的学习技术,这些技术可以改善单个属性和一组相似属性的总体测试生成时间。针对涉及非初始输入信号会使搜索状态空间爆炸的问题,文献1 1 使用一种针对寄存器传输级R T L(R e g i s t e r T r a n s f e r L e v e l)的朴素前向遍历算法,但其强行打断反馈电路使得实验结果并不好。文献1 2 提出了一种自动的、可扩展的机制,使用符号执行和R T L模型的具体仿真相结合的C o n c o l i c方式来生成定向测试,但其仍然没有解决如何大量生成覆盖目标的测试
20、向量的问题。2.2 电路不变式提取在软件验证领域,D a i k o n1 3搜索满足一组不变式模板的值。作为为硬件设计推断不变式的第一次尝试,I O D I N E(I m p l e m e n t a t i o n O f D y n a m i c I N v a r i a n t E x t r a c t i o n)1 4在待验证设计DUV(D e-s i g n U n d e r V e r i f i c a t i o n)中的一个或多个变量中假设了一组候选不变式。D i a n o s i s1 5检查预定义的不变式,只留下仿真执行路径中有效的候选不变式,该方法不断
21、重新组合这些候选不变式,直到不能创建新的不变式为止,从而得到一组电路不变式。I n f e r n o1 6通过分析仿真执行路径来推断不变6631C o m p u t e r E n g i n e e r i n g&S c i e n c e 计算机工程与科学 2 0 2 3,4 5(8)式,即在执行数据中多次出现的信号值序列,以及在某些边界值中开始/结束的序列。V a s u d e v a n等人1 7提出了G o l d M i n e,其结合了静态分析和基于决策树 的 仿 真 数 据 监 督 学 习。此 外,D a n e s e等人1 8提出了A-T E AM工具,可以从DUV
22、仿真执行路径中动态提取线性时序逻辑L T L(L i n e a r-T i m e L o g i c)断言,该工具既适用于布尔数据类型,也适用于数值数据类型。2.3 相关研究总结测试向量相关技术仍存在下述问题:基于随机采样的约束求解测试向量生成技术无法处理断言的激活条件中涉及到的非初始输入信号情况;基于模型检验或符号执行的定向测试生成技术无法在有限时间内生成大量激活断言的测试向量。本文采用G o l d M i n e中决策树的方法挖掘一系列初始输入信号和非初始输入信号之间的关系序列,进一步组合为非初始输入信号的S u r r o g a t e模型。然后基于此S u r r o g a
23、t e模型,利用随机采样技术,在有限时间内生成的测试向量即可大量激活断言。3 相关定义及方法3.1 相关定义(1)覆盖目标。本文以S y s t e mV e r i l o g中的断言为覆盖目标,使断言激活的条件称为覆盖条件。(2)断言的激活(分析覆盖条件)。S y s t e mV e r i l o g中的断言分为即时断言和并发断言。即时断言一般内嵌于模块功能实现内部,检查模块设计中的漏洞。并发断言一般编写于模块功能实现后。本文将2类断言分类处理:针对即时断言,激活断言定义为到达此断言所在分支语句,即此断言所在分支语句条件为真。针对并发断言:在本文中,断言的激活是指找到“非空洞地”否定断
24、言的反例。“空洞”在文献1 9 中的定义为:如果公式中存在子公式,可以用任意公式替换,且不影响模型检验结果,则模型M中的公式为“空洞”的。例如,在公式pq中,如果p总是假的,则该公式是“空洞”的,因为q可以被任何公式替换。激活如 下 所 示 的 并 发 断 言,即 找 到 可 以 使“a&b”为真的输入序列:p r o p e r t y p1;(p o s e d g e c l k)a&b|-c;e n d p r o p e r t ya s s e r t p r o p e r t y(p1);(3)S u r r o g a t e模型。S u r r o g a t e模型描述了
25、复杂电路系统中输入信号对非初始输入信号的影响关系,如图1所示。图1 a展示了电路中信号取值的迁移,图中每个圆点表示一组电路中信号的取值,最左侧表示的是复位状态下所有信号的取值,而虚线框出的部分表示了电路在不同输入情况下的信号取值的迁移(其中一个颜色表示一组输入);而图1 b则将中间信号取值迁移部分用黑盒表示,此黑盒即为S u r r o g a t e模型,将复杂的电路使用简单的输入信号的组合代替。简单来讲,S u r r o g a t e模型即一组输入信号的取值组合,具体内涵表述如下:使目标信号从初始取值经过特定时钟周期后,变为目标取值的输入信号取值组合。此S u r r o g a t
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 基于 Surrogate 模型 断言 覆盖 技术研究
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。