The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
The paper presents an experimental evaluation of test generation methods for digital circuits. Two methods are considered: an EFSM-based one, aimed at the code coverage of high-level (RTL) descriptions, and an equivalence-checking based on low-level (gate) description. High-level code and low-level fault coverage are measured for generated tests. Low-level mutants were generated for several fault...
This paper describes a model-based functional test generation method for hardware designs. The main principles are as follows. Two models are extracted from an HDL description: a functional model, which represents the design under scrutiny, and a coverage model, which represents a set of testing goals. Each goal is specified in the negative form to force a model checker to find a counterexample —...
In this paper we propose to think out of the box and discuss an approach for universal mitigation of Negative Bias Temperature Instability (NBTI) induced aging untied from the limitations of its modelling. The cost-effective approach exploits a simple property of a randomized design, i.e., the equalized signal probability and switching activity at gate inputs. The techniques considered for structural...
Electronic System Level (ESL) design flow tries to handle the complexity of today's System-on-Chip design and verification. Due to this complexity, design and verification methodologies start from an abstraction level higher than Register Transfer Level (RTL). In ESL, verification becomes a major bottleneck in the design flow, and finding a good verification methodology at this abstraction level is...
This paper overviews a technique for verifying cache coherence protocols described in the Promela language. The approach is comprised of the following steps. First, a model written for a certain configuration of the memory system is generalized to the model being parameterized with the number of processors. Second, the parameterized model is abstracted from the exact number of processors. Finally,...
In this paper, a tool for automatically generating test programs for ARM VMSAv8-64 memory management units is described. The solution is based on the MicroTESK framework being developed at ISP RAS. The tool consists of two parts: an architecture-independent test program generation core and VMSAv8-64 specifications. Such separation is not a new principle in the area -- it is applied in a number of...
The increasing complexity of hardware designs makes functional verification a challenge. The key issue of the state-of-the-art verification approaches is to obtain a “good” model for automated test generation or formal property checking. In this paper, we describe techniques for deriving EFSM-based models from HDL descriptions and briefly discuss applications of such models for verification. The distinctive...
Simulation-based verification is a widely-spread approach to ensure functional correctness of hardware designs [1,2]. It is usually done by co-simulating a design under verification with an independently created reference model and checking conformance of their reactions. To reduce verification expenses, abstract models are commonly used (they are simpler, less error-prone and more reusable). Design...
Verification has long been recognized as an integral part of the hardware design process. When designing a system, engineers usually use various design representations and concretize them step by step up to a physical layout. At the beginning of the process, when there is much of indeterminacy, only abstract reference models are applicable to verification; when the process is close to the end, more...
Automatic generation and simulation of test programs is known to be the main means for verifying microprocessors. The problem is that test program generators for new designs are often developed from scratch with little reuse of well-tried components. State-of-the-art tools, like Genesys-Pro and RAVEN, meet the challenge by using a model-based approach, where a microprocessor model is separated from...
In this paper we describe a method for simulation-based verification of microprocessor units based on cycle-accurate contract specifications. Such specifications describe behavior of a unit in the form of preconditions and postconditions of microoperations. Test sequence generation is based on traversal of FSM constructed automatically from specifications and test coverage definition. We have successfully...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.