层次数据通路的等价性验证方法

《层次数据通路的等价性验证方法》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第29卷第6期哈尔滨1二程大学学报V01．29№．62008年6月JournalofHarbinEngineeringUniVersityJurL2008．__I-【j同层次数据通路的等价性验证方法李东海，马光胜，胡靖(哈尔滨工程大学计算机科学与技术学院，黑龙江哈尔滨150001)摘要：为了实现多项式数据通路的初始算术规范与其相应的寄存器传输级实现之间的等价性验证，提出了一个有序的、简化的和正则的带权值广义表模型表达字级多项式，同时给ff{了该模型的化简、加法和乘法运算规则，基于这些规则对寄存器传输级电路构建其相应有序的、简化的和正则的带权值广义表模型．实验

2、结果表明，该模型对寄存器传输级电路的等价性验证与‘BMD相比。不论是在存储空间还是在cPu时间花费上均有明显的优势．关键词：字级多项式；带权值广义表；数据通路；等价验证中图分类号：TP391．7文献标识码：A文章编号：1006—7043(2008)06一0583一06ThemethodofequiValenceVerificationforhighleVeldatapathsLIDong—hai，MAGuang．sheng，HUJing(CollegeofComputerScienceandTechnology，HarbinEngineeringUniver

3、sity，Harbin150001，China)Abstr卵t：Toimplementtheequivalenceverificationbetweeninitialarithmeticspecificationsforpolynomialdatapathsandtheircorrespondingregistertransferlevelimplementationortheoptimizedcounterparts，anord∈red，reducedandcanonicalweightedgeneralizednstmodelforword—levelp

4、olynomialwaspresented．Theoperationalrulesforreduction，additionandmultiplicationweregiven．0nthebasisoftheserules，weconstructedtherelevantordered，reducedandcanonicalweightedgeneralizedlistmodeIforregistertrans—ferlevelcircuits．ExperimentaIresultsdemonstratedthat，comparedtheequivalent

5、verificationwithmulti—plicativebinarymomentdiagram(*BMD)，theproposedmethodisobviouslybetterthan*BMDinCPUtimeconsumptionandinmemoryspaceoccupancy．K

6、eywords：word—levelpolynomial；weightedgeneralizedlist；datapaths；equivalenceverification数字系统设计的规模和复杂度的日益增大，使得在设计周期的早期阶段进行验证成为必要．这就要求在较高的抽

7、象层次上(例如行为级、算术级以及RTI。(registertransferlevel))开发强健的、自动化的验证T具．同时，在许多数字系统例如音频、视频和多媒体的DSP(digitalsignalprocessing)设计中，广泛的采用实现多项式运算的数据通路Jj，文献[2]用字级多项式模型描述高层次数据通路，并在高层次综合阶段实现了数据通路的匹配和分配T作；基于多项式符号代数方法，一些学者实现了一些有效的算法，例如数据通路的综合算法∞]、复杂的库映收稿日期：2007—07一05．基金项目：固家自然科学基金资助项日(60273081)．作者简介：李东海(19

8、77一)，男，博士研究生，E—mail：ldhl215l@tonLCOm：马光胜(1944一)，男，教授。博士生导师．射算法[4]和低功耗优化算法[5【．如何验证这些数据通路综合前后的等价性是当前研究的热点．传统的等价验证方法主要有：基于判决图的方法例如BDDL6j(binarydecisiondiagram)、。BMI)L7](multi—plicativebinarymomentdiagram)和。PHDDl8](multip“cativepowerhybriddecisiondiagram)等，以及基于可满足性SATL9](satisfiability

9、)的方法和基于算术转换AT[10](arithmet