ホーム > HOT TOPIX > SOCインテグレーションにおけるフォーマル検証の適用 Jasper Design Automation

SOCインテグレーションにおけるフォーマル検証の適用 Jasper Design Automation

SOCインテグレーションにおけるフォーマル検証の適用

by Antonio Dimalanta, Field Applications Engineer, and Sebastian Skalberg, Field Applications Engineer Manager, Jasper Design Automation

イントロダクション

SoC インテグレーションでは、デザインが大規模になるにつれ、着実に検証が複雑になってきています。 今日のSoCは、大規模IPブロック、高速IO、複雑な低消費電力の実装、デバッグやテスト用論理などを組み合わせています。これらはチップレベルのコントローラによって管理され、動作のカスタマイズや制御のためにソフトウェアでコンフィギュレーション可能なステータスレジスタをもっていることがしばしばあります。これらのSoCにおける様々なブロックの境界と、ブロック間の変化する相互作用と仕様は、しばしば検証の焦点であり、最も緊急性の高い課題となっています。

 

この記事では、フォーマル検証がSoCの検証の全体的な品質を向上させながら、時間と労力を節約し、これらの課題を解決するのにどう使用されるかを検討します。また明らかなROIの例と共に詳細例を挙げてフォーマル検証がどのように広められているのかをご紹介します。ここでは、接続チェックやパッドリング検証を取り上げますが、これらは従来シミュレーションでは困難なコンフィギュレーション・ステータスレジスタ検証と共に、増大しているSoCの要素間の複雑な接続を扱う必要があります。さらに、チップのタイミング制約が正しいことを確実にするためのマルチサイクルパス検証についても触れています。

フォーマル検証の適用

フォーマル検証は、ブロックレベルのモジュールに対して、バグハンティングやプロトコル検証、デザイン固有の仕様に対するアサーション検証に適用されてきました。取り扱える規模や抽象化技術の進歩で、より複雑な回路を含む、より抽象度の高いレベルでのフォーマル検証が可能になりました。

 

フォーマル技術の利点は明らかで、テストベクター無しに網羅検証が出来ることです。デバッグも強力です。フォーマル検証は、網羅的な数学的証明であり、設計チームと検証チームが想定していなかったコーナーケースを含む、すべてのケースがカバーされます。そして、フォーマル検証はすべての可能なケースをカバーしているので、テストベクターが必要ありません。これは設計チームと検証チームがテスト環境や特定のダイレクトテストを作成するための多大な労力を軽減します。反例が見つかると、対応する信号の波形が自動的に生成されますので設計チームと検証チームは、すぐに波形を調べて必要な修正を行うことができます。

SoCインテグレーションにおける多様なアプリケーション

SoCインテグレーションの領域には、４つのキーアイテムがあります。

  1. チップレベルの接続検証
  2. 自動化されたパッドリング検証
  3. レジスタ検証
  4. マルチサイクルパスの生成

 

チップレベルの接続検証：SoCインテグレーションにおいて、サブシステムやブロック間のピンの接続を確立するのは重要で、機能的な信号、バス、general purpose IO (GPIO)ピン、およびパッドを含みます。接続に問題があるために機能検証でフェイルを引き起こすというつまらないデバッグを避けるために、接続検証はインテグレーションの早い段階で実施するべきです。フォーマル検証は接続の確立、解析、およびデバッグの問題に自動化と網羅性をもたらします。

 

自動化されたパッドリング検証：SoCインテグレーションにおいて、サブシステムやブロック間のピンの接続は、パッドリングのコンフィギュレーションを含んでいます。チップのコンフィギュレーションが増えるのに従って、リングはしばしば変更されます。各コンフィギュレーションで意図している接続を捉えて、パッドリング検証にフォーマル技術を利用することによって、新しいコンフィギュレーションを容易に加えることができます。フォーマル検証が可能性のあるすべての組合せを完全に探索しますので、シミュレーションではその特定が難しいような、接続が存在すべきでないコーナーケースを特定できます。

 

レジスタ検証：制御ステータスレジスタはハードウェアとソフトウェア間の橋渡しをしています。そして、これらのレジスタの仕様に誤りがあれば下流の設計に誤りをもたらします。フォーマル検証は難しいコーナーケースの問題やアドレス可能なレジスタアクセスに対する順序の組み合わせのすべてについて探索します。

 

マルチサイクルパスの生成：静的タイミング解析において、RTL設計者は、特定のパスに対してより多くのサイクルを許容するために、マルチサイクルパスを指定できます。このようなコマンドにおける誤りが、シリコン上でタイミング問題を引き起こすことがあります。これらのコマンドはほとんど手入力ですので、意図しない誤りを発生させる可能性があります。また、シミュレーションでこれらのコマンドを検証するのは難しい場合があります。波形生成によるフォーマル技術によって、ユーザは指定したマルチサイクルパスに沿って動作を理解して、マルチサイクルパスに対して指定したサイクル領域が正しいことを検証できます。

チップレベルの接続検証

SoCの仕様とマイクロアーキテクチャが完成した後に、デザインは論理的なモジュールに分割されます。時間と共に、これらの論理パーティションは、レイアウトで物理パーティションになります。そして、デザインによっては、かなりの量のグル―ロジックがパーティション間に取り入れられます。論理と物理パーティション間には、１対１の対応が取れていないものがあるかもしれません。また、パーティション、グルーロジックやそれらの接続には、時間が経つにつれて著しい変化があるかもしれません。

 

チップレベルにおけるこれらの接続は、通常手動かスクリプトで行われます。 検証は従来、ダイレクトテストかランダムシミュレーションで長い間行われますが、インターフェースの問題を特定の原因まで追跡するのは、非常に難しいです。 例えば、2ビットが1つのモジュールから別のモジュールの間でスワップされるなら、そのインタフェースにかかわるテストは機能不全を示しますが、原因としてビットスワッピングに必ずたどり着くというわけではないでしょう。大変な時間を掛け、他のすべての原因を除外して問題を見つけられるか、どうかは、設計チームと検証チーム次第になります。


 

図１では、アナログとデジタルのブロックを含んだミックスドシグナルチップを考えます。デジタルブロックは、アナログブロックのいくつかのパラメータを制御して、標準インターフェースを通してプログラムできます。


jasper01.jpg図 1. ミックスドシグナルチップのブロックダイアグラム

 

デジタルとアナログのブロック間の接続は、特にグルーロジックと他の制御信号がある場合、通常検証が難しくなります。 私たちは、デジタルとアナログのブロック間の期待されるインタフェースの仕様に基づいて、容易にアサーションのセットを作成できます。

 

フォーマルを用いて、仕様が正しいことや、デザインが一連の変更に直面しても仕様の正しさが維持されることを完全に証明するために、私たちは"接続アサーション"のセットを使用します。以下に例を挙げます。

 

conn_check: assert property

(dblock.dsubblock.signal_1 == ablock1.signal_1);

 

アナログモジュール、デジタルモジュールのインタフェースや、デジタルモジュールの階層構造中に、信号が存在することに注意してください。フォーマルの利点は、この例に明確に示されているように、これらのタイプのアサーションをすぐに検証できることです。例えば、1,000個の接続アサーションがあるミックスドシグナルチップに対して、これらすべてのアサーションの証明は数分間で完了します。 誤りが見つかると、設計チームと検証チームがすぐに誤りの根本的原因をデバッグできるように、反例の波形（トレース）が自動的に作成されます。

 

代替手段としてフォーマル検証を検討してください。ブロック間の接続の仕様があれば、チェックするためのアサーションの生成を自動化できます。そしてフォーマル検証を使ってそれらを完全証明し、それらがフェイルするなら強力なデバッグ機能でデバッグを行います。ダイレクトテストは不要です。また、誤りの根本的原因を見つけるための複雑で時間が掛かるデバッグサイクルもありません。これは労力と時間を節約し、生産性の改善をもたらします。

 

パッドリング検証

SoCインテグレーションにおいて、サブシステムやブロック間のピンの接続には、パッドリングのコンフィギュレーションを含んでいます。チップのコンフィギュレーションが増えるのに従って、リングはしばしば変更されます。各コンフィギュレーションで意図している接続を把握し、パッドリング検証にフォーマル技術を利用することによって、新しいコンフィギュレーションを容易に加えることができます。フォーマル検証が可能性のあるすべての組合せを完全に探索しますので、シミュレーションではその特定が難しいような、接続が存在すべきでないコーナーケースを特定できます。

 

現在SoCデザインで一般的なJTAG、バウンダリスキャン、およびBISTを用いても、モジュール、チップ、およびシステムを検査する柔軟性が良くなったとは決して言えません。 JTAG TAP コントローラやバウンダリスキャン・レジスタなどのロジックをSoCに加えることによって、組込みシステム上でポストシリコン内のテストを実行できます。


jasper02.jpg図 2. パッドリングの例

図2では、I/Oセルのすべてが、バウンダリスキャン・レジスタチェーンを介して接続されて、TAPコントローラによって制御されます。TAPコントローラは、モジュールレベルのエンベデッドテストにアクセスするのにも使用されます。 テストの結果がステータスレジスタに書き込まれ、値を調べるのにバウンダリスキャン・レジスタチェーンが使用されます。デザインが進歩してコンフィギュレーションが変化すると、IOの信号順序、接続順序、TAPコントローラインタフェース、ブロックのテストやインタフェースが同様に変化します。

 

ここでは、ブロックレベルテストの検証と同様に、特にバウンダリスキャンの順序やTAPコントローラとのインタフェースをチェックするために記述されたアサーションを証明することによって、フォーマルが期待された接続と機能を検証します。例えば、仕様とアサーションが一旦セットアップされると、SoCの'パッドリング　アサーション'をわずか数分で証明します。これはデザインプロセスを通して、パッドリングの検証とリグレッションを行うシステマティックな手法となっています。

レジスタ検証

制御ステータスレジスタ（CSR）はハードウェアとソフトウェア間のインタフェースです。不適切に実装されたCSRは必ず下流設計の機能を壊します。そしてこの実装のバグは機能的不具合のデバッグを難しくしますので、レジスタ検証は非常に重要です。

 

フォーマル技術は、CSRの仕様を、コントロールレジスタがコンフィギュレーションされ得る状態、コントロールレジスタが安定した値を保持すべき状態、ステータスレジスタが特定の値を受け取るべき状態等を捉えるプロパティのセットに変換します。そして、フォーマル検証は、これらの状態があらゆるケースで

満たされることを検証し、他の不具合のデバッグ工程を簡素化できます。

 

通常、CSRの仕様は、リセットにおけるデフォルト値とマスクフィールドを持ったアドレス可能なレジスタセットを含んでいます。レジスタ自身は、プロトコルインタフェース経由で読み書きされます。 図3はアドレス可能なレジスタとプロトコル制御信号とのインタフェースを示しています。


jasper03.jpg図 3. CSRに対するプロトコルインタフェース

 

アドレス可能な領域でレジスタの1つを考えます。それを完全に検証するためには、レジスタが読まれる時はいつも期待値がすべての可能なシナリオの下で実際の値に合っているのを保証する必要があります。リセット後に、レジスタから読まれたデータがデフォルト値と合っているのを保証する必要があります。そして、レジスタがあるアドレスに書いた後に、読まれたデータが書かれたデータと合っているのを保証する必要があります。また、複数のリード・ライトや異なったアドレス間のリード・ライト等、すべてのコーナーケースがカバーされているのを保証する必要があります。これらのケースはプロトコルインタフェースによってすべて決められています。プロトコルインタフェースを正しいシーケンスに適切に制約することによって、無効のプロトコルによる疑似フェイルを避けることができます。もちろん、全く制約を与えないことを選択することもでき、プロトコル通りか、どうかに関わらず、全てのコーナーケースの問題について知ることができます。

 

接続チェックと同様に、それぞれのレジスタに関する仕様が必要です。アサーションは仕様単位でしばしば自動的に作成されます。そして、フォーマルは特定のデザインでこれらのアサーションを証明します。以下に例を挙げます。

 

read_reg_check : assert property

  (@(posedge clk) read_from_reg |-> (reg_dout == read_data);

 

ここで、'read_from_reg'はプロトコル（イネーブル、リード・ライト等）によって決められます。'reg_dout'は、アドレス、デフォルト値、マスクフィールドを考慮したレジスタのリファレンスモデルです。このモデルは、アサーションを証明するために実データ（read_data）と比較されます。

 

従来手法やダイレクトテストでCSRを検証するのは、退屈で、時間がかかって、不完全な場合があります。デザインに対するプロトコルがあれば、考慮すべき無数のシナリオや順序があります。フォーマルによる網羅的な解析がこれをカバーして、設計チームや検証チームによって考えられなかったコーナーケースを見つけることができます。

 

これら特定のタイプのチェックにフォーマルを適用することによって、CSR論理の完全性が確かめられ、下流設計での論理における誤りが、CSRの誤りで引き起こされることは無くなります。これはデザインのプロトコルコンプライアンスの完全性とアドレス可能なレジスタ論理の完全性において、より高い信用をもたらします。フォーマルは従来手法に比べて、より早く、より完全にこれを実行します。例えば、チップレベルのデザインにおいて数百のCSRをフォーマルで検証するのは、ダイレクトテストや特定のテストベクターの生成に時間を使うことなく、わずか数時間で済ませられます。デザインと仕様が変更されると、その仕様変更を反映させるためにアサーションが自動的に再生成され、完全性を確認するためのリグレッションテストで証明が再実行されます。

マルチサイクルパス (MCP) の検証

論理の実装や静的タイミング解析において、RTLデザイナーは、特定のパスに対してより多くのサイクルを許容するために、マルチサイクルパスを指定できます。このようなコマンドにおける誤りが、シリコン上のタイミング問題や場合によっては機能バグを引き起こすことがあります。波形生成によるフォーマル技術によって、ユーザは指定したマルチサイクルパスに沿って動作を理解して、マルチサイクルパスに対して指定したサイクル領域が正しいことを検証できます。

 

フォーマルを使って、"マルチサイクルパス アサーション"を生成するためにstandard design constraints (SDC)ファイルを使用できます。これらのアサーションはデザインに対して証明されます。パスした証明はMCPの制約を有効にしますが、フェイルはMCPがなぜ有効でないかを示す反例の波形（トレース）を発生させます。


jasper04.jpg図 4. マルチサイクルパスと SDC Constraint

図4を参照してください。"regA" から "regB" へのタイミングパスは、2サイクルかかります。したがって、合成とタイミングツールはSDCを読み込んで、このパスをそのようにアノテートするでしょう。制約が有効であることを証明するために、アサーションに変換されて証明されます。

 

%assert -mcp -cycles 2 -from regA -to regB

 

「不正な」マルチサイクルパスの制約を考えてみます。それは合成とタイミング、および機能的なバグにおいて、潜在的にタイミング問題を引き起こす場合があります。これは論理合成と場合によってはレイアウトの更なるイタレーションになる可能性があります。フォーマル検証を用いてマルチサイクルパス制約の完全性を確認することによって、コストがかかるイタレーションを避けることができます。

まとめ

SoCインテグレーションには、検証に対する多くの課題があります。設計チームと検証チームが従来手法で取り組めば、これらの挑戦は難しく、時間がかかり、退屈なものになります。現在はるかに大きな規模が扱う事が出来、より高い抽象レベルで期待される動作を定義出来るフォーマル検証手法であれば、高速、正確で、徹底的なソリューションを提供します。

 

2009年の調査では、チップインテグレーションに関して、非常に多くの回答者がマルチサイクルパス生成とチップレベルの接続検証にフォーマルの大きな利用価値を見いだしたことを示しました。自動化されたパッドリング検証が、後に続いています。


jasper05.jpg図 5.  Jasper Design Automationによる調査結果

 

チップレベルの接続検証、コンフィギュレーションの変更に対応したパッドリング検証、CSRの検証、マルチサイクルパス制約の検証等、フォーマル検証はSoCインテグレーションにおいて、設計チームと検証チームに対し、注目すべきソリューションを提供します。

 

SoCインテグレーションにおけるフォーマル検証に対するROIは明確です。ダイレクトテストを作成し、特定のシミュレーションテストを書き、難しいバグを探してシミュレーションベースのデータをデバッグするのに費やされるリソースは、フォーマル検証を用いて価値の高い領域の特定の検証タスクを実行することで節約されます。チップレベルの接続検証、パッドリング検証、レジスタ検証、およびマルチサイクルパス制約をフォーマル検証することで、複数の技術者の時間と労力を節約し、これらの検証を数時間あるいはほんの数分で実行することが期待できます。これらのテストの完全性をフォーマルで証明することで、従来手法でおそらく見つけられていないバグを見つけるだけでなく、それらのバグをより早く、時間と労力を省いて見つけられます。 

 

 

ジャスパー社について
Jasper Design Automation, Inc.は、最新のフォーマル技術をベースに、半導体の設計、検証、デザインの再利用に向け、
業界をリードするEDAソフトウェアのソリューションを提供しています。カスタマーは、ワイヤレス、コンシューマ、
コンピューティング、ネットワークなどの分野で世界をリードするトップ企業で、200を超えるチップ開発で成功して
います。ジャスパー社の本社は、米国カリフォルニア州マウンテ ンビューにあり、他に北米、南米、ヨーロッパ、
日本 に支社や代理店があります。
開発のリスクを減らし、設計、検証、再利用などの生産性を引き上げ、Time to Marketを加速し、ターゲットとする
ROIを得るため、是非ジャスパー社のホームページ　http://www.jasper-da.com/  をご覧下さい。

 

 

問合せ先

ＣｙｂｅｒＴｅｃ株式会社 

神奈川県横浜市都筑区茅ヶ崎中央50番17号　CM　Port5階

TEL: 045-945-3690　FAX: 045-945-3680

URL: http://www.cyber-tec.co.jp/

 

 

# # #

Antonio Dimalanta, Sr. Staff Field Applicatons Engineer, Jasper Design Automation, has over 19 years of experience in ASIC design, logical implementation, applications engineering, and physical implementation. Prior to joining Jasper Design Automation, Antonio was Director of Engineering at Symmid Semiconductor Technology, a Design Services company, and Staff Application Consultant with Synopsys supporting formal verification, physical design, and logical and behavioral synthesis. At Caspian Networks, he was responsible for physical implementation of several multi-million gate network processors in IBM ASIC. Earlier, as a design engineer with National Semiconductor's ASIC Division, he designed SONET/ATM chipsets. Antonio earned a BSEE from San Jose University in 1991.

Sebastian Skalberg, Field Applications Engineer Manager, Jasper Design Automation, has worked in the area of formal verification for over 10 years and has extensive experience in applying formal methods to a variety of hardware designs, including routers, controllers, and super scalar processors. As a FAE Manager, he is responsible for coordinating both pre- and post-sales support of Jasper's product line. Prior to joining Jasper, Sebastian was at OneSpin Solutions, where he was part of the Advanced Methodology team. Sebastian received both his Master's degree and doctorate degree in mathematical logic from the University of Copenhagen, Denmark.