现代电子技术
現代電子技術
현대전자기술
MODERN ELECTRONICS TECHNIQUE
2005年
20期
57-60
,共4页
形式化验证%时序电路的验证%Tempura语言%逻辑公式
形式化驗證%時序電路的驗證%Tempura語言%邏輯公式
형식화험증%시서전로적험증%Tempura어언%라집공식
对硬件的形式化验证是硬件验证的一个发展方向,形式化验证一个时序电路就是证明电路的实现是否满足他的规格描述.本文提出了用等式逻辑ε的一个公式Ws来表示电路的实现,用Tempura的程序B表示对该电路的特性描述.公式P(C)B引入来证明电路的正确性,这里P是电路的初始状态,是从Ws中抽取的,另外还要从Ws提取输出等式.这样,一旦证明了P(C)B,就能证明实现满足规格描述.最后,给出了一个例子来说明此证明方法.
對硬件的形式化驗證是硬件驗證的一箇髮展方嚮,形式化驗證一箇時序電路就是證明電路的實現是否滿足他的規格描述.本文提齣瞭用等式邏輯ε的一箇公式Ws來錶示電路的實現,用Tempura的程序B錶示對該電路的特性描述.公式P(C)B引入來證明電路的正確性,這裏P是電路的初始狀態,是從Ws中抽取的,另外還要從Ws提取輸齣等式.這樣,一旦證明瞭P(C)B,就能證明實現滿足規格描述.最後,給齣瞭一箇例子來說明此證明方法.
대경건적형식화험증시경건험증적일개발전방향,형식화험증일개시서전로취시증명전로적실현시부만족타적규격묘술.본문제출료용등식라집ε적일개공식Ws래표시전로적실현,용Tempura적정서B표시대해전로적특성묘술.공식P(C)B인입래증명전로적정학성,저리P시전로적초시상태,시종Ws중추취적,령외환요종Ws제취수출등식.저양,일단증명료P(C)B,취능증명실현만족규격묘술.최후,급출료일개례자래설명차증명방법.
