Failure trace解析に基づくGasP回路の形式的検証  [in Japanese] Analyzing Failure Traces for Verification of GasP Circuits  [in Japanese]

GasP回路は,正常に動作するためのタイミング制約が非常に厳しい非同期式回路である.形式的検証ツールは,回路がタイミング制約を満足するか否かを検査するためには有効であるが,回路に誤りが存在する場合にそれを除去する方法を知るのが困難である.本研究では,GasP回路の形式的モデルを定義した上で,形式的検証ツールの出力するfailure traceの解析によって,GasP回路が正しく動作するためのタイミング条件を自動的に導出する手法を提案する.

Recently, timed circuits are designed with aggressive and complex sets of timing constraints, and it is difficult for the desigsners to obtain sufficient timing constraints. In this work, we present a formal model of GasP circuits, and propose a fully automatic way to obtain sufficient timing constraints for a given GasP circuits to work correctly by analysing failure traces that a formal verification tool produces.