OneSpin のデータシート、記事、ホワイトペーパー
OneSpin のデータシート
- 360 MV製品ファミリー（クリックしてデータシートをダウンロード)
最も包括的なフォーマルABV（アサーションベース検証）ソリューション - 360 Equivalence Checker – FPGA （クリックしてデータシートをダウンロード)
合成により最適化された先端FPGAのためのフォーマル検証ソリューション - 360 Equivalence Checker – ASIC（クリックしてデータシートをダウンロード)
高精度ASIC等価チェックのためのフォーマル検証ソリューション - 成功事例（クリックして成功事例をダウンロード)
360 MV ユーザー事例
ホワイトペーパー
- Capturing Timing Diagrams in Operational SVA （ダウンロードご希望の方はタイトル名をクリックし登録ページよりお申し込みください）
Timing diagrams provide an excellent, intuitive starting point for writing assertions to capture the intended behavior of designs. However, the standard assertion languages SVA and PSL do not provide direct constructs for capturing timing diagrams. This white paper presents Operational SVA – a simple yet powerful SVA library – which allows to develop assertions directly from timing diagrams and waveforms. - Achieving 100 % Functional Coverage by Operational Assertion-Based Verification（ダウンロードご希望の方はタイトル名をクリックし登録ページよりお申し込みください）
This white paper presents Operational Assertion-Based Verification (ABV), an advanced formal verification methodology resulting in a predictable, small number of high-level assertions capturing the functionality of a design. Operational ABV enables an automatic formal coverage analysis, which identifies holes in verification plans, unverified design functionality as well as errors and omissions in specifications. The formal coverage analysis ensures that 100 % of the design functionality is verified – answering the question 'Have I written enough assertions?'. - Formal Analysis of X Propagation（ダウンロードご希望の方はタイトル名をクリックし登録ページよりお申し込みください）
Verifying the absence of undefined signal values in a design is in general a hard problem. Formal 4-state logic analysis offers a powerful solution. This white paper discusses X-related verification issues, and how advanced 4-state formal analysis solves them.
360 MV製品ファミリーについてのオンライン記事
【EDSF 2009】「徐々に馴染めるように」，独OneSpinがフォーマル検証製品の体系を見直し 日経BP Tech-On独OneSpin、フォーマル検証ツール「360 MV」製品ファミリーを拡張 EDA Express
OneSpin offers step-by-step formal verification suite by Richard Goering
OneSpin automates formal assertion/RTL debug by Bill Murray
OneSpin brings formal assertion-based verification (ABV) to the masses by Max Maxfield
360 MV についてのその他のオンライン記事
Timing Diagrams Ease Formal Property Development by iDESIGNFormal Verification Goes Mainstream by Mike Donlin
フォーマル検証についての記事
過去数年間、ダイナミック検証を補完するためのフォーマル検証の使用が目に見えて拡大しています。何故でしょうか？ フォーマル検証を使用する16社に対してユーザー調査が行われています。Mixing Formal and Dynamic Verification
Formal methods: Rocket science or mainstream technology? A deeper look published in SCDsource
Formal property checking – what the users say by Richard Goering
Formal property checking – what the vendors say by Richard Goering
Formal verification expands its use model by Bill Murray
360 MV に関連した技術的記事
自動化されたフォーマル手法による高度にコンフィギュラブルなHW/SWインターフェイスの検証(SCDsource 記事)Alcatel-LucentのJoachim Knablein氏とHans Sahm氏が自動化されたアサーション生成と自動化されたフォーマル手法を 使って大規模なSDH/SONETチップの複雑なHW/SWインターフェイスを検証し、検証工数を70%短縮した方法を解説します。
Automated formal method verifies highly-configurable HW/SW interface
TriCore2 および他のプロセッサの完全なフォーマル検証（ホワイトペーパー）
DVCon 2007で発表されたこの論文は、OneSpinの360 MVをInfineonの安全性が重視される組み込みアプリケーション向け次世代ハイエンド プロセッサであるTriCore2に適用した事例を紹介しています。 他のフォーマル アプローチとは異なり、ここで採用されている手法はシミュレーションから独立してハードウェア検証を行うものです。 検証プランとプロパティ セットに含まれるすべてのギャップを体系的に消していくことで、IPに機能的エラーが含まれない、最高の品質を保証します。
TriCore2 および他のプロセッサの完全なフォーマル検証
最高のIP品質を効率的に達成（EEtimes記事） この記事では、PPv2と呼ばれるコンフィギュラブル ネットワークプロセッサをOneSpinの360MVを使って検証する事例をIPプロバイダの視点から解説しています。 この検証プロジェクトの詳細を説明するとともに、以下のような結果がどのように達成されたかについて説明します：
- あらゆるコンフィギュレーションに対してPPv2全体でエラーのない機能動作を達成
- 達成されたIP品質を証明し、迅速なIP品質評価を可能にする検証レポート
- IPに対する統合条件の完全な記述
- 仕様の大幅な改善
- IPにはリリース以来改版、再設計の必要が生じていない
- 開発工数4人月を達成 - をそれまでのシミュレーション ベースのプロジェクトと比較して約40%削減
IP 機能検証で完全性を達成 (EEtimes 記事)
360 MV は、完全性を実現した唯一の機能検証ソリューションです。 検証が客観的に「完全」であると言えるのは、DUV（Design Under Verification）の出力信号がすべての時点であらゆる可能性のある入力シナリオに対して意図された値を持つことが確認されたときです。 この完全性の概念は入力シナリオに対する 100% のカバレッジ、出力動作に対する 100% のカバレッジを意味するものであり、機能検証が達成可能な最高のカバレッジであり、エラーのない動作を保証する上で重要な意味を持ちます。 これは、フォーマル検証を通常のバグ探しとコーナーケース探査アプローチから、完全な「機能サインオフ」アプローチへと転換することではじめて可能になります。 この、完全な機能検証のためのアプローチと、他の検証アプローチ −シミュレーション ベース、アサーション ベース、フォーマルを含む − の比較については、EETimes に掲載された以下の記事で説明しています：
EETimes 記事: Achieving Completeness in IP Functional Verification