Serwis Infona wykorzystuje pliki cookies (ciasteczka). Są to wartości tekstowe, zapamiętywane przez przeglądarkę na urządzeniu użytkownika. Nasz serwis ma dostęp do tych wartości oraz wykorzystuje je do zapamiętania danych dotyczących użytkownika, takich jak np. ustawienia (typu widok ekranu, wybór języka interfejsu), zapamiętanie zalogowania. Korzystanie z serwisu Infona oznacza zgodę na zapis informacji i ich wykorzystanie dla celów korzytania z serwisu. Więcej informacji można znaleźć w Polityce prywatności oraz Regulaminie serwisu. Zamknięcie tego okienka potwierdza zapoznanie się z informacją o plikach cookies, akceptację polityki prywatności i regulaminu oraz sposobu wykorzystywania plików cookies w serwisie. Możesz zmienić ustawienia obsługi cookies w swojej przeglądarce.
This document describes the IFIP WG10.2 hardware-verification benchmark circuits, intended for evaluating different approaches and algorithms for hardware verification. The paper presents the rationale behind the circuits, describes them briefly and indicates how to get access to the verification benchmark set.
We have developed a formal definition of correctness for pipelines that ensures that transactions terminate and satisfy a functional specification. This definition separates the correctness criteria associated with the pipelining aspects of a design from the functional relationship between input and output transactions. Using this definition, we developed and formally verified a technique that divides...
What does it mean for an instruction pipeline to be correct? We recently completed the specification and verification of a pipelined microprocessor called UINTA. Our proof makes no simplifying assumptions about data and control hazards. This paper presents the specification, describes the verification, and discusses the effect of pipelining on the correctness model. The most significant effect on...
Theorem proving techniques are particularly well suited for reasoning about arithmetic above the bit level and for relating different levels of abstraction. In this paper we show how a non-restoring integer square root algorithm can be transformed to a very efficient hardware implementation. The top level is a Standard ML function that operates on unbounded integers. The bottom level is a structural...
Our approach for verifying the equivalence of two VHDL architectures consists in translating these descriptions into functional forms and then in proving the equivalence of these functions. As far as replicated or parallel architectures are concerned, an induction-based method is used for verifying generic n-bit descriptions. This technique takes advantage of the regular structure of these devices...
To embrace the fast growth of circuit complexity, verification researchers are probing new verification methods. Verification by composition, among others, is regarded as a promising direction. Symbolic Trajectory Evaluation (STE) is a theory for digital circuit verification. In the last a few years, STE has been used in proving practical digital circuits and has been proven a practical methodology...
A major challenge in the area of hardware verification is to devise methods that can handle circuits of practical size. This paper intends to show how the applicability of combinational circuit verification tools based on binary decision diagrams (BDDs) can be greatly improved. The introduction of dynamic variable ordering techniques already makes these tools more robust; a designer no longer needs...
The single pulser is a clocked sequential device which generates a unit-time pulse on its output for every pulse on its input. This paper explores how a single-pulser implementation is verified by various formal reasoning tools, including the PVS theorem prover for higher-order logic, the SMV model checker for computation tree logic, the DDD design derivation system, and the Oct Tools design environment...
Speed-independence is a property of a circuit ensuring correct operating regardless of the magnitude of delays in all its gates. In this paper, circuits are modeled by formal transition systems, and speed-independence is characterized by state predicates expressing constraints on the transition system. This makes it possible to define a formal condition corresponding to speed-independence, and to...
In this paper, we propose a technique for proving the correctness of the implementations of synchronous sequential circuits automatically, where the specifications of synchronous sequential circuits are described in an algebraic language ASL, which we have designed, and the specifications are described in a restricted style. For a given abstract level's specification, we refine the specification into...
This paper describes a mechanized approach to verifying that one concrete design is a refinement of another abstract design. A widely used notion of refinement is trace inclusion, which implies that each externally visible behavior of the concrete design can also be caused by the abstract design. In some cases this is too restrictive and the verification technique proposed here is based on a more...
The attractiveness of using theorem provers for system design verification lies in their generality. The major practical challenge confronting theorem proving technology is in combining this generality with an acceptable degree of automation. We describe an approach for enhancing the effectiveness of theorem provers for hardware verification through the use of efficient automatic procedures for rewriting,...
In this paper, we propose a new approach to formal synthesis which focuses on the generation of verification-friendly circuits. Starting from a high-level implementation description, which may result from the application of usual scheduling and allocation algorithms, hardware is automatically synthesized. The target architecture is based on handshake processes, modules which communicate by a simple...
This tutorial describes a mechanized technique for design verification. The aim is, in the early design phases, to verify selected key properties of a partially specified design. A supporting design language called Synchronized Transitions is used for describing designs. The design verification is mechanized by tools, in particular, a theorem prover called the Larch Prover (lp) used for reasoning...
PVS stands for “Prototype Verification System.” It consists of a specification language integrated with support tools and a theorem prover. PVS tries to provide the mechanization needed to apply formal methods both rigorously and productively. This tutorial serves to introduce PVS and its use in the context of hardware verification. In the first section, we briefly sketch the purposes for which...
A general-purpose proof interface has been created on top of the higher-order-logic theorem prover LAMBDA in order to improve the efficiency of human interaction and minimize the learning overhead. Users are freed from tedious low-level interactions by way of extended proof automation routines. All essential LAMBDA functions for interactive proof development are accessible via a handy set of user...
Formal based synthesis allows design space exploration to identify optimized implementations conforming to the initial abstract specification. Wepropose to exploit the synergies between formal synthesis (at high level of abstraction) and logic synthesis (at lower levels of abstraction). In this way a two-fold goal is reached: quantitative figures are provided as a measureof the applicability of formal...
In this paper we introduce a verification methodology well adapted to circuits where the specifications are described in terms of characteristic properties instead of algorithmic procedures. This method avoids most of the interpretation mistakes which could invalidate the proof process. In order to describe implementations, we present a formalism, based on sequences, which is close to HDLs. Then these...
Diagrams have been left as an informal tool in hardware reasoning, thus rendering them unacceptable representations within formal reasoning systems. We demonstrate some advantages of formally supporting diagrams in hardware verification systems via a simple example from the verification of a single-pulser.
Podaj zakres dat dla filtrowania wyświetlonych wyników. Możesz podać datę początkową, końcową lub obie daty. Daty możesz wpisać ręcznie lub wybrać za pomocą kalendarza.