基于路径约束求解的多目标状态激励生成方法
|
摘要
该文提出了一种针对多个难达目标状态的激励生成方法,该方法基于抽象引导的半形式化方法框架.采用一个评估函数对候选状态进行评价,该评估函数综合考虑了从一个状态到不同目标状态的全局抽象距离信息,评价出从各个状态到达某个目标状态或者同时到达多个目标状态的潜能,并以此指导模拟过程直到最终搜索到一条能同时覆盖多个目标状态的状态序列.此外,该文采用了基于路径约束求解的激励生成方式,这种方式结合了具体模拟和符号模拟技术,符号模拟沿着具体执行路径提取分支条件构成路径约束,通过约束条件的翻转与求解能够有效地产生输入向量,以一种较均衡的模式遍历设计的状态空间,帮助验证快速覆盖到目标.实验结果表明,该文方法能够有效地同时验证设计中的多个目标状态.
In this paper,we propose a test generation method to cover multiple hard-to-reach states,which operates in an abstraction-guided simulation framework.An evaluation function,which considers the global abstract distance information for one state to different target states,is used to evaluate the potentiality of each candidate next state to targets and guide the simulation processes to cover multiple target states.In addition,apath constraint solving based test generation method which combines concrete simulation and symbolic simulation is used.Symbolic simulation walks in the design following the concrete path and extracts the corresponding symbolic expressions of the branch conditions in the path as path constraints.The test generation engine can generate valid input vectors through constraint mutation and solving,and it helps to search state in the design state space in a balanced manner.Experimental results show that our approach is effective in covering multiple target states.
In this paper,we propose a test generation method to cover multiple hard-to-reach states,which operates in an abstraction-guided simulation framework.An evaluation function,which considers the global abstract distance information for one state to different target states,is used to evaluate the potentiality of each candidate next state to targets and guide the simulation processes to cover multiple target states.In addition,apath constraint solving based test generation method which combines concrete simulation and symbolic simulation is used.Symbolic simulation walks in the design following the concrete path and extracts the corresponding symbolic expressions of the branch conditions in the path as path constraints.The test generation engine can generate valid input vectors through constraint mutation and solving,and it helps to search state in the design state space in a balanced manner.Experimental results show that our approach is effective in covering multiple target states.
引文
[1]Shyam S,Bertacco V.Distance-guided hybrid verification with GUIDO//Proceedings of the International Conference on Design,Automation and Test in Europe.Munich,Germany,2006:1211-1216
[2]Nanshi K,Somenzi F.Guiding simulation with increasingly refined abstract traces//Proceedings of the ACM/IEEE Design Automation Conference.San Francisco,USA,2006:737-742
[3]Paula F M D,Hu A J.An effective guidance strategy for abstraction-guided simulation//Proceedings of the ACM/IEEE Design Automation Conference.San Diego,USA,2007:63-68
[4]Wu W X,Hsiao M S.Efficient design validation based on cultural algorithms//Proceedings of the International Conference on Design,Automation and Test in Europe.Munich,Germany,2008:402-407
[5]Zhang T,Lv T,Li X W.An abstraction-guided simulation approach using Markov models for microprocessor verification//Proceedings of the International Conference on Design,Automation and Test in Europe.Dresden,Germany,2010:484-489
[6]Wang J,Li H W,Lv T,et al.Functional test generation guided by steady-state probabilities of abstract design//Proceedings of the International Conference on Design,Automation and Test in Europe.Dresden,Germany,2014:1-4
[7]Zhou Y H,Wang T C,Lv T,et al.Path constraint solving based test generation for hard-to-reach states//Proceedings of the Asian Test Symposium.Yilan,China,2013:239-244
[8]Chatterjee D,Bertacco V.Activity-based refinement for abstraction-guided simulation//Proceedings of the IEEEInternational High Level Design and Test Workshop.San Francisco,USA,2009:146-153
[9]Wang J,Li H W,Li X W.A novel abstraction-guided simulation approach using posterior probabilities for verification//Proceedings of the International Symposium on VLSI Design,Automation and Test.Hsinchu,China,2014:1-4
[10]Liu L Y,Vasudevan S.STAR:Generating input vectors for design validation by static analysis of RTL//Proceedings of the IEEE International High Level Design and Test Workshop.San Francisco,USA,2009:32-37
[11]Liu L Y,Vasudevan S.Efficient validation input generation in RTL by hybridized source code analysis//Proceedings of the International Conference on Design,Automation and Test in Europe.Grenoble,France,2011:1-6
[12]Liu Jie,Xu Wei-Jun,Xia Yu-Wen,Qin Ji-Long.Constrained random in design verification.China Integrated Circuit,2006,15(11):28-32(in Chinese)(刘杰,徐伟俊,夏宇闻,秦冀龙.设计验证中的随机约束.中国集成电路,2006,15(11):28-32)
(1)http://www.google.com/patents/US20120266118
(1)VIS Homepage.http://vlsi.colorado.edu/~vis/
(1)CVC3 Homepage.http://www.cs.nyu.edu/acsys/cvc3/doc/index.html
(2)http://www.cerc.utexas.edu/itc99-benchmarks/bench.html
(3)http://bbs.eetop.cn/thread-329826-1-1.html
[2]Nanshi K,Somenzi F.Guiding simulation with increasingly refined abstract traces//Proceedings of the ACM/IEEE Design Automation Conference.San Francisco,USA,2006:737-742
[3]Paula F M D,Hu A J.An effective guidance strategy for abstraction-guided simulation//Proceedings of the ACM/IEEE Design Automation Conference.San Diego,USA,2007:63-68
[4]Wu W X,Hsiao M S.Efficient design validation based on cultural algorithms//Proceedings of the International Conference on Design,Automation and Test in Europe.Munich,Germany,2008:402-407
[5]Zhang T,Lv T,Li X W.An abstraction-guided simulation approach using Markov models for microprocessor verification//Proceedings of the International Conference on Design,Automation and Test in Europe.Dresden,Germany,2010:484-489
[6]Wang J,Li H W,Lv T,et al.Functional test generation guided by steady-state probabilities of abstract design//Proceedings of the International Conference on Design,Automation and Test in Europe.Dresden,Germany,2014:1-4
[7]Zhou Y H,Wang T C,Lv T,et al.Path constraint solving based test generation for hard-to-reach states//Proceedings of the Asian Test Symposium.Yilan,China,2013:239-244
[8]Chatterjee D,Bertacco V.Activity-based refinement for abstraction-guided simulation//Proceedings of the IEEEInternational High Level Design and Test Workshop.San Francisco,USA,2009:146-153
[9]Wang J,Li H W,Li X W.A novel abstraction-guided simulation approach using posterior probabilities for verification//Proceedings of the International Symposium on VLSI Design,Automation and Test.Hsinchu,China,2014:1-4
[10]Liu L Y,Vasudevan S.STAR:Generating input vectors for design validation by static analysis of RTL//Proceedings of the IEEE International High Level Design and Test Workshop.San Francisco,USA,2009:32-37
[11]Liu L Y,Vasudevan S.Efficient validation input generation in RTL by hybridized source code analysis//Proceedings of the International Conference on Design,Automation and Test in Europe.Grenoble,France,2011:1-6
[12]Liu Jie,Xu Wei-Jun,Xia Yu-Wen,Qin Ji-Long.Constrained random in design verification.China Integrated Circuit,2006,15(11):28-32(in Chinese)(刘杰,徐伟俊,夏宇闻,秦冀龙.设计验证中的随机约束.中国集成电路,2006,15(11):28-32)
(1)http://www.google.com/patents/US20120266118
(1)VIS Homepage.http://vlsi.colorado.edu/~vis/
(1)CVC3 Homepage.http://www.cs.nyu.edu/acsys/cvc3/doc/index.html
(2)http://www.cerc.utexas.edu/itc99-benchmarks/bench.html
(3)http://bbs.eetop.cn/thread-329826-1-1.html