PR

 米Chrysalis Symbolic Design, Inc.(ホームページ)は,モデル・チェッキング用のフォーマル・ベリファイアを複数発売すると発表した。同社は,展示会などでモデル・チェッキング用のフォーマル・ベリファイアについて一部公表していたが,今回正式に製品発表した。モデル・チェッキング用のフォーマル・ベリファイアは,設計結果が設計仕様(プロパティ)に沿っているかどうかを解析するためのツールで,プロパティ・チェッカとも呼ばれる。数学的に解析するため,シミュレーションのようなテスト・ベクトルが不要なうえ,原理的には検証の漏れがない。

 今回,Chrysalis社が発表したのは汎用のモデル・チェッキング用のフォーマル・ベリファイア「Design INSIGHT Formal Model Checker」(リリース文)と,用途を特定したモデル・チェッキング用のフォーマル・ベリファイア「Formal Design Rule Check (FDRC)」である(リリース文)。FDRCはDesign INSIGHT Formal Model Checkerのサブセットといえる。

 FDRCは4品種発表した。Clock Domain Checker (CDC) FDRC, One-Hot Checker (OHC) FDRC, Scan Chain Checker (SCC) FDRC, そしてReset Logic Checker (RLC) FDRCである。CDC FDRCは,マルチクロック・システムにおいて信号間の同期が取れているかどうかを検証する。OHC FDRCは,モジュールの入力が特定の値になるかどうかをチェックする。CDC FDRCとOHC FDRCは1999年4月に出荷の予定。SCC FDRCとRLC FDRCは1999年第2四半期の出荷予定で,それぞれスキャン設計のチェック,リセットのチェック用。なお,Design INSIGHT Formal Model Checkerは即日出荷する。