1,721,143 research outputs found
Symbad: Formal Verification in System Level-based Design
No full textThe paper presents the SYMBAD project: a system level design and verification framework for HW and SW integrated systems. Such a framework leads to a new methodology in high-level system design which joins different formal and dynamic verification strategies
Logic-Level Analysis of High-Level Faults
No full textMany high-level fault models have been proposed in the past to perform verification at functional level, however high-level automatic test pattern generators (ATPGs) are still in a prototyping phase, while very efficient logic-level ATPGs are available. This paper proposes a strategy to map high-level faults into logic-level faults. Thus, functional verification, based on a high-level fault model, can be performed by exploiting the capability of state of the art logic-level ATPGs
Too Few or too Many Properties? Measure it by ATPG!
No full textVerification of a design, based on model checking, requires the identification of a set of formal properties manually derived from the specification of the design under verification (DUV). Such a set can include too few or too many properties. This paper proposes to use a functional ATPG to identify missing properties and to remove unnecessary ones. In partic- ular, the paper refines, extends, and compares, with other symbolic approaches, a methodology to estimate the completeness of formal properties, which exploits a functional fault model and a functional ATPG. More- over, the same fault model and ATPG are used to face the opposite problem of identifying useless properties, that is, properties which are in logical consequence. Logical consequence between properties is generally examined by using theorem proving, which may require a large amount of time and space resources. On the contrary, the paper proposes a faster approach which analyzes logical consequence by observing the property capability of revealing functional faults. The joint use of the methodologies allows to optimize the set of properties used for several verification sessions needed to check all design phases of an incremental design flow
Simulation-based Fault Injection with QEMU for Speeding-up Dependability Analysis of Embedded Software
Full text linkSimulation-based fault injection (SFI) represents a valuable solu- tion for early analysis of software dependability and fault tolerance properties before the physical prototype of the target platform is available. Some SFI approaches base the fault injection strategy on cycle-accurate models imple- mented by means of Hardware Description Languages (HDLs). However, cycle- accurate simulation has revealed to be too time-consuming when the objective is to emulate the effect of soft errors on complex microprocessors. To overcome this issue, SFI solutions based on virtual prototypes of the target platform has started to be proposed. However, current approaches still present some draw- backs, like, for example, they work only for specific CPU architectures, or they require code instrumentation, or they have a different target (i.e., design errors instead of dependability analysis). To address these disadvantages, this paper presents an efficient fault injection approach based on QEMU, one of the most efficient and popular instruction-accurate emulator for several microprocessor architectures. As main goal, the proposed approach represents a non intrusive technique for simulating hardware faults affecting CPU behaviours. Perma- nent and transient/intermittent hardware fault models have been abstracted without losing quality for software dependability analysis. The approach mini- mizes the impact of the fault injection procedure in the emulator performance by preserving the original dynamic binary translation mechanism of QEMU. Experimental results for both x86 and ARM processors proving the efficiency and effectiveness of the proposed approach are presented
Exploiting clustering and decision-tree algorithms to mine LTL assertions containing non-boolean expressions
No full textState-of-the-art mining tools generate assertions that either describe the temporal relations between Boolean expressions, or extract non-temporal logic formulas between more complex propositions involving arithmetic and/or relational operators. This paper presents a method for generating Linear Temporal Logic (LTL) assertions containing both the temporal dimension and the complexity of non-Boolean expressions. Starting from a set of simulation traces of the design under verification (DUV), our approach generates LTL assertions where the Boolean layer contains expressions of the form c = ne, c ≤ ne, c ≥ ne, c l ≤ ne ≤ c r , where c, c l , c r are constants of numeric type, and ne is a numerical expression predicating over the variables of the DUV. The method exploits a clustering algorithm to mine a meaningful set of propositions following the aforementioned structure. After that, the propositions are used to generate temporal assertions through a decision tree algorithm. Experimental results show real improvements with respect to the state-of-the-art in terms of fault coverage and readability of the mined assertions
A testbench specification language for SystemC Verification
No full textTesting of embedded systems, operating in the real environment, is generally performed by using an industrial test bench that stimulates the system through sensors and human-machine interfaces. The test bench provides the engineers with a set of tools for reproducing the environmental conditions which may affect the system. On the contrary, a different approach is adopted at the early stages of the design flow, when system level languages, like SystemC, are used to describe the functionality of the design. At this level, stimuli for testing the design are traditionally generated in a random or statistical way, which makes more difficult to capture well-specific behaviors of the considered environment, thus decreasing the effectiveness and the efficiency of the verification. This is particularly evident for dynamic assertion-based verification where, to avoid vacuous passes of assertions, stimuli must reflect specific scenarios to activate the assertions. In this work, we propose a graphical framework to automatically generate stimuli, particularly suited to be used for dynamic ABV of embedded SW. The framework relies on the definition of a Testbench Specification Language (TSL) that allows to formally capture the behavior of the real environment where embedded SW is intended to be executed, i.e., how input values evolve on time intervals. Then, the framework allows to automatically synthesize TSL descriptions into SystemC-based stimuli generators, which exploit and extend the functionality of the SystemC Verification Library
Invited Talk: Pros and Cons of Assertion Mining
No full textAssertion mining flips the way verification works by extracting formal properties from the actual implementation of the target design and searching for inconsistencies with respect to the initial specification. While this removes the burden of time-consuming and error-prone manual definition, are the mined properties actually useful? After reviewing the state of the art concerning existing approaches and tools, this talk questions the pros and cons of assertion mining and describes how mined assertions can be exploited as an effective coverage metrics for functional verification
Simplified stimuli generation for scenario and assertion based verification
No full textSimulation-based approaches that require to drive the design under verification (DUV) to specific conditions, like for example, scenario-based testing and dynamic assertion-based verification (ABV), cannot rely on generic coverage-driven stimuli generators. On the contrary, constraint-based generation must be adopted. In this context, among several solutions, the Universal Verification Methodology (UVM) and the SystemC Verification Library (SCV) represent the main alternatives. However, their powerfulness is paid in term of easiness of use. In fact, their application generally requires to write complex pieces of code to specify the constraints that must be satisfied by the stimuli generator to produce the desired sequences of values. More is the complexity of setting up an effective stimuli generator, more is the risk of failing to capture the right behaviour and/or having a longer verification time. To overcome these problems, the paper presents a framework and a corresponding language for the automatic generation of stimuli that requires to write intuitive and compact directives representing the desired constraints. The approach is independent from the language adopted for the DUV implementation and it works for both embedded hardware as well as embedded software
A Baseline Framework for the Qualification of LTL Specification Miners
No full textOver the past few decades, the verification community has developed several specification miners as an alternative to manual assertion definition. However, assessing their effectiveness remains a challenging task. Most studies evaluate these miners using predefined ranking metrics, which often fail to ensure the quality of the inferred specifications, especially when no fixed ground truth exists and the relevance of the specifications varies depending on the use case. This paper presents a comprehensive framework aimed at facilitating the evaluation and comparison of Linear Temporal Logic (LTL) specification miners. Unlike traditional approaches, which struggle with subjective analyses and complex tool configurations, our framework provides a structured method for assessing and comparing the quality of specifications generated by multiple sources, using both semantic and syntactic techniques. To achieve this, the framework offers users an easy-to-extend environment for installing, configuring, and running third-party miners via Docker containers. Additionally’ it supports the inclusion of new evaluation methods through a modular design. Miner comparison can be based either on user-defined designs or on synthetic benchmarks, which are automatically generated to serve as a non-subjective ground truth for the evaluation of the miners. We demonstrate the utility of our framework through comparative analyses with four well-known LTL miners, illustrating its ability to standardize and enhance the specification mining evaluation process
Smart systems integration and simulation
No full textThis book-presents new methods and tools for the integration and simulation of smart devices. The design approach described in this book explicitly accounts for integration of Smart Systems components and subsystems as a specific constraint. It includes methodologies and EDA tools to enable multi-disciplinary and multi-scale modeling and design, simulation of multi-domain systems, subsystems and components at all levels of abstraction, system integration and exploration for optimization of functional and non-functional metrics. By covering theoretical and practical aspects of smart device design, this book targets people who are working and studying on hardware/software modelling, component integration and simulation under different positions (system integrators, designers, developers, researchers, teachers, students etc.). In particular, it is a good introduction to people who have interest in managing heterogeneous components in an efficient and effective way on different domains and different abstraction levels. People active in smart device development can understand both the current status of practice and future research directions. Provides a comprehensive overview of smart systems design, focusing on design challenges and cutting-edge solutions; Enables development of a co-simulation and co-design environment that accounts for the peculiarities of the basic subsystems and components to be integrated; Describes development of modeling and design techniques, methods and tools that enable multi-domain simulation and optimization at various levels of abstraction and across different technological domains
- …
