Assertion-checker synthesis for hardware verification, in-circuit debugging and on-line monitoring

• Main Author: Boulé, Marc
• Other Authors: Zeljko Zilic (Internal/Supervisor)
• Format: Others
• Language: en
• Published: McGill University 2008
• Subjects: Engineering - Electronics and Electrical
• Online Access: http://digitool.Library.McGill.CA:80/R/?func=dbin-jump-full&object_id=18754

Producing error-free circuits is of paramount importance in the semiconductor industry. Assertions are becoming an indispensable means of verifying the correctness of increasingly complex digital designs. Assertions model the proper behavior of a design, and are expressed in a high level language based on temporal logic. In dynamic verification, simulation is used to exercise a circuit in order to assess its behavior. For large designs, simulation times are often prohibitively excessive, and designs are instead emulated in hardware. Because of their high-level temporal operators, assertion statements do not lend themselves directly to hardware implementations such as emulation. This thesis introduces techniques and algorithms for generating resource-efficient circuit-level checkers from hardware assertion statements. These checkers are added to the source design, where they monitor the appropriate circuit signals to find faulty execution sequences. In this work, a finite automaton framework and a set of algorithms are developed and used extensively to create an intermediate representation of assertions. Implementing the large variety of temporal operators found in properties is also performed using specially designed rewrite rules. Checkers are circuit-level implementations of assertions, and thus allow assertions to be used in hardware emulation and simulation acceleration. The checkers are not only beneficial in pre-fabrication functional verification, but can also be used for debugging fabricated silicon, at speed, where timing issues are most prevalent. Using checkers beyond verification and silicon debug is also explored, by proposing the use of assertions and a checker generator to automate the design of certain types of circuits. A variety of enhancements are also introduced to improve the debugging process with assertion checkers. These enhancements range from additional observability and metric-reporting features, to behavioral modifications to the che === La production de circuits exempts d'erreurs est d'une importance capitale dans le domaine des semiconducteurs. Avec l'augmentation constante de la complexité des circuits numériques, la vérification matérielle basée sur les assertions devient indispensable. Les assertions modélisent le bon fonctionnement d'un circuit, et sont spécifiées à l'aide d'un langage faisant appel à la logique temporelle. En vérification dynamique, la simulation est utilisée afin d'analyser le comportement d'un circuit. Cependant, les temps de simulation deviennent trop longs pour de gros circuits et par conséquent, ces derniers sont souvent émulés de façon matérielle. Étant donné la présence d'opérateurs de logique temporelle de haut niveau, les assertions ne sont pas directement implantables de façon matérielle. Cette thèse présente les méthodes et les algorithmes nécessaires pour générer des circuits vérificateurs efficaces à partir des assertions. Ces vérificateurs se branchent au circuit à tester afin d'y observer les signaux, permettant ainsi de déceler un mauvais fonctionnement. Dans cet ouvrage, une série d'algorithmes ainsi qu'un modèle basé sur les automates finis sont développés et utilisés comme représentation intermédiaire pour les assertions. L'implémentation du vaste éventail d'opérateurs se fait aussi grâce à des règles de réécriture. En créant des circuits vérificateurs, les assertions peuvent dès lors être utilisés dans l'émulation matérielle et les accélérateurs de simulation. Les vérificateurs sont déjà fort utiles lors de la vérification préfabrication. Ces circuits peuvent aussi être utilisés lors de la vérification de circuits manufacturés où les problèmes de cadençage sont les plus réalistes. L'utilisation des vérificateurs est aussi applicable au-delà de la vérification et du déverminage post-fabrication, et peut servir pour la conception de circuits de haut niveau. Un ensemble d'extensi