Search

Symbolic trajectory evaluation is an industrial-strength formal hardware verification method, based on symbolic simulation, which has been highly successful in data-path verification, especially for microprocessor execution units. It is a ‘model-checking’ method in the basic sense that properties, expressed in a simple temporal logic, are verified by (symbolic) exploration of formal models of sequential circuits. Its defining characteristic is that it operates by symbolic simulation over abstractions of sets of states that only partially delineate the circuit states in the set. These abstract state sets are ordered in a lattice by information content, based on a three-valued domain for values on circuit nodes (true, false, and don’t know). The algorithm operates over families of these abstractions encoded by Boolean formulas, providing a flexible, specification-driven mechanism for partitioned data abstraction. We provide a basic introduction to symbolic trajectory evaluation and its extensions, and some details of how it is deployed in industrial practice. The aim is to get across the essence and value of the method in clear and accessible terms.

Systems biology is centrally engaged with computational modelling across multiple scales and at many levels of abstraction. Formal modelling, precise and formalised abstraction relationships, and computation also lie at the heart of computer science—and over the past decade a growing number of computer scientists have been bringing their discipline's core intellectual and computational tools to bear on biology in fascinating new ways. This paper explores some of the apparent points of contact between the two fields, in the context of a multi-disciplinary discussion on conceptual foundations of systems biology.

The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis called Abstract Conflict Driven Learning for Programs (ACDLP). ACDLP alternates between model search, which performs over-approximate deduction with constraint propagation, and conflict analysis, which performs under-approximate abduction with heuristic choice. We instantiate the model search and conflict analysis algorithms to an abstract domain of template polyhedra, strictly generalizing CDCL from the Boolean lattice to a richer lattice structure. Our template polyhedra can express intervals, octagons and restricted polyhedral constraints over program variables. We have implemented ACDLP for automatic bounded safety verification of C programs. We evaluate the performance of our analyser by comparing with CBMC, which uses Boolean CDCL, and Astr´ee, a commercial abstract interpretation tool. We observe two orders of magnitude reduction in the number of decisions, propagations, and conflicts as well as a 1.5x speedup in runtime compared to CBMC. Compared to Astr´ee, ACDLP solves twice as many benchmarks and has much higher precision. This is the first instantiation of CDCL with a template polyhedra abstract domain.

This paper describes a set of theorem proving tools based on a new derived principle of definition in HOL, namely the introduction of relations inductively defined by a set of rules. Such inductive definitions abound an computer science. Example application areas include reasoning about structured operational semantics, type judgements, transition relations for process algebras, reduction relations, and compositional proof systems. The package described in this paper automates the derivation of certain inductive definitions involved in these applications and provides the basic tools needed for reasoning about the relations introduced by them.

One application of equivalence checking is to establish correspondence between a high-level, abstract design and a low-level implementation. We propose a new partitioning technique for the case in which the two designs are substantially different and traditional equivalence-point insertion fails. The partitioning is performed in tandem in both models, exploiting the structure present in the high-level model. The approach generates many but tractable SAT/SMT queries. We present experimental data quantifying the benefit of our partitioning method for both combinational and sequential equivalence checking of difficult arithmetic circuits and control-intensive circuits.

Dynamic hardware reconfiguration based on run-time system specialization is viable with FPGAs. The research challenge for formal verification is to help ensure the correctness of dynamically generated hardware. In this paper, the approach is to verify a specialization synthesis algorithm used to reconfigure FPGA designs at run-time. The verification approach is based on a deep embedding of a language for netlist and the relational hardware modeling style.

The practical utility of interactive, user-guided, theorem proving depends on the design of good interaction environments, the study of which should be grounded in methods of research into human‐computer interaction (HCI). This paper discusses the relevance of classifications of programming errors developed by the HCI community to the problem of interactive theorem proving. A new taxonomy of errors is proposed for interaction with theorem provers and its adequacy as a usability metric is assessed experimentally. q 2000 Elsevier Science B.V. All rights reserved.

Model checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic trajectory evaluation can handle, and deductive theorem proving has long been proposed as a complement to symbolic trajectory evaluation to enable such compositional reasoning. This paper describes an approach to verification by symbolic simulation, called Relational STE, that raises verification properties to the purely logical level suitable for compositional reasoning in a theorem prover. We also introduce a new deductive theorem prover, called Goaled, that has been integrated into Intel's Forte verification framework for this purpose. We illustrate the effectiveness of this combination of technologies by describing a general framework, accessible to non-experts, that is widely used for verification and regression validation of integer multipliers at Intel. © 2013 FMCAD Inc.

The HOL system is an LCF-style mechanized proof assistant for conducting proofs in higher-order logic. This paper discusses a proposal to extend the primitive basis of the logic underlying the HOL system with a very simple form of quantification over types. It is shown how certain practical problems with using the definitional mechanisms of HOL would be solved by the additional expressive power gained by making this extension.

Effective formal verification tools require that robust implementations of automatic procedures for first-order logic and satisfiability modulo theories be integrated into expressive interactive frameworks for logical deduction, such as higher-order logic theorem provers. This paper states some pragmatic requirements for implementations of decision procedures that make them well-suited to integration into such frameworks. The aim is to open a dialogue with the designers of decision procedure software that will lead to greater and easier uptake of their implementations by verification users.

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself. The paper motivates and presents the syntax and type system of this language, which brings together a new combination of pattern-matching and reflection features targeted specifically at our application domain. It also gives an operational semantics based on a novel use of contexts as expression constructors, and it presents a scheme for compiling reFLect programs using the same context mechanism.

Symbolic indexing is a data abstraction technique that exploits the partially-ordered state space of symbolic trajectory evaluation (STE). Use of this technique has been somewhat limited in practice because of its complexity. We present logical machinery and efficient algorithms that provide a much simpler interface to symbolic indexing for the STE user. Our logical machinery also allows correctness assertions proved by symbolic indexing to be composed into larger properties, something previously not possible.

This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prove a theorem that translates correctness results from trajectory evaluation over a four-valued lattice into a shallow embedding of temporal operators over Boolean streams. This translation connects the specialized world of trajectory evaluation to a general-purpose logic and provides the semantic basis for connecting additional decision procedures and model checkers.

A special issue of the Journal of Functional Programming will be devoted to the use of functional programming in theorem proving. The submission deadline is 31 August 1997.The histories of theorem provers and functional languages have been deeply intertwined since the advent of Lisp. A notable example is the ML family of languages, which are named for the meta language devised for the LCF theorem prover, and which provide both the implementation platform and interaction facilities for numerous later systems (such as Coq, HOL, Isabelle, NuPrl). Other examples include Lisp (as used for ACL2, PVS, Nqthm) and Haskell (as used for Veritas).This special issue is devoted to the theory and practice of using functional languages to implement theorem provers and using theorem provers to reason about functional languages. Topics of interest include, but are not limited to:– architecture of theorem prover implementations– interface design in the functional context– limits of the LCF methodology– impact of host language features– type systems– lazy vs strict languages– imperative (impure) features– performance problems and solutions– problems of scale– special implementation techniques– term representations (e.g. de Bruijn vs name carrying vs BDDs)– limitations of current functional languages– mechanised theories of functional programming

The expressive power of higher order logic makes it possible to define a wide variety of types within the logic and to prove theorems that state the properties of these types concisely and abstractly. This paper contains a tutorial introduction to the logical basis for such type definitions. Examples are given of the formal definitions in logic of several simple types. A method is then described for systematically defining any instance of a certain class of commonly-used recursive types. The automation of this method in HOL, an interactive system for generating proofs in higher order logic, is also discussed.