The Property Specification Language (PSL) is an IEEE standard which allows developers to specify precise behavioral properties of hardware designs. PSL assertions can be embedded within code written in hardware description languages (HDL) such as Verilog to monitor signals of interest. Debugging simulations at the register transfer level (RTL) is often required to verify the functionality of a design before synthesis. Traditional methods of RTL debugging can help locate failures, but do not necessarily immediately help in discovering the reasons for the failures. The P2VSim tool presents the ability to combine multiple Verilog signals not only instantaneously, but also across multiple clock cycles, producing a graphical display of the state of active PSL assertions in a given RTL simulation. When using the P2VSim tool, users will write PSL assertions directly into their Verilog source files. After the tool searches for and loads the embedded assertions, execution trace monitors for the relevant Verilog signals are dynamically generated and written back into the Verilog source code. P2VSim then invokes an RTL simulator, Modelsim, to generate a simulation execution trace, requiring that the designer has some hardware or software testbench already in place. Next, the input PSL assertions are parsed into time intervals that have logical and temporal properties. These intervals are to be displayed graphically when PSL property checking is performed. Finally, the user is allowed to step through simulation one cycle at a time, while the tool applies the simulation execution trace to the instantiated time intervals, performing PSL property checking at each clock cycle. From this, the user can witness the exact clock cycles when PSL assertions are satisfied or violated, along with the causes of such results.

The most time-consuming component of designing and launching hardware products to market is the verification of Integrated Circuits (IC). An effective way of verifying a design can be achieved by adding assertions to the design. Automatic translation of hardware specifications from natural language to assertions in a formal representation has the potential to improve the verification productivity of ICs. However, natural language specifications have the characteristics of being imprecise, incomplete, and ambiguous. An automation framework can benefit verification engineers only if it is designed with the right balance between the ease of expression and precision of meaning allowed for in the input natural language specifications. This requirement introduces two major challenges for designing an effective translation framework. The first challenge is to allow the processing of expressive specifications with flexible word order variations and sentence structures. The second challenge is to assist users in writing unambiguous and complete specifications in the English language that can be accurately translated. In this dissertation, we address the first challenge by modeling semantic parsing of the input sentence as a game of BINGO that can capture the combinatorial nature of natural language semantics. BINGO parsing considers the context of each word in the input sentence to ensure high precision in the creation of semantic frames. We address the second challenge by designing a suggestion and feedback framework to assist users in writing clear and coherent specifications. Our feedback generates different ways of writing acceptable sentences when the input sentence is not understood. We evaluated our BINGO model on 316 hardware design specifications taken from the documents of AMBA, memory controller, and UART architectures. The results showed that highly expressive specifications could be handled in our BINGO model. It also demonstrated the ease of creating rules to generate the same semantic frame for specifications with the same meaning but different word order. We evaluated the suggestion and rewriting framework on 132 erroneous specifications taken from AMBA and memory controller architectures documents. Our system generated suggestions for all the specs. On manual inspection, we found that 87% of these suggestions were semantically closer to the intent of the input specification. Moreover, automatic contextual analysis of the rewritten form of the input specification allowed the translation of the input specification with different words and different order of words that were not defined in our grammar. / Doctor of Philosophy / The most time-consuming component of designing and launching hardware products to market is the verification of hardware circuits. An effective way of verifying a design is to add programming codes called assertions in the design. The creation of assertions can be time-consuming and error-prone due to the technical details needed to write assertions. Automatically translating assertion specifications written in English to program code can reduce design time and errors since the English language hides away the technical details required for writing assertions. However, sentences written in English language can have multiple and incomplete interpretations. It becomes difficult for machines to understand assertions written in the English language. In this work, we automatically generate assertions from assertion descriptions written in English. We propose techniques to write rules that can accurately translate English specifications to assertions. Our rules allow a user to write specifications with flexible use of word order and word interpretations. We have tested the understanding framework on English specifications taken from four different types of hardware design architectures. Since we cannot create rules to understand all possible ways of writing a specification, we have proposed a suggestion framework that can inform the user about the words and word structures acceptable to our translation framework. The suggestion framework was tested on specifications of AMBA and memory controller architectures.

Avec la complexité croissante des systèmes sur puce, le processus de vérification devient une tâche de plus en plus cruciale à tous les niveaux du cycle de conception, et monopolise une part importante du temps de développement. Dans ce contexte, l'assertion-based verification (ABV) a considérablement gagné en popularité ces dernières années. Il s'agit de spécifier le comportement attendu du système par l'intermédiaire de propriétés logico-temporelles, et de vérifier ces propriétés par des méthodes semi-formelles ou formelles. Des langages de spécification comme PSL ou SVA (standards IEEE) sont couramment utilisés pour exprimer ces propriétés. Des techniques de vérification statiques (model checking) ou dynamiques (validation en cours de simulation) peuvent être mises en œuvre. Nous nous plaçons dans le contexte de la vérification dynamique. A partir d'assertions exprimées en PSL ou SVA, des descriptions VHDL ou Verilog synthétisables de moniteurs matériels de surveillance peuvent être produites (outil Horus). Ces composants peuvent être utilisés pendant la conception (en simulation et/ou émulation pour le débug et la validation de circuits), ou comme composants embarqués, pour la surveillance du comportement de systèmes critiques. Pour l'analyse en phase de conception, que ce soit en simulation ou en émulation, le problème de la génération des séquences de test se pose. En effet, des séquences de test générées aléatoirement peuvent conduire à un faible taux de couverture des conditions d'activation des moniteurs et, de ce fait, peuvent être peu révélatrices de la satisfaction des assertions. Les méthodes de génération de séquences de test sous contraintes n'apportent pas de réelle solution car les contraintes ne peuvent pas être liées à des conditions temporelles. De nouvelles méthodes doivent être spécifiées et implémentées, c'est ce que nous nous proposons d'étudier dans cette thèse. / With the increasing complexity of SoC, the verification process becomes a task more crucial at all levels of the design cycle, and monopolize a large share of development time. In this context, the assertion-based verification (ABV) has gained considerable popularity in recent years. This is to specify the behavior of the system through logico-temporal properties and check these properties by semiformal or formal methods. Specification languages such as PSL or SVA (IEEE) are commonly used to express these properties. Static verification techniques (model checking) or dynamic (during simulation) can be implemented. We are placed in the context of dynamic verification. Our assertions are expressed in PSL or SVA, and synthesizable descriptions VHDL or Verilog hardware surveillance monitors can be produced (Horus tool). These components can be used for design (simulation and/or emulation for circuit debug and validation) or as embedded components for monitoring the behavior of critical systems. For analysis in the design phase, either in simulation or emulation, the problem of generating test sequences arises. In effect, sequences of randomly generated test can lead to a low coverage conditions of activation monitors and, therefore, may be indicative of little satisfaction assertions. The methods of generation of test sequences under constraints do not provide real solution because the constraints can not be linked to temporal conditions. New methods must be specified and implemented, this's what we propose to study in this thesis.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste. / Over the last years, the growing of electronic circuit complexity has experienced a tremendous evolution. Moreover, electronic circuits have become widespread elements in many different areas. This development leads to Systems-on-Chip incorporating a combination of components with highly heterogeneous features. Ensuring the correct behavior of each component, as well as validating the behavior of the whole system, is both a compelling and painful task. In this context, Assertion-Based Verification (ABV) has widely gained acceptance over the recent years : following this approach, temporal properties expressed using languages such as PSL or SVA specify the expected behavior of the design. While most existing ABV solutions are restricted to the register transfer level (RTL), the work of this thesis attempts to overcome some limitations by developing an actual ABV solution for the transaction level modeling (TLM) in SystemC. An effective technique for the construction of checker modules from PSL properties is proposed : this technique for SystemC TLM is inspired from a pioneering approach for RTL. A specific method for monitoring communication activities at a high level of abstraction is also described. The scope of the proposed technique is significantly improved by adding to PSL both a formal and a practical support for auxiliary global and local variables, which are compelling in higher level specifications. All these concepts are implemented in a prototype tool. In order to present the applicability of the proposed solution, we performed various experiments using designs of different sizes and complexities. The experimental results show that this dynamic verification methodology is also suitable for real-world designs.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste.

SystemC has emerged as a de facto standard modeling language for hardware and embedded systems. However, the current standard does not provide support for temporal specifications. Specifically, SystemC lacks a mechanism for sampling the state of the model at different types of temporal resolutions, for observing the internal state of modules, and for integrating monitors efficiently into the model's execution. This work presents a novel framework for specifying and efficiently monitoring temporal assertions of SystemC models that removes these restrictions. This work introduces new specification language primitives that (1) expose the inner state of the SystemC kernel in a principled way, (2) allow for very fine control over the temporal resolution, and (3) allow sampling at arbitrary locations in the user code. An efficient modular monitoring framework presented here allows the integration of monitors into the execution of the model, while at the same time incurring low overhead and allowing for easy adoption. Instrumentation of the user code is automated using Aspect-Oriented Programming techniques, thereby allowing the integration of user-code-level sample points into the monitoring framework. While most related approaches optimize the size of the monitors, this work focuses on minimizing the runtime overhead of the monitors. Different encoding configurations are identified and evaluated empirically using monitors synthesized from a large benchmark of random and pattern temporal specifications. The framework and approaches described in this dissertation allow the adoption of assertion-based verification for SystemC models written using various levels of abstraction, from system level to register-transfer level. An advantage of this work is that many existing specification languages call be adopted to use the specification primitives described here, and the framework can easily be integrated into existing implementations of SystemC.

No description available.

No description available.

This thesis describes the Omnibus language and its supporting framework of tools. Omnibus is an object-oriented language which is superficially similar to the Java programming language but uses value semantics for objects and incorporates a behavioural interface specification language. Specifications are defined in terms of a subset of the query functions of the classes for which a frame-condition logic is provided. The language is well suited to the specification of modelling types and can also be used to write implementations. An overview of the language is presented and then specific aspects such as subtleties in the frame-condition logic, the implementation of value semantics and the role of equality are discussed. The challenges of reference semantics are also discussed. The Omnibus language is supported by an integrated verification tool which provides support for three assertion-based verification approaches: run-time assertion checking, extended static checking and full formal verification. The different approaches provide different balances between rigour and ease of use. The Omnibus tool allows these approaches to be used together in different parts of the same project. Guidelines are presented in order to help users avoid conflicts when using the approaches together. The use of the integrated verification approach to meet two key requirements of safe software component reuse, to have clear descriptions and some form of certification, are discussed along with the specialised facilities provided by the Omnibus tool to manage the distribution of components. The principles of the implementation of the tool are described, focussing on the integrated static verifier module that supports both extended static checking and full formal verification through the use of an intermediate logic. The different verification approaches are used to detect and correct a range of errors in a case study carried out using the Omnibus language. The case study is of a library system where copies of books, CDs and DVDs are loaned out to members. The implementation consists of 2278 lines of Omnibus code spread over 15 classes. To allow direct comparison of the different assertion-based verification approaches considered, run-time assertion checking, extended static checking and then full formal verification are applied to the application in its entirety. This directly illustrates the different balances between error coverage and ease-of-use which the approaches offer. Finally, the verification policy system is used to allow the approaches to be used together to verify different parts of the application.

Avec l'avènement des systèmes intégrés complexes, la vérification par assertions(Assertion Based Verification ou ABV) s'est imposée comme une solution pour la vérification semi-formelle des circuits. L'ABV permet de valider qu'un circuit satisfait ou non une propriété(ou assertion). Des travaux antérieurs ont montré qu'il était possible de synthétiser ces propriétés sous la forme de moniteurs matériels. Ces derniers peuvent ainsi être embarqués à demeure sur un circuit afin qu'ils assurent une tâche de monitoring. Avec un objectif de surveillance et de sûreté, l'utilisation de tels moniteurs est un plus. Néanmoins, ces derniers sont aussi sensibles que les circuits surveillés à une dégradation environnementale(tension, température, vieillissement, …). Afin de réduire le risque de dysfonctionnement des moniteurs, initialement conçus comme des circuits synchrones, une variante asynchrone(quasi-insensible aux délais) est proposée dans cette thèse. Ces travaux s'inscrivent dans le cadre du projet ANR SFINCS(Thalès, Dolphin Integration, TIMA) et ont mené à la définition d'une méthode de synthèse de moniteurs asynchrones matériels tirant parti de la robustesse et de la modularité des implémentations asynchrones. Les études menées se focalisent en premier lieu sur la conception d'une bibliothèque de moniteurs élémentaires asynchrones et sur une méthode d'interconnexion ad hoc permettant de constituer des moniteurs complexes. Afin de garantir les bonnes propriétés de robustesse de ces moniteurs, une étude a été menée à l'aide de l'outil de vérification formelle RAT. Il a notamment été prouvé que la connexion d'un moniteur asynchrone avec un circuit synchrone(à surveiller) était un point particulièrement délicat car les hypothèses du circuit synchrone contraignent le moniteur asynchrone. Il a donc été proposé d'introduire un dispositif de contrôle de l'horloge du circuit synchrone, appelé « clock stretching », afin de relaxer les hypothèses temporelles synchrones qui sont appliquées à la partie asynchrone. / With the advent of complex integrated systems, the assertion based verification(ABV) has emerged as a solution for the semi-formal circuits verification. The ABV is used to validate that a circuit satisfies a property(or assertion). Previous work has shown that it is possible to synthesize these properties in the form of hardware monitors. These can then be embeddded permanantly on a circuit so that they provide monitoring task. With a goal of security and surveillance, the use of such monitors is a plus. Nevertheless, they are as sensitive as the monitored circuits to environmental degradation(voltage, temperature, age, ...). To reduce the risk of failure in monitors, originally designed as synchronous circuits, an asynchronous variant(quasi-delay insensitive) is proposed in this thesis. This work is part of the ANR project SFINCS(Thales, Dolphin Integration, TIMA) and led to the definition of a method for synthesizing asynchronous hardware monitors leveraging the robustness and modularity of asynchronous implementations. The studies focus primarily on the design of a library of basic asynchronous monitors and an ad hoc method of interconnection to build complex monitors. To ensure the robustness of these monitors, a study was conducted using formal verification tool RAT. In particular it was proved that the connection of an asynchronous monitor with a synchronous circuit(to watch) was particularly tricky because the timing assumptions of synchronous circuit impact the asynchronous monitor. It was therefore proposed to introduce a devicet, called "clock stretching", for controlling the clock of the synchronous circuit and relax synchronous timing assumptions that are applied to the asynchronous monitor.