计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2007年
7期
1138-1144
,共7页
李暾%屈婉霞%郭阳%刘功杰%李思昆
李暾%屈婉霞%郭暘%劉功傑%李思昆
리돈%굴완하%곽양%류공걸%리사곤
谓词抽象%Verilog约束逻辑编程%模型检验%符号模拟
謂詞抽象%Verilog約束邏輯編程%模型檢驗%符號模擬
위사추상%Verilog약속라집편정%모형검험%부호모의
利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.
利用人工智能最新研究成果--約束邏輯編程對Verilog描述進行謂詞抽象,併與目前基于SAT的方法進行瞭比較.首先通過符號模擬建立Verilog的形式化模型,然後結閤要抽象的謂詞,將謂詞抽象問題轉化為約束邏輯編程問題併進行求解.該方法的優點是在計算抽象繫統時,不需要像基于SAT的方法那樣將字級約束打散成位級約束,求解效率顯著提高;提供瞭一箇統一的框架用于描述各種約束.實驗結果錶明,與基于SAT的抽象技術相比,基于約束邏輯編程的抽象方法的求解速度有顯著提高.
이용인공지능최신연구성과--약속라집편정대Verilog묘술진행위사추상,병여목전기우SAT적방법진행료비교.수선통과부호모의건립Verilog적형식화모형,연후결합요추상적위사,장위사추상문제전화위약속라집편정문제병진행구해.해방법적우점시재계산추상계통시,불수요상기우SAT적방법나양장자급약속타산성위급약속,구해효솔현저제고;제공료일개통일적광가용우묘술각충약속.실험결과표명,여기우SAT적추상기술상비,기우약속라집편정적추상방법적구해속도유현저제고.
