期刊文献+

基于线性带权值的广义表的模型检验方法

Method of model checking based on linear weighted generalized list
下载PDF
导出
摘要 提出了一个线性带权值的广义表(Linear Weighted Generalized List,LWGL)模型,同时给出了LWGL加法和乘法、析取和合取运算规则,实现了基于LWGL的高层次模型检验方法。实验结果表明LWGL模型对高层次模型检验是有效的。 A model of linear weighted generalized list (LWGL) is proposed.The rules of addition,multiplication,union and intersect for LWGL are proposed.Based on the LWGL,it is implemented for high level model checking.Experimental results show that LWGL used for high level model checking is effective.
作者 刘恩军
出处 《计算机工程与应用》 CSCD 北大核心 2008年第29期88-91,共4页 Computer Engineering and Applications
关键词 线性带权值的广义表 模型检验 验证 数据流图 linear weighted generalized list model checking verification data flow diagrams
  • 相关文献

参考文献9

  • 1Bryant R E.Graph based algorithms for Boolean function manipulation[J].IEEE Transaction on Computers,1986,C-35(8):677-691.
  • 2Clarke E,Biere A,Raimi A,et al.Bounded model checking using satisfiability solving[J].Formal Methods in System Design,2001,19 (1):7-34.
  • 3Prasad M R,Biere A,Gupta A.A Survey of Recent Advances in SAT-based Formal Verification[J].International Journal on Software Tools for Technology Transfer,2005,7(2): 156-173.
  • 4Keim M,Dreehsler R,Becker B,et al.Polynomial formal verification of multiplier[J].Formal Methods in System Design,2003,22(1):39-58.
  • 5Drechsler R,Becker B,Ruppertz S.The K*BMD:a verification data structre[J].IEEE Design & Test, 1997, 14( 2 ) : 51-59.
  • 6王海霞,韩承德.整数乘法电路的形式化验证方法研究[J].计算机研究与发展,2005,42(3):404-410. 被引量:6
  • 7DU Z J,MA G S,FENG G.A new model for Verifieation[J],Journal of Harbin Institute of Technology(New Serise),2007,14(3):305-310.
  • 8Peymandoust A,DeMicheli G.Application of symbolic computer algebra in high-level data-flow synthesis[J].IEEE Transaction on Computer-Aided Design,2003,22(9) : 1154-1165.
  • 9Brayton R K,Sangiovanni A,Aziz A,et al.VIS:a system for verification and synthesis[C]//Proeeeding of the Eighth International Conference on Computer Aided Verification, 1996:428-432.

二级参考文献12

  • 1R. E. Bryant. On the complexity of VLSI implementations and graph representations of Boolean functions with applications to integer multiplication. IEEE Trans. on Computers, 1991, 40(2) : 205--213.
  • 2B. Yang, Y.-A. Chen, R. Bryant, et al. Space-and-time-efficient BDD construction via working set control. The Asia and South Pacific Design Automation Conf. (ASPDAC'98),Yokohama, Japan, 1998.
  • 3H. Ochi, K. Yasuuoka, S. Yajima. Breadth-first manipulation of very large binary-decision diagrams. In: Proc. of ICCAD-93, Los Alamitos, CA: IEEE Computer Society Press, 1993. 48--55.
  • 4J. R. Bureh. Using BDDs to verify multipliers. In: Proc. of the 28th Design Automation Conf. Los Alamitos, CA: IEEE Computer Society Press, 1991. 408--412.
  • 5J. Jain, J. Bitner, M. Abadir, et al. Indexed BDDs:Algorithmic advances in techniques to represent and verify Boolean functions. IEEE Trans. on Computers, 1997, 46(11) : 1230--1245.
  • 6Y. T. Lai, S. Sastry. Edge-valued binary-decision diagrams for multi-level hierarchical verification. In: Proc. of the 29th Design Automation Conf. Los Alamitos, CA: IEEE Computer Society Press, 1992. 608--613.
  • 7E. M. Clarke, K. L. McMillan, X. Zhao, et al.Spectral transforms for large Boolean functions with applications to technology mapping. In: Proc. of the 30th ACM/IEEE Design Automation Conf. Los Alamitos, CA: IEEE Computer Society Press, 1993. 54--60.
  • 8R. E. Bryant, Y. A. Chen. Verification of arithmetic functions with binary moment diagrams. In: Proc. of the 32nd ACM/IEEE Design Automation Conf. Los Alamitos, CA: IEEE Computer Society Press, 1995. 535--541.
  • 9E.M. Clarke, M. Fujita, X. Zhao. Hybrid decision diagrams:Overcoming the limitations of MTBDDs and BMDs. In: Proc. of the 1995 IEEE Int'l Conf. on Computer Aided Design. Los Alamitos, CA: IEEE Computer Society Press, 1995. 159--163.
  • 10Y. A. Chen, R. E. Bryant. *PHDD: An efficient graph representation for floating point circuit verification. In: Proc. of the Int'l Conf. on Computer Aided Design. Los Alamitos, CA:IEEE Computer Society Press, 1997. 2--7.

共引文献5

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部