Fusion of Meta-Scalable Theorem Prover and Parallel Model Checker to Realize Large-Scale Fast Formal Verification

2022 Fiscal Year Final Research Report

• Project/Area Number: 19K11821
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Shinshu University
• Principal Investigator: Wasaki Katsumi 信州大学, 学術研究院工学系, 教授 (70271492)
• Project Period (FY): 2019-04-01 – 2023-03-31
• Keywords: 非同期並列システム / ハードウェアコンパイラ / 定理証明器 / モデル検査器 / 形式検証系 / 関数型言語系 / 状態空間生成 / ペトリネット

Outline of Final Research Achievements

For the purpose of rigorous property checking of circuits to be verified, a study was conducted to model the connections between logic gate elements using message-passing parallel computation. Theorem proving was done by property checking on the circuit structure and the validity of the connections. As an actual example of PE with scalable and repetitive structures, we actually wrote a theorem proof for a high radix compressor module of a high-speed multiplier circuit using multisort algebra as the theoretical basis, and performed machine verification using the Mizar proof checker. The desired properties, such as the correctness of the circuit synthesis structure and input-output relations, were successfully verified.

Free Research Field

数理情報学

Academic Significance and Societal Importance of the Research Achievements

LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ、状態空間生成器を用いて初期状態から駆動するが、状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため、削除可能状態のオンライン判定アルゴリズムに関する検討を行った点に学術的意義がある。なおペトリネット検証系に関する基礎研究として、サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知、一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た点についても学術的意義がある。