La firme allemande OneSpin Solutions, spécialiste des outils de vérification formelle des fichiers de conception de circuits intégrés ou des blocs de propriété intellectuelle (IP), élargit ses technologies à la communauté des développeurs de processeurs et puces-systèmes fondés sur le jeu d’instructions open source RISC-V.... Dévoilée en début d'année lors de la manifestation DesignCon, la solution de vérification pour le développement et l'évaluation des cœurs RISC-V de OneSpin s’appuie sur la formalisation du jeu d’instructions RISC-V dans un ensemble d’assertions écrites en langage SystemVerilog (SVA), et sur une application d’analyse formelle intégrée à un ensemble plus vaste de vérification du code RTL d’un circuit utilisant un coeur RISC-V (l’environnement 360 MV).

Cette approche assure notamment la conformité au standard ouvert RISC-V ISA sur la base de preuves formelles, un atout qui s'avère essentiel pour les fournisseurs de blocs d’IP et un objectif qui n’est pas atteignable en utilisant des outils classiques de simulation.

En parallèle, la solution OneSpin vérifie sans ambiguïté, via des assertions formelles, que les cœurs RISC-V ne contiennent pas de bogues matériels (avec la découverte systématique de toutes les instructions cachées ou l'analyse des effets induits non désirés de certaines instructions). Elle garantit en outre l'absence d'erreurs fonctionnelles et contribue à l’élimination des vulnérabilités de sécurité afin d’instiller de la confiance dans les conceptions. Ainsi, à travers cette solution, les concepteurs de puces-systèmes SoC peuvent attribuer une licence à un cœur de RISC-V en s’assurant qu’il se conforme à la spécification ISA, tandis que les fournisseurs d’IP peuvent prendre en charge leurs propres écosystèmes et vérifier que leurs partenaires respectent également cette exigence.

Par ailleurs, les concepteurs de SoC peuvent ajouter des fonctionnalités personnalisées au jeu d'instructions RISC-V pour prendre en charge leurs applications spécifiques exemptes de bogues, en s’appuyant sur les vérifications apportées par la solution de OneSpin.

Concrètement, l’outil de vérification d'intégrité des fichiers RISC-V inclut des registres de contrôle et d'état (CSR) et sépare clairement les parties vérification et spécification, du mapping jusqu’à l’implantation finale du code, afin de réutiliser les suites d’instructions SVA, tout au long du cycle de conception.

Vous pouvez aussi suivre nos actualités sur la vitrine LinkedIN de L'Embarqué consacrée à l’architecture de processeur RISC-V : Embedded-RISCV https://www.linkedin.com/showcase/embedded-riscv/