微电子学与计算机
微電子學與計算機
미전자학여계산궤
MICROELECTRONICS & COMPUTER
2013年
6期
43-47
,共5页
GSTE%形式化验证%并发性质%模型检验%断言图
GSTE%形式化驗證%併髮性質%模型檢驗%斷言圖
GSTE%형식화험증%병발성질%모형검험%단언도
GSTE%formal verification%concurrent property%model checking%assertion graph
由于GSTE的性质描述断言图的时序特性,使其不能够简洁易懂地描述电路的并发性质,因此将meet运算符引入GSTE ,重新定义GSTE断言图及其验证算法,使之能更简洁的描述和验证数字电路的并发性质,实验表明引入meet运算符后的算法能够降低验证的复杂度.
由于GSTE的性質描述斷言圖的時序特性,使其不能夠簡潔易懂地描述電路的併髮性質,因此將meet運算符引入GSTE ,重新定義GSTE斷言圖及其驗證算法,使之能更簡潔的描述和驗證數字電路的併髮性質,實驗錶明引入meet運算符後的算法能夠降低驗證的複雜度.
유우GSTE적성질묘술단언도적시서특성,사기불능구간길역동지묘술전로적병발성질,인차장meet운산부인입GSTE ,중신정의GSTE단언도급기험증산법,사지능경간길적묘술화험증수자전로적병발성질,실험표명인입meet운산부후적산법능구강저험증적복잡도.
@@@@This paper extends the GSTE with a new a new operator “meet” .We modify the assertion graph and the algorithm of GSTE to make it can succinctly describe and verify the concurrent properties of digital circuits .The experiment result express that the new method can reduce the complexity of verification .
