命令セットアーキテクチャ(ISA)に対するギャップや不整合のない迅速かつ網羅的な検証および準拠の証明
RISC-VはIP、EDA、ソフトウェアサプライヤに幅広く支持されているオープンソースのハードウェア命令セットアーキテクチャ(ISA)です。RISC-V IPコアプロバイダは、公開されているISAに対する検証とコンプライアンスという高いハードルに直面します。これらの課題をクリアすることは、多数のシリコン実装実績やデザインイン実績を持つ古い十分に確立されたISAとの競争を勝ち抜くためにはきわめて重要です。さらに、コアプロバイダは設計が[1][2]信頼性[3][4] と [5][6]セキュリティ[3][4] についての顧客の期待を満足するものであることを保証しなければなりません。これにはハードウェアトロイやその他攻撃者に利用される恐れのある意図しない機能が存在しないことも重要です。[9]
OneSpin RISC-V Integrity Verification Solution は、コアプロバイダとコアインテグレータ両方のニーズに対応した業界初の商用ツールスイートです。車載向けその他の高信頼性プロセッサアプリケーション分野で使用されているOneSpinの高度なフォーマル検証技術を使って、最小限のセットアップおよび処理時間でインプリメンテーションを網羅的に検証することができます。ソリューションの中核にあるのは、RISC-V ISAをOneSpin独自のOperational Assertionアプローチを使って一連のSystemVerilog Assertions(SVA)として形式化したものです。Operational SVAにより、エンドツーエンドのトランザクションおよび要件を簡潔かつ洗練された方法で表した、ハイレベルの、重複の無いアサーションが実現されています:
- 機能要件をフォーマルかつシミュレーション実行可能形式に変換
- 回路トランザクション全体をタイミングダイアグラムのような簡潔かつ洗練された表現に
- ハイレベルでレビューしやすいアサーションにより100%の機能カバレッジを達成
- 幅広いアプリケーションに適用可能であり、シミュレータにもフォーマルツールにも最適なパフォーマンスを提供する一貫したアサーションスタイルを採用
- インプリメンテーション固有の検証コードと再利用可能な仕様レベルのコードを明確に分離
- OneSpin の GapFreeVerification™ を使ってアサーションセットをさらに活用し、仕様の漏れやエラー、検証プランの穴、未検証のRTLファンクションなどを自動的に検知
このメソドロジはRISC-V ISAの主要なルールを表現するのに理想的です。個々のオペレーションは1つのOperational Assertionとして記述されます。これらのアサーションはハイレベルのオペレーションを表し、シーケンシャルまたはパイプライン型インプリメンテーション、アウトオブオーダー実行、およびその他RTLコアで可能なオプションにマッピングされます。RISC-V Integrity Verification Solution には、Privileged ISA、Control and Status Registers(CSRs)、例外メカニズム、その他の拡張が含まれています。検証フレームワークは仕様サイドをマッピングから分離し、完全なSVA再利用が可能です。ターゲットインプリメンテーションへのマッピングは、OneSpinが提供するガイド手順に沿って簡単に行えます。
OneSpinのフォーマルエンジンは、RTLコアインプリメンテーションとアサーションで表現されたISAの間のあらゆる不整合を検知します。 GapFreeVerification™ を適用する効果は、RTLとOperational SVAセットの間の等価性を証明することだけではありません。 アサーションのセットがRISC-V コアのデザインをカバーするのに十分であるかどうかを検証し、また検証されていないRTL機能がないことも確認することもできます。ハードウェアトロイのような余計な機能がデザインに含まれていれば検知され、ISA の違反として報告されます。 この機能には、隠れた命令や、命令の意図しない副効果の体系的な発見も含まれます。 これにより、コアプロバイダと顧客のどちらも、RISC-Vインプリメンテーションの[1][2]信頼性[3][4] と[5][6]セキュリティ[3][4] に最大限の自信を持つことができます。
OneSpinのRISC-V Integrity Verification Solutionは、IPコアインプリメンテーションがするべきことをすべて行い、するべきでないことをまったく行わないことを保証するものです。これにより、システムオンチップ(SoC)設計者は RISC-V コアが ISA仕様に準拠していることに自信を持ってライセンスできます。また IP ベンダーは自社独自のエコシステムをサポートしながら、エコシステム利用者も正しく準拠させることができます。 さらに、SoC設計者は RISC-V ISA にカスタム機能を追加して特定のアプリケーションをサポートすることもできます。OneSpin の RISC-V Integrity Verification Solution は、機能を追加しても何も壊れないことを保証し、また新しい機能を検証するのにも十分な柔軟性を備えています。
OneSpin の RISC-V 関連コンテンツを是非ご確認ください
- RISC-V Verification Q & A
»Check out the Videos - Formal Verification of RISC-V Cores
»Watch the Video - RISC-V Summit 2019 Videos
»Watch the Videos - “A Holistic View Of RISC-V Verification”
by Nicolae Tusinschi, Semiconductor Engineering, 7 August 2019
»https://semiengineering.com/a-holistic-view-of-risc-v-verification/ - “Assuring the Integrity of RISC-V Cores and SoCs”
white paper, OneSpin Solutions, July 2019
»Download White Paper - “Enabling The RISC-V Ecosystem”
by Nicolae Tusinschi, Semiconductor Engineering, 27 June 2019
»https://semiengineering.com/enabling-the-risc-v-ecosystem/ - “Lösung zum Sicherstellen der Integrität von RISC-V-Kernen”
by Sven Beyer and Tom Anderson, Elektronik Industrie, 19 June 2019
»https://www.all-electronics.de/loesung-zum-sicherstellen-der-integritaet-von-risc-v-kernen/ - “Formalizing the RISC-V ISA in a set of SystemVerilog assertions that can be proven
to be complete, consistent, and free from gaps”
by Sergio Marchese, Verification Futures, 13 June 2019
»https://www.testandverification.com/conferences/verification-futures/vf2019/ - “Formal Verification of PULPino and other RISC-V SoCs”
by Nicolae Tusinschi and Sven Beyer, RISC-V Workshop Zurich, 12 June 2019
»Download pdf - “Unbounded Formal Verification of RISC-V CSRs with Interval Property Checking”
by Nicolae Tusinschi and Sven Beyer, RISC-V Workshop, Zurich, 11 June 2019 - “Unbounded Formal Verification of RISC‑V CSRs with Interval Property Checking”
by Nicolae Tusinschi and Sven Beyer, Design Automation Conference (DAC), Las Vegas, 2 June 2019 - “Verification Challenges for RISC-V Adoption”
by Tom Anderson, GSA Forum, 2 May 2019
»https://www.gsaglobal.org/forums/1386/verification-challenges-for-risc-v-adoption/ - “In the middle of every difficulty lies opportunity.” – Albert Einstein
- “Complete Formal Verification of RISC-V Processor IPs for Trojan-Free Trusted ICs”
by Paul McHale (Edaptive) and David Landoll, GOMACTech Conference, Albuquerque, 28 March 2019 - “Ensure Compliance and Trust for RISC-V Cores and SoCs with Complete Formal Verification”
by Sasa Stamenkovic, Verification 3.0 Innovation Summit, Santa Clara, 19 March 2019
»https://www.youtube.com/watch?v=bC2-11q9QS4 - "Unbounded Formal Verification of RISC-V CSRs with Interval Property Checking”
by Nicolae Tusinschi, RISC-V Workshop, Taiwan, 12 March 2019
»Download pdf - “Formal Verification Of RISC-V Cores”
by Sven Beyer, Semiconductor Engineering, 28 February 2019
»https://semiengineering.com/formal-verification-of-risc-v-cores/
More information…
the RISC-V Verification App is the industry’s first tool to address the needs of both core providers and core integrators. It leverages OneSpin’s advanced formal verification expertise for high-integrity processor applications.
»Download the data sheet…OneSpin’s Operational SVA enables formal verification enthusiasts to develop high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way.
»Learn more…The OneSpin 360 Design Verification (DV) product line leverages the most advanced, high-performance formal technology as the basis for a range of verification solutions, from automated design analysis to advanced property checking.
»Download the flyer…OneSpin’s Quantify measures the quality of a formal verification test bench. It provides precise, actionable information on what parts of the design-under-test (DUT) are verified, and it highlights RTL code that could still hide bugs.
»Download the data sheet…OneSpin’s Connectivity XL App is the industry’s first and only solution for the efficient specification and formal verification of huge numbers of deep connections in multi-billion-gate chips.
»Download the data sheet…OneSpin’s VCI App enables users to export structural coverage results produced by OneSpin’s QuantifyTM in different database formats with a single command.
»Download the data sheet…OneSpin 360 DV-Verify adds coverage-driven assertion-based verification (ABV) to the DVInspect platform.
»Download the data sheet…In a systematic verification flow, requirements tracking and coverage play an indispensable role. Generally, this starts from requirements specification, where individual requirements are broken down into features, implementations, verification goals, and metrics.
»Download the data sheet…Design verification has a lot in common with human hygiene practices. The goal of both activities is to remove all dirt, grime, and bugs through an active process of establishing good hygiene.
»Download the white paper…Fault-tolerant hardware development is no longer a niche and presents new challenges. Many engineers face the daunting task of having to examine countless faulty variants of their design in order to integrate and verify multiple safety mechanisms within complex Systems-on-Chip (SoCs).
»Download the white paper…Get in touch!
Learn more about RISC-V verification with OneSpin!
Sven Beyer, Product Manager Design Verification