en fr Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level Techniques et outils pour la vérification de Systèmes-sur-Puce au niveau transaction Report as inadecuate




en fr Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level Techniques et outils pour la vérification de Systèmes-sur-Puce au niveau transaction - Download this document for free, or read online. Document in PDF available to download.

1 VERIMAG - IMAG - VERIMAG

Abstract : The work presented in this document deals with the formalverification models of Systems-on-a-Chip at the transaction levelTLM. We present the transaction level and its variants, and remindhow this new level of abstraction is today necessary in addition tothe register transfer level RTL to accommodate the growingconstraints of productivity and quality, and how it integrates inthe design flow.We present a new tool, called \lussy, that allows property-checkingon transactional models written in SystemC. Its structure is similarto the one of a compiler: A front-end, Pinapa, that reads thesource program, a semantic extractor, bise, into our intermediateformalism HPIOM, a number of optimizations in the component \birth,and code generators for provers like Lustre and SMV.Lussy has been designed to have as few limitation as possibleregarding the way the input program is written. \pinapa uses a novelapproach to extract the information from the SystemC program, andthe semantic extraction implements several TLM constructs that havenot been implemented in any other SystemC verification tool as ofnow. It doesn-t require any manual annotation. The tool chain iscompletely automated.Lussy is currently able to prove properties on small platforms. Itscomponents are reusable to build compositional verification tools,or static code analyzers using techniques other than model-checkingthat can scale up more efficiently.We present the theoretical principles for each step of thetransformation, as well as our implementation. The results are givenfor small examples, and for a medium size case-study called EASY.Experimenting with Lussy allowed us to compare the various tools weused as provers, and to evaluate the effects of the optimizations weimplemented.

Résumé : Les travaux présentés dans ce document portent sur la vérificationde modèles de systèmes sur puce, au niveau transactionnel TLM.Nous présentons le niveau transactionnel et ses variantes, etrappelons en quoi ce nouveau niveau d-abstraction est aujourd-huinécessaire en plus du niveau de transfert de registre RTL pourrépondre aux contraintes de productivités et de qualités de plus enplus fortes, et comment il s-intègre dans le flot de conception.Nous présentons un nouvel outil, LusSy, permettant la vérificationformelle de modèles transactionnels écrits en SystemC. Sa structureinterne s-apparente à celle d-un compilateur: Une partie frontale,Pinapa, qui lit le programme source, une extraction de lasémantique, Bise, dans notre formalisme intermédiaire \hpiom, unesérie d-optimisations dans le composant Birth, et des générateursde code pour les outils de preuves pour Lustre et SMV.Lussy est conçu et écrit de manière à avoir aussi peu de limitationque possible sur la forme du code SystemC accepté en entrée. \pinapautilise une approche innovante qui lui permet de s-affranchir de laplupart des limitations dont souffrent les outils similaires.L-extraction de la sémantique implémente plusieurs constructions TLMqu-aucun autre outil disponible aujourd-hui ne gère. Il ne demandepas d-annotation manuelle du code source, toute la chaîne étantentièrement automatisée.Lussy est capable de prouver formellement des propriétés sur desmodèles de petites taille, et ses composants sont réutilisables pourdes outils de preuve compositionnelle, ou d-analyse de code autreque le model-checking qui passeront mieux à l-échelle que l-approcheactuelle.Nous présentons les principes de chaque étape de la transformation,ainsi que notre implémentation. Les résultats sont donnés pour desexemples simples et petits, et pour une étude de cas de taillemoyenne, EASY. Les expérimentations avec Lussy nous ont permis decomparer les différents outils de preuves que nous avons utilisés,et d-évaluer l-efficacité des optimisations que nous avonsimplémentées.

en fr

Keywords : System-on-a-Chip Formal verification compilation SystemC lustre smv model-checking semantics TLM

Mots-clés : Systèmes sur puce Vérification formelle sémantique





Author: Matthieu Moy -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents