• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 54
  • 13
  • 6
  • 6
  • 6
  • 5
  • 5
  • 4
  • 3
  • 3
  • 1
  • Tagged with
  • 118
  • 118
  • 57
  • 53
  • 26
  • 25
  • 25
  • 22
  • 20
  • 19
  • 19
  • 18
  • 16
  • 15
  • 15
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
91

A Unifying Interface Abstraction for Accelerated Computing in Sensor Nodes

Iyer, Srikrishna 31 August 2011 (has links)
Hardware-software co-design techniques are very suitable to develop the next generation of sensornet applications, which have high computational demands. By making use of a low power FPGA, the peak computational performance of a sensor node can be improved without significant degradation of the standby power dissipation. In this contribution, we present a methodology and tool to enable hardware/software co-design for sensor node application development. We present the integration of nesC, a sensornet programming language, with GEZEL, an easy-to-use hardware description language. We describe the hardware/software interface at different levels of abstraction: at the level of the design language, at the level of the co-simulator, and in the hardware implementation. We use a layered, uniform approach that is particularly suited to deal with the heterogeneous interfaces typically found on small embedded processors. We illustrate the strengths of our approach by means of a prototype application: the integration of a hardware-accelerated crypto-application in a nesC application. / Master of Science
92

Design Methods for Cryptanalysis

Judge, Lyndon Virginia 24 January 2013 (has links)
Security of cryptographic algorithms relies on the computational difficulty of deriving the secret key using public information. Cryptanalysis, including logical and implementation attacks, plays an important role in allowing the security community to estimate their cost, based on the computational resources of an attacker. Practical implementations of cryptanalytic systems require complex designs that integrate multiple functional components with many parameters. In this thesis, methodologies are proposed to improve the design process of cryptanalytic systems and reduce the cost of design space exploration required for optimization. First, Bluespec, a rule-based HDL, is used to increase the abstraction level of hardware design and support efficient design space exploration. Bluespec is applied to implement a hardware-accelerated logical attack on ECC with optimized modular arithmetic components. The language features of Bluespec support exploration and this is demonstrated by applying Bluespec to investigate the speed area tradeoff resulting from various design parameters and demonstrating performance that is competitive with prior work. This work also proposes a testing environment for use in verifying the implementation attack resistance of secure systems. A modular design approach is used to provide separation between the device being tested and the test script, as well as portability, and openness. This yields an open-source solution that supports implementation attack testing independent of the system platform, implementation details, and type of attack under evaluation. The suitability of the proposed test environment for implementation attack vulnerability analysis is demonstrated by applying the environment to perform an implementation attack on AES. The design of complex cryptanalytic hardware can greatly benefit from better design methodologies and the results presented in this thesis advocate the importance of this aspect. / Master of Science
93

Co-diseño de sistemas hardware/software tolerantes a fallos inducidos por radiación

Restrepo Calle, Felipe 04 November 2011 (has links)
En la presente tesis se propone una metodología de desarrollo de estrategias híbridas para la mitigación de fallos inducidos por radiación en los sistemas empotrados modernos. La propuesta se basa en los principios del co-diseño de sistemas y consiste en la combinación selectiva, incremental y flexible de enfoques de tolerancia a fallos basados en hardware y software. Es decir, la exploración del espacio de soluciones se fundamenta en una estrategia híbrida de grano fino. El flujo de diseño está guiado por los requisitos de la aplicación. Esta metodología se ha denominado: co-endurecimiento. De esta forma, es posible diseñar sistemas embebidos confiables a bajo coste, donde no sólo se satisfagan los requisitos de confiabilidad y las restricciones de diseño, sino que también se evite el uso excesivo de costosos mecanismos de protección (hardware y software).
94

Modeling of Multiphysics Electromagnetic & Mechanical Coupling and Vibration Controls Applied to Switched Reluctance Machine / Modélisation multiphysique du couplage électromagnétique/mécanique et développement de contrôles de vibration appliqués aux machines à réluctance variable

Zhang, Man 12 September 2018 (has links)
En raison de ses avantages inhérents, tels que son faible coût, sa fiabilité élevée, sa capacité de fonctionnement à grande vitesse et en environnements difficiles, la machine à réluctance variable (MRV) est une solution attrayante pour l'industrie automobile. Cependant, la traction automobile est une application pour laquelle le comportement acoustique du groupe motopropulseur doit être particulièrement considéré, dans l'optique de ne pas dégrader le confort des passagers. Afin de rendre la MRV compétitive pour cette application automobile, le travail présenté se concentre sur plusieurs méthodes de contrôle cherchant à améliorer le comportement acoustique des MRV en réduisant les vibrations d'origine électromagnétique. Un modèle multi-physique électromagnétique / mécanique semi-analytique est proposé à partir de résultats de simulation numérique obtenus par la méthode des éléments finis. Ce modèle multiphysique est composé de modèles électromagnétiques et structurels, qui sont reliés par la composante radiale de la force électromagnétique. Deux méthodes de contrôle sont ensuite proposées. La première réduit la vibration en faisant varier l'angle de coupure du courant, la fréquence du la variation étant basée sur les propriétés mécaniques de la structure MRV. De plus, une fonction aléatoire uniformément distribuée est introduite pour éviter une composante fréquentielle locale de forte vibration. Une seconde méthode est basée sur le contrôle direct de la force (DFC), qui vise à obtenir une force radiale globale plus douce pour réduire les vibrations. Un adaptateur de courant de référence (RCA) est proposé pour limiter l'ondulation de couple introduite par le DFC, provoquée par l'absence de limitation de courant. Cette seconde méthode de réduction des vibrations appelée DFC & RCA est évaluée par des tests expérimentaux utilisant un prototype de MRV 8/6 afin de montrer sa pertinence. Une solution de partitionnement hardware/software est proposée pour implémenter cette méthode sur une carte FPGA utilisée en combinaison avec un microprocesseur. / Due to its inherent advantages Switched Reluctance Machine (SRM) are appealing to the automotive industry. However, automotive traction is a very noise sensitive application where the acoustic behavior of the power train may be the distinction between market success and market failure. To make SRM more competitive in the automotive application, this work will focus on the control strategy to improve the acoustic behavior of SRM by vibration reduction. A semi-analytical electromagnetic/structural multi-physics model is proposed based on the simulation results of numerical computation. This multi-physics model is composed by electromagnetic and structural models, which are connected by the radial force. Two control strategies are proposed. The first strategy to improve the acoustic behavior of SRM by vibration reduction. A semi-analytical electromagnetic/ structural multi-physics model is proposed based on the simulation results of numerical computation. This multi-physics model is composed by electromagnetic and structural models, which are connected by the radial force. Two control strategies are proposed. The first one reduces the vibration by varying the turn-off angle, the frequency of the variable signal is based on the mechanical property of switched reluctance machine. Besides, an uniformly distributed random function is introduced to avoid local high vibration component. Another one is based on the Direct Force Control (DFC), which aims to obtain a smoother total radial force to reduce the vibration. An reference current adapter (RCA) is proposed to limit the torque ripple introduced by the DFC, which is caused by the absence of the current limitation. The second vibration reduction strategy named DFC&RCA is evaluated by experimental tests using an 8/6 SRM prototype. A hardware/software partitioning solution is proposed to implement this method, where FPGA board is used combined with a Microprocessor.
95

Hardware/Software Co-Design for Keyword Spotting on Edge Devices

Jacob Irenaeus M Bushur (15360553) 29 April 2023 (has links)
<p>The introduction of artificial neural networks (ANNs) to speech recognition applications has sparked the rapid development and popularization of digital assistants. These digital assistants perform keyword spotting (KWS), constantly monitoring the audio captured by a microphone for a small set of words or phrases known as keywords. Upon recognizing a keyword, a larger audio recording is saved and processed by a separate, more complex neural network. More broadly, neural networks in speech recognition have popularized voice as means of interacting with electronic devices, sparking an interest in individuals using speech recognition in their own projects. However, while large companies have the means to develop custom neural network architectures alongside proprietary hardware platforms, such development precludes those lacking similar resources from developing efficient and effective neural networks for embedded systems. While small, low-power embedded systems are widely available in the hobbyist space, a clear process is needed for developing a neural network that accounts for the limitations of these resource-constrained systems. In contrast, a wide variety of neural network architectures exists, but often little thought is given to deploying these architectures on edge devices. </p> <p><br></p> <p>This thesis first presents an overview of audio processing techniques, artificial neural network fundamentals, and machine learning tools. A summary of a set of specific neural network architectures is also discussed. Finally, the process of implementing and modifying these existing neural network architectures and training specific models in Python using TensorFlow is demonstrated. The trained models are also subjected to post-training quantization to evaluate the effect on model performance. The models are evaluated using metrics relevant to deployment on resource-constrained systems, such as memory consumption, latency, and model size, in addition to the standard comparisons of accuracy and parameter count. After evaluating the models and architectures, the process of deploying one of the trained and quantized models is explored on an Arduino Nano 33 BLE using TensorFlow Lite for Microcontrollers and on a Digilent Nexys 4 FPGA board using CFU Playground.</p>
96

Timing verification in transaction modeling

Tsikhanovich, Alena 12 1900 (has links)
Les systèmes Matériels/Logiciels deviennent indispensables dans tous les aspects de la vie quotidienne. La présence croissante de ces systèmes dans les différents produits et services incite à trouver des méthodes pour les développer efficacement. Mais une conception efficace de ces systèmes est limitée par plusieurs facteurs, certains d'entre eux sont: la complexité croissante des applications, une augmentation de la densité d'intégration, la nature hétérogène des produits et services, la diminution de temps d’accès au marché. Une modélisation transactionnelle (TLM) est considérée comme un paradigme prometteur permettant de gérer la complexité de conception et fournissant des moyens d’exploration et de validation d'alternatives de conception à des niveaux d’abstraction élevés. Cette recherche propose une méthodologie d’expression de temps dans TLM basée sur une analyse de contraintes temporelles. Nous proposons d'utiliser une combinaison de deux paradigmes de développement pour accélérer la conception: le TLM d'une part et une méthodologie d’expression de temps entre différentes transactions d’autre part. Cette synergie nous permet de combiner dans un seul environnement des méthodes de simulation performantes et des méthodes analytiques formelles. Nous avons proposé un nouvel algorithme de vérification temporelle basé sur la procédure de linéarisation des contraintes de type min/max et une technique d'optimisation afin d'améliorer l'efficacité de l'algorithme. Nous avons complété la description mathématique de tous les types de contraintes présentées dans la littérature. Nous avons développé des méthodes d'exploration et raffinement de système de communication qui nous a permis d'utiliser les algorithmes de vérification temporelle à différents niveaux TLM. Comme il existe plusieurs définitions du TLM, dans le cadre de notre recherche, nous avons défini une méthodologie de spécification et simulation pour des systèmes Matériel/Logiciel basée sur le paradigme de TLM. Dans cette méthodologie plusieurs concepts de modélisation peuvent être considérés séparément. Basée sur l'utilisation des technologies modernes de génie logiciel telles que XML, XSLT, XSD, la programmation orientée objet et plusieurs autres fournies par l’environnement .Net, la méthodologie proposée présente une approche qui rend possible une réutilisation des modèles intermédiaires afin de faire face à la contrainte de temps d’accès au marché. Elle fournit une approche générale dans la modélisation du système qui sépare les différents aspects de conception tels que des modèles de calculs utilisés pour décrire le système à des niveaux d’abstraction multiples. En conséquence, dans le modèle du système nous pouvons clairement identifier la fonctionnalité du système sans les détails reliés aux plateformes de développement et ceci mènera à améliorer la "portabilité" du modèle d'application. / Hardware/Software (Hw/Sw) systems are likely to become essential in all aspects of everyday life. The increasing penetration of Hw/Sw systems in products and services creates a necessity of their efficient development. However, the productive design of these systems is limited by several factors, some of them being the increasing complexity of applications, the increasing degree of integration, the heterogeneous nature of products and services as well as the shrinking of the time-to-market delay. Transaction Level Modeling (TLM) paradigm is considered as one of the most promising simulation paradigms to break down the design complexity by allowing the exploration and validation of design alternatives at high levels of abstraction. This research proposes a timing expression methodology in TLM based on temporal constraints analysis. We propose to use a combination of two paradigms to accelerate the design process: TLM on one hand and a methodology to express timing between different transactions on the other hand. Using a timing specification model and underlining timing constraints verification algorithms can decrease the time needed for verification by simulation. Combining in one framework the simulation and analytical design exploration methods can improve the analytical power of design verification and validation. We have proposed a new timing verification algorithm based on the linearization procedure and an optimization technique to improve its efficiency. We have completed the mathematical representation of all constraint types discussed in the literature creating in this way a unified timing specification methodology that can be used in the expression of a wider class of applications than previously presented ones. We have developed the methods for communication structure exploration and refinement that permitted us to apply the timing verification algorithms in system exploration at different TLM levels. As there are many definitions of TLM and many development environments proposing TLM in their design cycle with several pro and contra, in the context of our research we define a hardware/software (Hw/Sw) specification and simulation methodology which supports TLM in such a way that several modeling concepts can be seen separately. Relying on the use of modern software engineering technologies such as XML, XSLT, XSD, object oriented programming and others supported by the .Net Framework, an approach that makes an intermediate design model reuse possible in order to cope with time-to-market constraint is presented. The proposed TLM design methodology provides a general approach in system modeling that separates various application modeling aspects from system specification: computational models, used in application modeling, supported by the language used for the functional specification and provided by simulator. As a result, in the system model we can clearly identify system functionality without details related to the development platform thereby leading to a better “portability” of the application model.
97

Architectures pour des systèmes de localisation et de cartographie simultanées / Architectures for simultaneous localization and mapping systems

Vincke, Bastien 03 December 2012 (has links)
La robotique mobile est un domaine en plein essor. L'un des domaines de recherche consiste à permettre à un robot de cartographier son environnement tout en se localisant dans l'espace. Les techniques couramment employées de SLAM (Simultaneous Localization And Mapping) restent généralement coûteuses en termes de puissance de calcul. La tendance actuelle vers la miniaturisation des systèmes impose de restreindre les ressources embarquées. L'ensemble de ces constatations nous ont guidés vers l'intégration d'algorithmes de SLAM sur des architectures adéquates dédiées pour l’embarqué.Les premiers travaux ont consisté à définir une architecture permettant à un robot mobile de se localiser. Cette architecture doit respecter certaines contraintes, notamment celle du temps réel, des dimensions réduites et de la faible consommation énergétique.L’implantation optimisée d’un algorithme (EKF-SLAM), en utilisant au mieux les spécificités architecturales du système (capacités des processeurs, implantation multi-cœurs, calcul vectoriel ou parallélisation sur architecture hétérogène), a permis de démontrer la possibilité de concevoir des systèmes embarqués pour les applications SLAM dans un contexte d’adéquation algorithme architecture. Une seconde approche a été explorée ayant pour objectif la définition d’un système à base d’une architecture reconfigurable (à base de FPGA) permettant la conception d'une architecture fortement parallèle dédiée au SLAM. L'architecture définie a été évaluée en utilisant une méthodologie HIL (Hardware in the Loop).Les principaux algorithmes de SLAM sont conçus autour de la théorie des probabilités, ils ne garantissent en aucun cas les résultats de localisation. Un algorithme de SLAM basé sur la théorie ensembliste a été défini garantissant l'ensemble des résultats obtenus. Plusieurs améliorations algorithmiques sont ensuite proposées. Une comparaison avec les algorithmes probabilistes a mis en avant la robustesse de l’approche ensembliste.Ces travaux de thèse mettent en avant deux contributions principales. La première consiste à affirmer l'importance d'une conception algorithme-architecture pour résoudre la problématique du SLAM. La seconde est la définition d’une méthode ensembliste permettant de garantir les résultats de localisation et de cartographie. / Mobile robotics is a growing field. One important research area is Simultaneous Localization And Mapping (SLAM). Algorithms commonly used in SLAM are generally expensive in terms of computing power. The current trend towards miniaturization imposes to restrict the embedded processing units. All these observations lead us to integrate SLAM algorithms on dedicated architectures suitable for embedded systems.The first work was to define an architecture for a mobile robot to localize itself. This architecture must satisfy some constraints, including the real-time, small dimensions and low power consumption. The optimized implementation of a SLAM algorithm, using the best architectural characteristics of the system (capacity of processors, multi-core implementation, SIMD instructions or parallelization on heterogeneous architecture), has demonstrated the ability to design embedded systems for SLAM applications in the context of Hardware-Software codesign.A second approach has been explored with the aim of designing a system based on a reconfigurable architecture (FPGA-based) for a highly parallel architecture dedicated to SLAM. The defined architecture was evaluated using a HIL (Hardware in the Loop) methodology.The main SLAM algorithms use the probabilistic theories, they do not guarantee their localization results. A SLAM algorithm based on interval analysis is defined to guarantee the overall results. Several algorithmic improvements are then proposed. A comparison with probabilistic algorithms highlighted the robustness of the approach.This thesis put forward two main contributions. The first is to affirm the importance of the hardware software codesign to solve the problem of SLAM with real-time constraint. The second is the definition of a new algorithm to ensure the results of localization and mapping.
98

Towards Low-Complexity Scalable Shared-Memory Architectures

Zeffer, Håkan January 2006 (has links)
<p>Plentiful research has addressed low-complexity software-based shared-memory systems since the idea was first introduced more than two decades ago. However, software-coherent systems have not been very successful in the commercial marketplace. We believe there are two main reasons for this: lack of performance and/or lack of binary compatibility.</p><p>This thesis studies multiple aspects of how to design future binary-compatible high-performance scalable shared-memory servers while keeping the hardware complexity at a minimum. It starts with a software-based distributed shared-memory system relying on no specific hardware support and gradually moves towards architectures with simple hardware support.</p><p>The evaluation is made in a modern chip-multiprocessor environment with both high-performance compute workloads and commercial applications. It shows that implementing the coherence-violation detection in hardware while solving the interchip coherence in software allows for high-performing binary-compatible systems with very low hardware complexity. Our second-generation hardware-software hybrid performs on par with, and often better than, traditional hardware-only designs.</p><p>Based on our results, we conclude that it is not only possible to design simple systems while maintaining performance and the binary-compatibility envelope, it is often possible to get better performance than in traditional and more complex designs.</p><p>We also explore two new techniques for evaluating a new shared-memory design throughout this work: adjustable simulation fidelity and statistical multiprocessor cache modeling.</p>
99

Design, Implementation and Evaluation of a Configurable NoC for AcENoCs FPGA Accelerated Emulation Platform

Lotlikar, Swapnil Subhash 2010 August 1900 (has links)
The heterogenous nature and the demand for extensive parallel processing in modern applications have resulted in widespread use of Multicore System-on-Chip (SoC) architectures. The emerging Network-on-Chip (NoC) architecture provides an energy-efficient and scalable communication solution for Multicore SoCs, serving as a powerful replacement for traditional bus-based solutions. The key to successful realization of such architectures is a flexible, fast and robust emulation platform for fast design space exploration. In this research, we present the design and evaluation of a highly configurable NoC used in AcENoCs (Accelerated Emulation platform for NoCs), a flexible and cycle accurate field programmable gate array (FPGA) emulation platform for validating NoC architectures. Along with the implementation details, we also discuss the various design optimizations and tradeoffs, and assess the performance improvements of AcENoCs over existing simulators and emulators. We design a hardware library consisting of routers and links using verilog hardware description language (HDL). The router is parameterized and has a configurable number of physical ports, virtual channels (VCs) and pipeline depth. A packet switched NoC is constructed by connecting the routers in either 2D-Mesh or 2D-Torus topology. The NoC is integrated in the AcENoCs platform and prototyped on Xilinx Virtex-5 FPGA. The NoC was evaluated under various synthetic and realistic workloads generated by AcENoCs' traffic generators implemented on the Xilinx MicroBlaze embedded processor. In order to validate the NoC design, performance metrics like average latency and throughput were measured and compared against the results obtained using standard network simulators. FPGA implementation of the NoC using Xilinx tools indicated a 76% LUT utilization for a 5x5 2D-Mesh network. A VC allocator was found to be the single largest consumer of hardware resources within a router. The router design synthesized at a frequency of 135MHz, 124MHz and 109MHz for 3-port, 4-port and 5-port configurations, respectively. The operational frequency of the router in the AcENoCs environment was limited only by the software execution latency even though the hardware itself could be clocked at a much higher rate. An AcENoCs emulator showed speedup improvements of 10000-12000X over HDL simulators and 5-15X over software simulators, without sacrificing cycle accuracy.
100

Une approche compositionnelle pour la modélisation et l'analyse des composants systemC au niveau TLM et au niveau des Delta Cycles / A Stepwise Compositional Approach to Model and Analyze SystemC Designs at the Transactional Level and the Delta Cycle Level

Harrath, Nesrine 04 November 2014 (has links)
Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément Intégrés mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile. Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l'industrie, l'automatisation du processus de développement de ces systèmes prend de plus en plus d'ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l'ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l'explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le rafinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Nous proposons ensuite une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l'exécution symbolique et l'abstraction des prédicats. Nous proposons un ensemble d'algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d'appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite l'expérimenter pour donner une estimation du pire temps d'exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l'application des techniques du model checking pour prouver la correction de l'analyse abstraite de notre approche. / Embedded systems are increasingly integrated into existing real-time applications. They are usually composed of deeply integrated but heterogeneous hardware and software components. These components are developed under strict constraints. Accordingly, the work of design engineers became more tricky and challenging. To meet the high quality standards in nowadays embedded systems and to satisfy the rising industrial demands, the automatization of the developing process of those systems is gaining more and more importance. A major challenge is to develop an automated approach that can be used for the integrated verification and validation of complex and heterogeneous HW/SW systems.In this thesis, we propose a new compositional approach to model and verify hardware and software written in SystemC language. This approach is based on the SystemC Waiting State Automata (WSA). The SystemC Waiting State Automata are used to model the abstract behavior of hardware or software systems described in SystemC. They preserve the semantics of the SystemC scheduler at the temporal and the delta-cycle level. This model allows to reduce the complexity of the modeling process of complex systems due to the problem of state explosion during modeling while remaining faithful to the original system. The SystemC waiting state automaton is also compositional and supports refinement. In addition, this model is extended with parameters such as time and counters in order to take into account further aspects like temporality and other extra-functional properties such as QoS.In this thesis, we propose a stepwise approach on how to automatically extract the SystemC WSAs from SystemC descriptions. This construction is based on symbolic execution together with predicate abstraction. We propose a set of algorithms to symbolically compose and reduce the SystemC WSAs in order to study, analyze and verify concurrent behavior of systems as well as the data exchange between various components. We then propose to use the SystemC WSA to model and simulate hardware and software systems, and to compute the worst cas execution time (WCET) using the Timed SystemC WSA. Finally, we define how to apply model checking techniques to prove the correctness of the abstract analysis.

Page generated in 0.0399 seconds