计算机辅助设计与图形学学报
計算機輔助設計與圖形學學報
계산궤보조설계여도형학학보
JOURNAL OF COMPUTER-AIDED DESIGN & COMPUTER GRAPHICS
2008年
2期
137-143
,共7页
杨志%马光胜%冯刚%邵晶波
楊誌%馬光勝%馮剛%邵晶波
양지%마광성%풍강%소정파
高层次设计%定界模型检验%吴方法%形式验证
高層次設計%定界模型檢驗%吳方法%形式驗證
고층차설계%정계모형검험%오방법%형식험증
以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.
以吳方法為理論基礎,提齣一種針對高層次設計驗證的定界模型檢驗方法.通過使用多項式等式建模高層次設計和待驗證性質,將定界模型檢驗問題轉化為定理證明問題,併用吳方法有效地解決該定理證明問題.實驗結果錶明,與基于佈爾SAT、基于LP的RTL SAT以及基于非線性求解器的性質檢驗方法相比,該方法在時間消耗上具有相噹大的優勢.
이오방법위이론기출,제출일충침대고층차설계험증적정계모형검험방법.통과사용다항식등식건모고층차설계화대험증성질,장정계모형검험문제전화위정리증명문제,병용오방법유효지해결해정리증명문제.실험결과표명,여기우포이SAT、기우LP적RTL SAT이급기우비선성구해기적성질검험방법상비,해방법재시간소모상구유상당대적우세.
