並列モデルであるシストリックアレイのレジスタ転送レベルでのモデルに対して振る舞い検証を行う．シストリックアレイは計算セルを複数個用意し，一定の繰り返し構造により規則的に配置することで全体として並列計算アルゴリズムを実行するシステムである．例えばW1型シストリックアレイとして，セルを1次元上に配置し，システム全体としてコンボリューション積を得るアーキテクチャが既に提案されている．本研究ではW1型シストリックアレイのLOTOS記述から得られたプロセストレースグラフに対してモデル検証を行う．具体的にはモデル検査ツールCADPを用いて，トレースグラフ内の実行パスとしてシストリックアレイが仕様通りに振る舞う動作が存在するか，クロック同期時に演算器の遅延が大きすぎてパイプライン動作が不調になるケースが存在するか，など多様な探索を試みる．