Horus

Vérification de propriétés pour systèmes embarqués

Introduction

Des applications grand public -transport, multimédia, télécom- aux applications critiques -aérospatial, aéronautique-, les systèmes embarqués intègrent un nombre sans cesse croissant de fonctionnalités. Garantir les performances de ces systèmes -temps réel, sûreté/sécurité, consommation, etc.- nécessite des vérifications complexes à chaque étape de développement des phases initiales du flot de conception jusqu'au prototypage matériel.

Bénéfices

L'environnement HORUS doté d'une interface ergonomique, vous permettra de gagner un temps considérable dans les différentes phases du flot de conception, grâce à la vérification automatique des performances de votre système.

  • Facilité et rapidité de mise en oeuvre
  • Spécifications exprimées dans un langage normalisé
  • Méthode de construction prouvée formellement

 

Offre

Au niveau RTL :

  • simulation avec les outils standard
  • simulation accélérée par émulation FGPA
  • surveillance en ligne des circuits critiques
  • extension en cours à la construction de moniteurs asynchrones (vérification de systèmes multi-horloges)

 

Au niveau TLM :

  • vérification dynamique de descriptions System C TLM avec ou sans temps
  • expression de propriétés élaborées (sur plusieurs canaux de communication et/ou signaux)
  • expression de contraintes sur les paramètres des fonctions de communication
  • performance (faible pénalisation sur le temps de simulation)

 

Technologie

L'environnement HORUS utilise la méthodologie de vérification d'assertions logico-temporelles (ABV, Assertion-Based Verification). A partir d'assertions écrites dans un langage standard IEEE 1850 PSL, il permet de générer automatiquement :

Au niveau RTL : des descriptions VHDL ou Vérilog synthétisables

  • de moniteurs de surveillance synchrones ou asynchrones pour la vérification des fonctionnalités à garantir par le système (assert)
  • de générateurs de séquences de test satisfaisant des contraintes temporelles sur ses entrées (assume)


Au niveau TLM (transactionnel) :
des descriptions System C TLM de moniteurs de surveillance pour la vérification de propriétés logico-temporelles sur les communications

Horus

Domaines d'application

  • Applications multimedia
  • Télécommunications
  • Avionique ou spatial
  • Automobile
  • Bâtiment


Contactez-nous