PSL for Assertions-Based Verification

Disponible désormais en deux demi-journées.

Si vous concevez ou vérifiez en VHDL sans utiliser le PSL, il y a un grand trou dans votre raquette !

Notre formation Assertion-Based Verification with PSL est très courte et efficace et ses bénéfices sont immédiats et spectaculaires !

Plus d’excuse ! Les assertions sont désormais supportées par les simulateurs QuestaSim Intel Edition et QuestaSim Microchip Edition qui accompagnent Quartus et Libero (même en version gratuite « Starter »).

  • Du lundi 6 mai 2024 au mardi 7 mai 2024 iCal
    Vérification : PSL for Assertions-Based Verification
    Formation intensive (2 x 1/2j) aux Assertions PSL.
    Lieu : à distance (OnLIne)

Présentation

Si vous êtes resté fidèle au langage VHDL, il vous faut d’urgence maîtriser le langage PSL qui en fait désormais partie ! Le PSL a été standardisé en 2005 (IEEE std 1850) et adopté par l’industrie très longtemps avant. Depuis bien des années, nous recommandons d’adopter l’usage des Assertions de Vérification dans le flot normal de conception pour tous types de projets, sans exception. L’investissement est faible (training court) et les bénéfices rapides et spectaculaires.
D’autant plus que les simulateurs qui accompagne Intel Quartus et Microchip Libero supportent désormais les assertions (PSL et SVA) !

Des livres entiers sont consacrés au sujet depuis 15 ans et démontrent les bénéfices évidents de la méthodologie de Vérification par Assertions.

Enfin, les Assertions (PSL ou SVA) sont le langage d’entrée des outils formels !

Se former, qui, pourquoi ?

On notera que PSL fait désormais partie du VHDL depuis l’édition 2008, mais nous maintenons une formation PSL indépendante car son intégration dans les formations VHDL aurait conduit à éliminer beaucoup trop de sujets importants pour laisser la place à ce langage à part entière.

Le langage en soi n’est pas excessivement complexe, mais nous avons constaté depuis longtemps que l’auto-apprentissage des Assertions (comme de la plupart des langages HDVL) conduisait pratiquement systématiquement à des échecs ou à des frustrations. Le langage cache en fait la nécessité d’adopter une méthodologie impeccable et de bien comprendre comment l’utiliser au mieux et en tirer partie dans les situations concrètes.

Les Assertions, c’est-à-dire le PSL ou son équivalent SVA en SystemVerilog, devraient impérativement être adoptées par :

  • Les Architectes
  • Les Spécifieurs
  • Les Ingénieurs de Conception
  • Les Ingénieurs de Vérification

Les bénéfices

L’utilisation des Assertions :

  • Améliorent la Qualité du code,
  • Font gagner du temps,
  • Réduisent les efforts de vérification,
  • Raccourcissent les cycles de développement et de vérification,
  • Assurent des bénéfices croissants au cours du temps !

Ce n’est pas un vœu pieu : c’est le constat d’une utilisation par les industriels depuis plus de 20 ans.

Contenu résumé

  • Les Propriétés (Properties) et le Langage PSL dans le processus de développement et de vérification.
  • Le rôle des propriétés dans le test dirigé, le random contraint, et la vérification statique formelle.
  • Savoir tirer le meilleur parti des Propriétés dans les flots de conception et de vérification.
  • Syntaxe et sémantique du langage PSL avec ses différentes couches (layers Booléen, Temporel…)
  • Comment écrire des propriétés efficaces et sûres, et savoir éviter les pièges classiques.
  • Utiliser PSL avec le simulateur HDL de votre choix, ou des outils formels.
  • PSL pour Mesurer la Couverture Fonctionnelle
  • Méthodologie pour la conception et l’utilisation des Assertions PSL
  • Utiliser PSL avec des System On Chips et bus AMBA.

Pré-requis

La compréhension préalable du langage VHDL est indispensable, de même que la pratique de la conception FPGA et de l’utilisation d’un simulateur.

Supports de cours

Nous sommes partis des manuels de cours Doulos d’origine, que nous avons réorganisés, améliorés et optimisés pour le format actuel en deux 1/2 journées.

Sont compris dans la formation :

  • Le Manuel du cours théorique complet, avec un Index. Il constitue un Manuel de Référence complet.
  • Le Cahier des Exercices pratiques qui permet de mettre en œuvre les connaissances théoriques.
  • Les fichiers des exercices et solutions.
  • Sous réserve de disponibilité : le « Doulos Golden Reference Guide », aide-mémoire PSL complet et pratique (syntaxe, sémantique et astuces).

Documents à télécharger

Revenir en haut