The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.

In order to mitigate the ever-increasing trend in software failures with far reaching consequences, research has suggested close coordination of requirements engineering (RE) and testing. The literature also advocates the notion of requirements-based testing (RBT) focusing on checking both the quality attributes and implementation of requirements. As requirements reside in the environment comprised of certain problem domain phenomena, the environment assertions connecting some of these phenomena in the indicative mood play a critical part in determining the correctness of a software solution. Although several investigations emphasize the role of environment assertions in testing and QA activities, including RBT, current literature provides manual techniques of formulating environment assertions. Such an approach is extremely time consuming and highly dependent on an individual's domain knowledge. In addition, developers often struggle to formulate good assertions from scratch. To address this issue, in this thesis, we develop a boilerplate with certain placeholders that can be replaced with relevant attributes to formulate individual environment assertions. Leveraging this boilerplate, we further present a framework to capture environment assertions in an automated manner.

Software developers dedicate a major portion of their development effort towards testing and quality assurance (QA) activities, especially during and around the implementation phase. Nevertheless, we continue to see an alarmingly increasing trend in the cost and consequences of software failure. In an attempt to mitigate such loss and address software issues at a much earlier stage, researchers have recently emphasized on the successful coordination of requirements engineering and testing (RET). Jackson points out that requirements reside in the environment which is comprised of certain phenomena, also known as environment assertions, and a large number of software issues stem from faulty environment assertions. Current literature doesn’t provide any explicit emphasis on the environment assertions during QA activities. In order to address this gap, in this thesis, we present a detailed empirical study on the prominence of environment assertions in RBT and further propose an automated support to capture environment assertions.

Application Specific Integrated Circuits (ASIC) and Field Programmable Gate Arrays (FPGA) verification is quite a time consuming phase in design flow cycle and it can be done using methodologies such as Universal Verification Methodology (UVM) and formal verification.The UVM methodology is simulation based verification where in the verifier will have to trigger the Design Under Test (DUT) manually by writing sequences which target different features of the DUT and the verification environment can also have verification directives such as assertions to spot design bugs. Formal verification on the other hand is purely assertion based verification where we describe the expected DUT behaviour using System Verilog Assertion (SVA) and we check for design sanity by exercising the assertions by letting the formal tool drive the inputs to the design in a constrained way. This completely eliminates the need of having to define sequences to drive the inputs. This thesis will bring up formal verification using jasper gold to light and will help verifiers to decide on how much of formal verification methodology can be used in verification of an IP with respect to the complexity of the design and the design behaviour to be verified. The results from this thesis proves how efficient formal verification was with respect to simulation based verification, to stress the design to test for corner case behaviour. The reason why formal verification cannot be extended for Top-Level Verification (TLV) and end to end functional verification is because of design complexity and this was also explored with the help of a complex ethernet design. Finally, a guideline as to when to use simulation based verification and formal verification was formulated. / ASIC och FPGA verifiering är en största del och är en tidskrävande fas av desingflödescyckeln. Det kan man göra den genom UVM eller Formell verifiering metoder.UVM metoder är simulering baserad verifiering där verifieraren måste utlösa DUT genom att skriva sekvenser som rikta olika funktioner av DUT och verifiering miljöer kan också ha verifiering direktiv som assertions som kan upptäcka designbugs.Formal verifiering är en assertion baserad verifiering metoder där i man kan beskriva förväntad DUT uppträdandet genom system verilog assertions (SVA) och verifiera designen genom använder assertions genom att låta det formal driva ingångarna till designen på ett begränsat sätt.Detta eliminerar helt behovet av att behöva definiera sekvenser för att driva ingångarna. Denna examensarbetena kommer att beskriva om formell verifiering med jasper gold och kommer att hjälpa verifierar bestämma hur mycket av den formal verifiering metoden kan man användas för att verifiera en ASIC IP med avseende på komplexitet och design uppträdandet att vara verifierat. Resultaten från denna examensarbetena kommer att bevisa hur effektiv formell metoderna var med avseende på simulering metoder att stressa design och verifiera den för undantags fall.Den ändleding varför formell verifiering metoder kan inte användande för TLV och från början till slut funktion verifiering är på grund av design komplexitet.Detta har analyserats med hjälp av en komplex ethernet design.En riktlinje för när kan man använda simulering metoder och formal metoder var föreslagit.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

As geopolíticas que sustentam as políticas externas implementadas durante os governos de Geisel e Lula no primeiro mandato encontram-se fundamentadas nas teorias elaboradas pelos pensadores geopolíticos como Mario Travassos, Meira Mattos e Golbery, O contexto atual do cenário subsaariano, que envolve inúmeros atores participantes das estruturas centrais do sistema mundo e de algumas potências médias, elevam a região subsaariana a uma centralidade na geopolítica atual e serve de justificativa para a contextualização histórica da região subsaariana, bem como da ação diplomática do Brasil e uma comparação das políticas externas desenvolvidas durante os governos dos dois presidentes. A busca de semelhanças ou rupturas em contextos diferenciados procura encontrar a continuidade ou descontinuidade da diplomacia para a região. De outro lado, encontrar as projeções geopolíticas para uma inserção do país nas estruturas centrais do sistema internacional, sabidamente um objetivo antigo da diplomacia brasileira. / The geopolitical underpinning the foreign policies implemented during the government of Lula and Geisel - in the first term - they are based on theories developed by thinkers such as geopolitical Mario Travassos, Meira Mattos and Golbery The current context of Saharan scenario, which involves many actors participants of the central structures of the world average and some power, amounting to a central Saharan region in the current geopolitical and serves as a justification for the historical contextualization of the Saharan region and the diplomatic action of Brazil and a comparison of the policies implemented during the governments of the two presidents. The search for similarities or disruptions in different contexts is searching for the continuity or discontinuity of diplomacy for the region. In addition, find the geopolitical projections for insertion of a country in central structures of the international system, formerly known a goal of Brazilian diplomacy.

As geopolíticas que sustentam as políticas externas implementadas durante os governos de Geisel e Lula no primeiro mandato encontram-se fundamentadas nas teorias elaboradas pelos pensadores geopolíticos como Mario Travassos, Meira Mattos e Golbery, O contexto atual do cenário subsaariano, que envolve inúmeros atores participantes das estruturas centrais do sistema mundo e de algumas potências médias, elevam a região subsaariana a uma centralidade na geopolítica atual e serve de justificativa para a contextualização histórica da região subsaariana, bem como da ação diplomática do Brasil e uma comparação das políticas externas desenvolvidas durante os governos dos dois presidentes. A busca de semelhanças ou rupturas em contextos diferenciados procura encontrar a continuidade ou descontinuidade da diplomacia para a região. De outro lado, encontrar as projeções geopolíticas para uma inserção do país nas estruturas centrais do sistema internacional, sabidamente um objetivo antigo da diplomacia brasileira. / The geopolitical underpinning the foreign policies implemented during the government of Lula and Geisel - in the first term - they are based on theories developed by thinkers such as geopolitical Mario Travassos, Meira Mattos and Golbery The current context of Saharan scenario, which involves many actors participants of the central structures of the world average and some power, amounting to a central Saharan region in the current geopolitical and serves as a justification for the historical contextualization of the Saharan region and the diplomatic action of Brazil and a comparison of the policies implemented during the governments of the two presidents. The search for similarities or disruptions in different contexts is searching for the continuity or discontinuity of diplomacy for the region. In addition, find the geopolitical projections for insertion of a country in central structures of the international system, formerly known a goal of Brazilian diplomacy.

No description available.

No description available.

Cette thèse porte sur le monitorage des simulations de circuits en signaux mixtes. Dans le domaine de la vérification de matériel, l'utilisation de formalismes déclaratifs pour la specification, dans le cadre de la validation par simulation, s'est installée dans la pratique courante. Cependant, le manque de fonctionnalités visant à spécifier les comportements asynchrones, ou l'intégration insuffisante des résultats de la vérification, rend les language d'assertions et de mesures inopérants pour la vérification de comportements en signaux mixtes. Nous proposons des outils théoriques et pratiques pour la description et le monitorage de ces comportements, qui comportent des aspects à la fois discrets et continus. Pour cela, nous nous appuyons sur des travaux antérieurs portant sur les extensions temps-réel de la logique temporelle et des expressions régulières. Nous décrivons de nouveaux algorithmes pour calculer la distance entre une trace de simulation et une propriété en logique temporelle données. Une nouvelle procédure de diagnostic est conçue pour déboguer efficacement de telles traces. Le monitorage des comportements continus est ensuite étendu à d'autres formes d'assertions basées sur des expressions régulières. Ces expressions constituent la base de notre language de description de mesures, qui permet de définir conjointement la mesure et les intervals temporels sur lesquels cette mesure doit être prise. Nous montrons comment d'autres mesures, déjà mises en œuvre dans les simulateurs analogiques peuvent être importées dans les descriptions digitales. Ceci permet d'étendre vers le domaine en signaux mixtes les approches hiérarchiques utilisées en vérification de circuits digitaux. / This thesis is concerned with the monitoring of mixed-signal circuit simulations. In the field of hardware verification, the use of declarative property languages in combination with simulation is now standard practice. However the lack of features to specify asynchronous behaviors, or the insufficient integration of verification results, makes existing assertion and measurement languages unable to enforce mixed-signal requirements. We propose several theoretical and practical tools for the description and automatic monitoring of such behaviors, that feature both discrete and continuous aspects. For this we build on previous work on real-time extensions of temporal logic and regular expressions. We describe new algorithms to compute the distance from some simulation trace to temporal logic specifications, whose complexity is not higher than traditional monitoring. A novel diagnostic procedure is provided in order to efficiently debug such traces. The monitoring of continuous behaviors is then extended to other forms of assertions based on regular expressions. These expressions form the basis of our measurement language, that describes conjointly a measure and the patterns over which that measure should be taken. We show how other measurements implemented in analog circuits simulators can be ported to digital descriptions, this way extending structured verification approaches used for digital designs toward mixed-signal.