期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于多项式符号代数方法的高层次数据通路的等价验证 被引量：2

Equivalence Verification of High-Level Datapaths Based on Polynomial Symbolic Algebra
在线阅读 下载PDF
导出
摘要 基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求.由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法.深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式.从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Grbner基计算的有效代数求解算法.针对不同基准数据通路的实验结果表明了该算法的有效性. As the size and functional complexity of IC designs increase, it has become important to address verification issues at early stages of the IC design flow. This means that IC designers require automated verification tools at higher levels of abstraction. Because of this, formal verification methods, such as equivalence verification, have become important for register transfer level or behavioral level verification. However, most of the existing techniques for equivalence verification are based on BDD or Boolean SAT, which are generally geared towards verification of designs implemented at lower levels of abstraction, such as gate level and circuit/layout level, and can hardly satisfy the high-level verification requirements. So in this paper, a new algorithm for the equivalence verification of high-level datapaths based on polynomial symbolic algebra is proposed. After researching further the method to describe behaviors of complex datapaths using polynomial expressions, the general form of the polynomial set representations for high-level datapaths is obtained. The functional equivalence of high-level datapaths is then defined from the perspective of common zeros of polynomial sets, and an efficient algebraic solution based on Groebner basis computation is presented. Experimental results on a variety of public benchmark suites show the efficiency of the proposed approach.
作者 杨志 马光胜 张曙
机构地区 哈尔滨工程大学计算机科学与技术学院 哈尔滨工程大学信息与通信工程学院
出处 《计算机研究与发展》 EI CSCD 北大核心 2009年第3期513-520,共8页 Journal of Computer Research and Development
基金 国家自然科学基金项目(60273081)~~
关键词 高层次数据通路 等价验证 多项式符号代数 形式验证 电子设计自动化 high-level datapaths equivalence verification polynomial symbolic algebra formalverification electronic design automation
分类号 TP391.7 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献15

  • 1韩俊剐,杜慧敏.数字硬件的形式化验证[M].北京:北京大学出版社,2001.
  • 2Bryant R E. Graph-based algorithms for Boolean function manipulation [J]. IEEE Trans on Computers, 1986, C-35 (8) : 677-691
  • 3Bryant R E, Chen Y A. Verification of arithmetic circuits with binary moment diagrams [C] //Proc of the 32nd Design Automation Conf. New York: ACM, 1995:535-541
  • 4王海霞,韩承德.整数乘法电路的形式化验证方法研究[J].计算机研究与发展,2005,42(3):404-410. 被引量：6
  • 5Ciesielski M, Kalla P, Askar S. Taylor expansion diagrams: A canonical representation for verification of data flow designs [J]. IEEE Trans on Computers, 2006, 55(9) : 1188- 1201
  • 6Goldberg E I, Prasad M R, Brayton R K. Using SAT for combinational equivalence checking [C] //IEEE/ACM Design, Automation and Test in Europe Conf. Piscataway, NJ: IEEE, 2001:114-121
  • 7李光辉,李晓维.基于增量可满足性的等价性检验方法[J].计算机学报,2004,27(10):1388-1394. 被引量：7
  • 8邓澍军,吴为民,边计年.RTL验证中的混合可满足性求解[J].计算机辅助设计与图形学学报,2007,19(3):273-278. 被引量：11
  • 9Brinkmann R, Drechsler R. RTL datapath verification using integer linear programming [C] //Proc of the 7th Asia and South Pacific Design Automation Conf. Washington, DC: IEEE Computer Society, 2002:741-746
  • 10Smith J, Micheli G D. Polynomial circuit models for component matching in high-level synthesis [J]. IEEE Trans on VLSI Systems, 2001, 9(6): 783-800

二级参考文献57

  • 1郑伟伟,吴为民,边计年.基于线性规划的RTL可满足性求解和性质检验[J].计算机辅助设计与图形学学报,2006,18(4):538-544. 被引量：7
  • 2R. 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.
  • 3B. 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.
  • 4H. 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.
  • 5J. 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.
  • 6J. 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.
  • 7Y. 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.
  • 8E. 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.
  • 9R. 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.
  • 10E.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.

共引文献18

同被引文献33

  • 1Badawy W,Jullien G.System-on-Chip for Real Time Applications[M].Amsterdam,Netherlands:Kluwer Academic Publishers,2003.
  • 2IEEE Standard 1364.IEEE Standard Verilog Hardware Description Language[S].Los Alamitos,CA:IEEE Computer Society,2001.
  • 3Muraoka M,Nishi H,Morizawa R K.Design methodology for SoC architectures based on reusable virtual cores[C]//Proc of Asia and South Pacific Design Automation Conf 2004.Piscataway,NJ:IEEE,2004:256-262.
  • 4Miti(c) M,Stoj(c)ev M.An overview of on-chip buses[J].Facta Universitatis-series:Electronics and Energetics,2006,19(3):405-428.
  • 5IBM.The CoreConnec Bus Architecture[EB/OL].1999[2013-11-15].https://www-01.ibm.com/chips/techlib/techlib.nsf/techdocs/852569B20050FF77852569910050C0FB/MYMfile/crcon_wp.pdf.
  • 6Andrews J.Co-verification of Hardware and Software for ARM SoC Design[M].Oxford:Newnes,2004:89-94.
  • 7OpenCores Organization.Specification for the:WISHBONE System-on-Chip (SoC) interconnection architecture for portable IP cores Revision:B.4[S/OL].2010[2013-11-15].http://opencores.org/websvn,filedetails? repname =pif2wb&path =% 2Fpif2wb% 2Ftrunk% 2FPIF2WB UserManual.pdf.
  • 8Rudolf Usselmann.WISHBONE interconnect matrix IP core[S/OL].2002.[2013-11-15].http://opencores.org/websvn,filedetails? repname =wb_conmax&path=% 2Fwb_conmax%2Ftrunk % 2Fdoc% 2Fconmax.pdf.
  • 9Morawice A,Ubar R,Raik J.Cycle-based simulation algorithms for digital systems using high-level decision diagrams[C]//Proc of the 5th Design,Automation and Test in Europe Conf and Exhibition 2000.Piscataway,NJ:IEEE,2000:743.
  • 10Mattia M,Del Giudice P.Efficient event-driven simulation of large networks of spiking neurons and dynamical synapses[J].Neural Computation,2000,12(10):2305-2329.

引证文献2

二级引证文献4

计算机研究与发展
2009年 第3期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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