Abstract The Move Prover () is a formal verifier for smart contracts written in the Move programming language. has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing. Besides the simplicity of smart contracts and the Move language, three implementation approaches are responsible for the practicality of : (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.

The Libra blockchain is designed to store billions of dollars in assets, so the security of code that executes transactions is important. The Libra blockchain has a new language for implementing transactions, called “Move.” This paper describes the Move Prover, an automatic formal verification system for Move. We overview the unique features of the Move language and then describe the architecture of the Prover, including the language for formal specification and the translation to the Boogie intermediate verification language .

Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network’s properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks. We describe the system architecture and main components, evaluate the technique and discuss ongoing work.

Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We demonstrate a methodology in which developers use an interactive proof assistant to both implement their system and to state a formal theorem defining what it means for their system to be correct. The process of proving this theorem interactively in the proof assistant exposes all implementation errors since any error in the program would cause the proof to fail. As a case study, we implement a new system, Certigrad, for optimizing over stochastic computation graphs, and we generate a formal (i.e. machine-checkable) proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational autoencoder using Certigrad and find the performance comparable to training the same model in TensorFlow.

Reducing the arithmetic precision of a computation has real performance implications, including increased speed, decreased power consumption, and a smaller memory footprint. For some architectures, e.g., GPUs, there can be such a large performance difference that using reduced precision is effectively a requirement. The tradeoff is that the accuracy of the computation will be compromised. In this paper we describe a proof assistant and associated static analysis techniques for efficiently bounding numerical and precision-related errors. The programmer/compiler can use these bounds to numerically verify and optimize an application for different input and machine configurations. We present several case study applications that demonstrate the effectiveness of these techniques and the performance benefits that can be achieved with rigorous precision analysis.

This paper describes an automatic method for proving equivalence of implementations of block ciphers (and similar cryptographic algorithms). The method can compare two object code implementations or compare object code to a formal, mathematical specification. In either case it proves that the computations being compared are bit-for-bit equivalent. The method has two steps. First the computations are represented as large mathematical terms. Then the two terms are proved equivalent using a phased approach that includes domain-specific optimizations for block ciphers and relies on a careful choice of both word-level and bit-level simplifications. The verification also relies on STP [5], a SAT-based decision procedure for bit-vectors and arrays. The method has been applied to verify real, widely-used Java code from Sun Microsystems and the open source Bouncy Castle project. It has been applied to implementations of the block ciphers AES, DES, Triple DES (3DES), Blowfish, RC2, RC6, and Skipjack as well as applications of the cryptographic hash functions SHA-1 and MD5 on fixed-length messages.

This article presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code. Instead of running code on manually or randomly constructed input, EXE runs it on symbolic input initially allowed to be anything. As checked code runs, EXE tracks the constraints on each symbolic (i.e., input-derived) memory location. If a statement uses a symbolic value, EXE does not run it, but instead adds it as an input-constraint; all other statements run as usual. If code conditionally checks a symbolic expression, EXE forks execution, constraining the expression to be true on the true branch and false on the other. Because EXE reasons about all possible values on a path, it has much more power than a traditional runtime tool: (1) it can force execution down any feasible program path and (2) at dangerous operations (e.g., a pointer dereference), it detects if the current path constraints allow any value that causes a bug. When a path terminates or hits a bug, EXE automatically generates a test case by solving the current path constraints to find concrete values using its own co-designed constraint solver, STP. Because EXE’s constraints have no approximations, feeding this concrete input to an uninstrumented version of the checked code will cause it to follow the same path and hit the same bug (assuming deterministic code). EXE works well on real code, finding bugs along with inputs that trigger them in: the BSD and Linux packet filter implementations, the dhcpd DHCP server, the pcre regular expression library, and three Linux file systems.

This paper presents EXE, an effective bug-finding tool that automatically generates inputs that crash real code. Instead of running code on manually or randomly constructed input, EXE runs it on symbolic input initially allowed to be "anything." As checked code runs, EXE tracks the constraints on each symbolic (i.e., input-derived) memory location. If a statement uses a symbolic value, EXE does not run it, but instead adds it as an input-constraint; all other statements run as usual. If code conditionally checks a symbolic expression, EXE forks execution, constraining the expression to be true on the true branch and false on the other. Because EXE reasons about all possible values on a path, it has much more power than a traditional runtime tool: (1) it can force execution down any feasible program path and (2) at dangerous operations (e.g., a pointer dereference), it detects if the current path constraints allow any value that causes a bug.When a path terminates or hits a bug, EXE automatically generates a test case by solving the current path constraints to find concrete values using its own co-designed constraint solver, STP. Because EXE's constraints have no approximations, feeding this concrete input to an uninstrumented version of the checked code will cause it to follow the same path and hit the same bug (assuming deterministic code).EXE works well on real code, finding bugs along with inputs that trigger them in: the BSD and Linux packet filter implementations, the udhcpd DHCP server, the pcre regular expression library, and three Linux file systems.

We introduce a heuristic for automatically checking the validity of first-order formulas of the form forallalphamexistbetanmiddot Psi(alpham,betan) that are encountered in inductive proofs of hardware correctness. The heuristic introduced in this paper is used to automatically check the validity of k-step induction formulas needed to verify hardware designs. The heuristic works on word-level designs that can have data and address buses of arbitrary widths. Our refinement heuristic relies on the idea of predicate instantiation introduced in (H. Abu-Haimed et al., 2003). The heuristic proves quantified formulas by the use of a validity checker, CVC (A. Stump et al., 2002), and a first-order theorem prover, Otter (W.W. McCune, 1994). Our heuristic can be used as a stand-alone technique to verify word-level designs or as a component in an interactive theorem prover. We show the effectiveness of this heuristic for hardware verification by verifying a number of hardware designs completely automatically. The large size of the quantified formulas encountered in these examples shows the effectiveness of our heuristic as a component of a theorem prover

Partitioned BDD-based algorithms have been proposed in the literature to solve the memory explosion problem in BDD-based verification. Such algorithms can be at times ineffective as they suffer from the problem of scheduling the relative order in which the partitions are processed. In this paper we present a novel multi-threaded reachability algorithm that avoids this scheduling problem while increasing the latent parallelism in partitioned state space traversal. We show that in most cases our method is significantly faster than both the standard reachability algorithm as well as the existing partitioned approaches. The gains are further magnified when our threaded implementation is evaluated in the context of a parallel framework.

Summary form only given. Touch-screen voting machines store records of cast votes in internal memory where the voter cannot check them. Because of our system of secret ballots, once the voter leaves the polls there is no way anyone can determine whether the vote captured was what the voter intended. Why should voters trust these machines? In December 2003, I drafted a resolution on electronic voting stating that every voting system should have a voter verifiable audit trail, which is a permanent record of the vote that can be checked for accuracy by the voter, and which is saved for a recount if it is required. After many rewrites, I posted the page in January 2004 with endorsements from many prominent computer scientists. At that point, I became embroiled in a surprisingly fierce (and time consuming) battle that continues today. We still do not have an answer for why we should trust electronic voting machines, but a lot of evidence has emerged for why we should not. I discuss the basic principles and issues in electronic voting.

Do formal verification tools and methodologies require a drastic overhaul to move beyond equivalence checking? Equivalence checking catches errors in synthesis and local hand-modifications to designs. However, powerful formal verification technologies are emerging to combat "behavioral" errors, which represent today's biggest verification problems. Nonetheless, formal verification experts are split on how formal tools should adapt to this challenge. Some of our panelists feel that designers can sufficiently benefit from new formal verification technologies by making incremental changes to current methodologies. Others, however, argue that major changes are required to reap meaningful benefits from these new technologies. Just how much change is enough, what is the capacity of our current tools and what is limiting the full deployment of FV technology.Our panel of experts, consisting of users, tool providers, and core engine builders, will answer these challenging questions. The panel will debate these issues while discussing real life examples from the user base. They will provide a perspective of how the progression of technology will bring the real promise of formal verification to the user base.

This paper presents novel uses of functional interface specifications for verifying RTL designs. We demonstrate how a simulation environment, a correctness checker, and a functional coverage metric are all created automatically from a single specification. Additionally, the process exploits the structure of a specification written with simple style rules. The methodology was used to verify a large-scale I/O design from the Stanford FLASH project.

The use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used despite its advantages. In this paper, we present a method for automatically extracting models from low level software implementations. Our method is based on the use of an extensible compiler system, xg++, to perform the extraction. The extracted model is combined with a model of the hardware, a description of correctness, and an initial state. The whole model is then checked with the Murφ model checker. As a case study, we apply our method to the cache coherence protocols of the Stanford FLASH multiprocessor. Our system has a number of advantages. First, it reduces the cost of creating models, which allows model checking to be used more frequently. Second, it increases the effectiveness of model checking since the automatically extracted models are more accurate and faithful to the underlying implementation. We found a total of 8 errors using our system. Two errors were global resource errors, which would be difficult to find through any other means. We feel the approach is applicable to other low level systems.

Recently, we have improved the efficiency of the predicate abstraction scheme presented by Das, Dill and Park (1999). As a result, the number of validity checks needed to prove the necessary verification condition has been reduced. The key idea is to refine an approximate abstract transition relation based on the counter-example generated. The system starts with an approximate abstract transition relation on which the verification condition (in our case, this is a safety property) is model-checked. If the property holds then the proof is done; otherwise the model checker returns an abstract counter-example trace. This trace is used to refine the abstract transition relation if possible and start anew. At the end of the process, the system either proves the verification condition or comes up with an abstract counter-example trace which holds in the most accurate abstract transition relation possible (with the user-provided predicates as a basis). If the verification condition fails in the abstract system, then either the concrete system does not satisfy it or the abstraction predicates chosen are not strong enough. This algorithm has been used on a concurrent garbage collection algorithm and a secure contract-signing protocol. This method improved the performance on the first problem significantly, and allowed us to tackle the second problem, which the previous method could not handle.

A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis and automated theorem proving. This paper presents a decision procedure for an extensional theory of arrays and proves it correct.

This paper presents an algorithm for hardware verification that uses simulation and satisfiability checking techniques to determine the correctness of a symbolic test case on a circuit. The goal is to have coverage greater than that of random testing, but with the ease of use and predictability of directed testing. The user uses symbolic variables in simple directed tests to increase the input space that is explored. The algorithm, which is called quasi-symbolic simulation, simulates these tests using only scalar (0,1,X) values internally causing potentially conservative values to be generated at the outputs. Divide and conquer of the symbolic input space is used to resolve this conservativeness. In the best case, this method is as efficient as symbolic simulation using BDDs and, in the worst case, gives coverage and predictability at least as good as directed testing.

BDD-based symbolic techniques of approximate reachability analysis based on decomposing the circuit into a collection of overlapping sub-machines (also referred to as overlapping projections) have been recently proposed. Computing a superset of the reachable states in this fashion is susceptible to false negatives. Searching for real counterexamples in such an approximate space is liable to failure. In this paper the "hybridization effect" induced by the choice of projections is identified as the cause for the failure. A heuristic based on Hamming Distance is proposed to improve the choice of projections, that reduces the hybridization effect and facilitates either a genuine counterexample of proof of the property. The ideas are evaluated on a real large design example from the PCI Interface unit in the MAGIC chip of the Stanford FLASH Multiprocessor.

Automatic state exploration tools (model checkers) have had some success when applied to protocols and hardware designs, but there are fewer success stories about software. This is unfortunate, since the software problem is worsening even faster than the hardware and protocol problems. Model checking of concurrent programs is especially interesting, because they are notoriously difficult to test, analyze, and debug by other methods.

This paper presents initial results in model checking multi-threaded Java programs. Java programs are translated into the SAL (Symbolic Analysis Laboratory) intermediate language, which supports dynamic constructs such as object instantiations and thread call stacks. The SAL model checker then exhaustively checks the program description for deadlocks and assertion failures, using traditional model checking optimizations to curb the state explosion problem. Most of the advanced features of the Java language are modeled within our framework.

Aggregation abstraction is a way of defining a desired correspondence between an implementation of a transaction-oriented protocol and a much simpler idealized version of the same protocol. This relationship can be formally verified to prove the correctness of the implementation. We present a technique for checking aggregation abstractions automatically using a finite-state enumerator. The abstraction relation between implementation and specification is checked on-the fly and the verification requires examining no more states than checking a simple invariant property. This technique can be used alone for verification of finite-state protocols, or as preparation for a more general aggregation proof using a general-purpose theorem-prover. We illustrate the technique on the cache coherence protocol used in the FLASH multiprocessor system.

Approximate reachability techniques trade o accuracy for the capacity to deal with bigger designs. Cho et al [4] proposed partitioning the set of state bits into mutually disjoint subsets and doing symbolic forward reachability on the individual subsets to obtain an overapproximation of the reachable state set. Recently [7] this was improved upon by dividing the set of state bits into various subsets that could possibly overlap, and doing symbolic reachability over the overlapping subsets. In this paper, we further improve on this scheme by augmenting the set of state variables with auxiliary state variables. These auxiliary state variables are added to capture some important internal conditions in the combinational logic. Approximate symbolic forward reachability onoverlapping subsets of this augmented set of state variables yields much tighter approximations than earlier methods. 1

The Mur/spl psi/ description language and verification system for finite-state concurrent systems is applied to the problem of specifying a family of multiprocessor memory models described in the SPARC Version 9 architecture manual. The description language allows for a straightforward operational description of the memory model which can be used as a specification for programmers and machine architects. The automatic verifier can be used to generate all possible outcomes of small assembly language multiprocessor programs in a given memory model, which is very helpful for understanding the subtleties of the model. The verifier can also check the correctness of assembly language programs including synchronization routines. This paper describes the memory models and their encoding in the Mur/spl psi/ description language. We describe how synchronization routines can be verified and how finite state programs can be analyzed. We also present some interesting findings from the verification and the analysis.

This paper describes a pseudo-polynomial time algorithm for timing analysis of a class of choice-free asynchronous systems, called tightly coupled systems, with both min- and max-type timing constraints and bounded component delays. The algorithm consists of two phases: (1) long-term behavior analysis, that computes bounds on the time separation of events after the system has run for a sufficiently long period of time, and (2) startup behavior analysis, that computes time separations between events during an initial startup period after the system is powered up. The results of the analysis are conservative in the worst case; nevertheless, they are found to be exact in our experiments. To demonstrate the practical utility of the approach, an asynchronous differential equation solver chip has been modeled and analyzed using the proposed algorithm. We report results of datapath timing verification, intercontroller protocol timing verification and performance analysis of the chip using the proposed technique.

We introduce a new design style called extended burst-mode. The extended burst-mode design style covers a wide spectrum of sequential circuits ranging from delay-insensitive to synchronous. We can synthesize multiple-input change asynchronous finite state machines and many circuits that fall in the gray area (hard to classify as synchronous or asynchronous) which are difficult or impossible to synthesize automatically using existing methods. Our implementation of extended burst-mode machines uses standard CMOS logic, generates low-latency outputs, and guarantees freedom from hazards at the gate level. In Part I, we formally define the extended burst-mode specification, provide an overview of the synthesis methods, and describe the hazard-free synthesis requirements for two different next-state logic synthesis methods: two-level sums-of-products implementation and generalized C-elements implementation. We also present an extension to existing theories for hazard-free combinational synthesis to handle nonmonotonic input changes.

We introduce a new design style called extended burst-mode. The extended burst-mode design style covers a wide spectrum of sequential circuits ranging from delay-insensitive to synchronous. We can synthesize multiple-input change asynchronous finite state machines and many circuits that fall in the gray area (hard to classify as synchronous or asynchronous) which are difficult or impossible to synthesize automatically using existing methods. Our implementation of extended burst-mode machines uses standard CMOS logic, generates low-latency outputs, and guarantees freedom from hazards at the gate level. In Part II, we present a complete set of automated sequential synthesis algorithms: hazard-free state assignment, hazard-free state minimization, and critical-rare-free state encoding. Experimental data from a large set of examples are presented and compared to competing methods whenever possible.

Bit-v ector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in suc h a theory is NP-hard, our implementation is efficient for many practical examples. We believ e this to be the first such implementation which is efficient, automatic, and complete.

This embedded tutorial surveys some possibilities for verification techniques that combine conventional simulation and ideas, techniques, and algorithms from formal verification, to obtain better functional test coverage of large designs.

Approximate reachability tec hniques trade off accuracy with the capacity to deal with bigger designs. Cho et al [3] proposed approximate FSM traversal algorithms over a partition of the set of state bits. In this paper w egeneralize it by allowing projectionson to a collection of nondisjoint subsets of the state variables. We establish the adv an tageof ha ving overlapping projections and present a new multiple constr ainfunction for BDDs, to compute efficiently the approximate image during symbolic forward propagation using overlapping projections. We demonstrate the effectiveness of this new algorithm by applying it to several control modules from the I/O unit in the Stanford FLASH Multiprocessor. We also present our results on the larger ISCAS 89 benchmarks.

In practice, model checkers are most useful when they find bugs, not when they prove a property. However, because large portions of the state space of the design actually satisfy the specification, model checkers devote much effort verifying correct portions of the design. In this paper, we enhance the bug-finding capability of a model checker by using heuristics to search the states that are most likely to lead to an error, first. Reductions of 1 to 3 orders of magnitude in the number of states needed to find bugs in industrial designs have been observed. Consequently, these heuristics can extend the capability of model checkers to find bugs in designs.

Approximate reachability techniques trade off accuracy for the capacity to deal with bigger desigw.In this paper, we extend the idea of approximations using overlapping projection to symbolic backward reachability.Thti is combined with a previous method of computing ouerapprom.mateforward reachable state sets using overlapping projections.The algom"thmcomputes a superset of the set of states that lie on a path from the initial state to a state that violates a specified invan.antproperty.If this set h empty, there ti no possibility of violating the invan.ant.If this set is non-empty, it may be possible to prove the existence of such a path by searching for a counter-example.A simple heuristic is given, which seems to work well in practice, for generating a counter-example path from this appron.mation.JVe evaluate these new algom.thmsby applying them to several control modules porn the I/O unit in the Stanford FLASH J!ultiprocessor.

We examine the implications of a new hazard-free combinational logic synthesis method, which generates multiplexor-based networks from binary decision diagrams (BDD's)-representations of logic functions factored recursively with respect to input variables-on extended burst-mode asynchronous synthesis. First, this method guarantees that there exists a hazard-free BDD-based implementation for every legal extended burst-mode specification. Second, it reduces the constraints on state minimization and assignment, which reduces the number of additional state variables required in many cases. Third, in cases where conditional signals are sampled, it eliminates the need for state variable changes preceding output changes, which reduces overall input-to-output latency. Last, we describe a circuit that exemplifies how the BDD variable ordering affects the path delay.

We describe a polynomial-time approximate algorithm for computing minimum and maximum time separations between all pairs of events in systems specified by acyclic timing constraint graphs. Even for acyclic graphs, the problem is NP-complete. We propose finding an approximate solution by first approximating the non-convex feasible space with a suitable convex "envelope", and then solving the problem efficiently in the approximate convex space. Unlike previous works, our algorithm can handle both min and max type timing constraints in the same system, and has a computational complexity that is polynomial in the number of events. Although the computed separations are conservative in the worst-case, experiments indicate that our results are highly accurate in practice.

We reduce the state explosion problem in automatic verification of finite-state systems by automatically collapsing subgraphs of the state graph into abstract states. The key idea of the method is to identify state generation rules that can be inverted. It can be used for verification of deadlock-freedom, error and invariant checking and stuttering-invariant CTL model checking. 1 Introduction Formal verification methods that rely on state enumeration are very effective in catching errors in designs. However, such methods suffer from the state explosion problem: the vast number of possibilities cannot be explored within available time and memory. The number of possibilities usually grows exponentially with number of components in the system. Although many techniques (e.g. BDDs [1, 3]) have been developed to tackle the state explosion problem, a lot of practical designs are still too complicated for automatic verification, especially for high level systems or protocols [8]. In this exp...

To verify cache coherence protocols for distributed multiprocessor

We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessor control circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description.

We describe the design of a high performance asynchronous SCSI (small computer systems interface) controller data path and the associated control circuits. The data path is an asynchronous pipeline and the control circuits for the data path are built out of extended burst-mode machines. This design is functionally compatible with a widely used commercial SCSI controller and was simulated correctly with respect to all of the applicable test vectors used for the commercial design. The technology used for this design is a 0.8 /spl mu/m CMOS standard cell. The performance is limited by the SCSI specification, not the design itself, and the area is competitive with the commercial design. This design improves the data transfer throughput by up to 2.5 times from previous work by incorporating a FIFO and a distributed control scheme based on extended burst-mode state machines.

Modern, high performance microprocessors are extremely complex machines which require substantial validation effort to ensure functional correctness prior to tapeout. Generating the corner cases to test these designs is a mostly manual process, where completion is hard to judge. Experience shows that the errors that are caught late in the design, many post-silicon, are interactions between different components in very improbable corner case situations. In this paper we present a technique that targets such error-causing interactions by automatically generating test vectors that will cause the processor to exercise all transitions of the control logic in simulation. We use techniques from formal verification to derive transition tours of a fully enumerated state graph of the control logic of the processor. Our system works from a Verilog description of the original machine and is currently being used to validate an embedded dual-issue processor in the node controller of the Stanford FLASH Multiprocessor. Modeling the processor control results in 200K states and an 8M instruction trace to check all transitions of control arcs.

The Murp description language and verijcation system for$nite-

This paper describes a new method for exact hazard-free logic-minimization of Boolean functions. Given an incompletely-specified Boolean function, the method produces a minimum-cost sum-of-products implementation which is hazard-free for a given set of multiple-input changes, if such a solution exists. The method is a constrained version of the Quine-McCluskey algorithm. It has been automated and applied to a number of examples. Results are compared with results of a comparable non-hazard-free method (espresso-exact). Overhead due to hazard elimination is shown to be negligible.>

In previous work, Hu and Dill identified a common cause of BDD-size blowup in high-level design verification and proposed the method of implicitly conjoined invariants to address the problem.That work, however, had some limitations: the user had to supply the property being verified as an implicit conjunction of BDDs, the heuristic used to decide which conjunctions to evaluate was rather simple, and the termination test, though fast and effective on a set of examples, was not proven to be always correct.In this work, we address those problems by proposing a new, more sophisticated heuristic to simplify and evaluate lists of implicitly conjoined BDDs and an exact termination test.We demonstrate on examples that these more complex heuristics are reasonably efficient as well as allowing verification of examples that were previously intractable.

The temporal logic model checking algorithm of Clarke, Emerson, and Sistla (1986) is modified to represent state graphs using binary decision diagrams (BDD's) and partitioned transition relations. Because this representation captures some of the regularity in the state space of circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5/spl times/10/sup 120/ states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to express a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.>

Many researchers have reported that the use of Boolean decision diagrams (BDDs) greatly increases the size of hardware designs that can be formally verified automatically.Our own experience with automatic verification of high-level aspects of hardware design, such as protocols for cache coherence and communications, contradicts previous results; in fact BDDs have been substantially inferior to brute-force algorithms that store states explicitly in a table.We betieve that new techniques will be needed to realize the potential advantages of BDD verification at the protocol level.Here, we identify &nctionally dependent variables as a common cause of BDD-size blowup, and describe new techniques to avoid the problem.Using the improved algorithm, we reduce an exponentiallysized problem to a provably O(n log n)-sized one, achieving several orders of magnitude reduction in BDD size.

Article Automatic technology mapping for generalized fundamental-mode asynchronous designs Share on Authors: Polly Siegel View Profile , Giovanni De Micheli View Profile , David Dill View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 61–67https://doi.org/10.1145/157485.164573Online:01 July 1993Publication History 41citation249DownloadsMetricsTotal Citations41Total Downloads249Last 12 Months7Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Hierarchical descriptions of combinational circuits often contain apparent loops. Since it may be difficult to distinguish apparent loops from actual loops, it is useful to construct models of combinational circuits that can handle cyclic dependencies. We show that Boolean relations are inadequate for this purpose, and define a ternary model that solves the problem. We use the model to characterize exact solutions to a broad class of substitution and rectification problems. The theory cleanly handles network transformations that might introduce cyclic dependencies.

We present a design style and synthesis algorithm that encompasses both asynchronous and synchronous state machines. Our proposed design style not only supports generalized "burst-mode" multiple-input change asynchronous designs, but also allows the automatic synthesis of any synchronous Moore machine using only basic gates (and not state-holding elements). Moreover, the synthesis method covers many circuit styles in the range between burst-mode and fully synchronous. We can easily specify and synthesize sequential circuits which change state on both rising and falling clock edges, have multiple-phase clocks, etc., and mixed synchronous/asynchronous designs, subject only to setup and hold-time constraints. To demonstrate the effectiveness of the design style and the synthesis tool, we present a modified version of a previously published large practical controller design - the SCSI data transfer controller redesigned to improve performance and to eliminate preprocessing circuit for converting "level-sensitive" signals to "edge-sensitive" signals, often a cumbersome manual design process, by interfacing directly with "level-sensitive" signals.

Previously (Proc. 11th Symp. on Computer Hardware Description Languages and their Application, April 1993), we proposed a reduction technique based on symmetries to alleviate the state explosion problem in automatic verification of concurrent systems. This paper describes the results of testing the technique on a wide range of algorithms and protocols, including realistic multiprocessor synchronization algorithms and cache coherence protocols. Memory requirements were reduced by amounts ranging from 83% to over 99%, and time requirements were often reduced as well. We also consider the effectiveness of the technique on different types of symmetries, such as symmetries in identical system components and symmetries in data values.>

A method for exact hazard-free logic minimization of Boolean functions is described. Given an incompletely specified Boolean function, the method produces a minimal sum-of-products implementation which is hazard-free for a given set of multiple-input changes, if such a solution exists. The method is a constrained version of the Quine-McCluskey algorithm. It has been automated and applied to a number of examples. Results are compared with results of a comparable non-hazard-free method (espresso-exact). Overhead due to hazard elimination is shown to be negligible.>

An automatic synthesis tool (3D) for designing asynchronous controllers from burst-mode specifications, a class of specifications allowing multiple input change fundamental mode operation, is described. An algorithm for constructing a three-dimensional next-state table, a heuristic for encoding states, and a procedure for generating necessary constraints for exact logic minimization are presented. The effectiveness of the 3D implementation and the synthesis procedure on numerous designs including a large realistic example (asynchronous data transfer protocol of the SCSI bus controller) is demonstrated. The latency (input to output delay) and the cycle time (time required for the circuit to stabilize after the excitation) for all benchmark designs using a 0.8- mu m CMOS standard cell library are estimated.>

The role of automatic formal protocol verification in hardware design is considered. Principles that maximize the benefits of protocol verification while minimizing the labor and computation required are identified. A novel protocol description language and verifier (both called Mur phi ) are described, along with experiences in applying them to two industrial protocols that were developed as part of hardware designs.>

Algorithms for analyzing systems of inequalities with min/max constraints that arise in interface timing specifications are examined. A general form of the inequality is shown to be NP-complete, but some interesting special cases can be solved efficiently. A branch-and-bound solution to the general case is developed and applied to a previously published example.>

The authors evaluate their proposed asynchronous state-machine synthesis method, which uses locally synthesized clocks, on two realistic examples: a DRAM controller and a small computer systems interface controller. These circuits are designed to satisfy existing interface specifications, and are substantially larger than interfaces that have been created by competing methods, such as signal transition graph synthesis. The performance of the resulting implementations is at least as good as that of comparable synchronous implementations.>

A synthesis procedure for designing asynchronous controllers from burst-mode specifications, a class of specifications allowing multiple-input-change fundamental mode operation, is described. This implementation of burst-mode state machines uses standard combinational logic, generates low-latency outputs and guarantees freedom from hazards at the gate level. It requires no locally synthesized clock and no storage elements. In addition, primary outputs as well as additional state variables are used as feedback variables. The state assignment technique is based on the construction of a three-dimensional next-state table.>

Three algorithms for checking the emptiness of a timed transition system have been implemented. The first algorithm performs a straightforward reachability analysis on sets of states of the system, rather than on individual states. This corresponds to stepping symbolically through the system many states at a time. The other two algorithms are minimization algorithms. These simultaneously perform reachability analysis and minimization from an implicit system description. The paradigm for verification is to test for the emptiness of the set of all timed system executions that violate a requirements specification. Preliminary results over two simple examples indicate that memory usage is a more limiting factor than time.>

The authors describe a novel automated design methodology for asynchronous state-machine controllers. Using a local-clocking scheme, the method allows multiple input changes and produces hazard-free designs with a minimal or near-minimal number of states. The authors present an automated program for asynchronous state machine synthesis, and describe a new heuristic for state minimization and new optimizations to improve implementations. The program is used to synthesize competitive implementations of published designs; results are compared.>

A completion-detection method is proposed for efficiently implementing Boolean functions as self-timed logic structures. Current-sensing completion detection (CSCD) allows self-timed circuits to be designed using single-rail variable encoding (one signal wire per logic variable) and implemented in about the same silicon area as an equivalent synchronous implementation. Compared to dual-rail encoding methods, CSCD can reduce the number of signal wires and transistors used by approximately 50%. CSCD implementations improved performance over equivalent dual-rail designs because of: reduced parasitic capacitance, removal of spacer tokens in the data stream, and computation state similarity of consecutive data variables. Several CSCD configurations are described and evaluated and transistor-level implementations are provided for comparison.>

A novel, correct design methodology for asynchronous state-machine controllers is presented. The goal of this work is a design style as close to a synchronous one as possible, but with the advantages of an asynchronous method. The implementations realize asynchronous state-machine specifications using standard combinational logic, flow latches as storage elements, and a locally-generated clocking signal that pulses whenever there is a change in state. This design style allows multiple input changes which can arrive at arbitrary times. The implementations use a minimal or near-minimal number of states. It also allows arbitrary state encoding and flexibility in logic minimization and gate-level realization, so it can take advantage of systematic CAD optimization techniques.>

The temporal logic model checking algorithm developed by Clarke, Emerson, and Sistla [9] is modified to represent a state graph using binary decision diagrams (BDD's) [4]. Because this representation captures some of the regularity in the state space of sequential circuits with data path logic, we are able to verify circuits with an extremely large number of states. We demonstrate this new technique on a synchronous pipelined design with approximately 5 x 1020 states. Our model checking algorithm handles full CTL with fairness constraints. Consequently, we are able to handle a number of important liveness and fairness properties, which would otherwise not be expressible in CTL. We give empirical results on the performance of the algorithm applied to both synchronous and asynchronous circuits with data path logic.

A formal verification method for concurrent systems is presented. The technique shows a correspondence between automata representing an implementation and specification behavior. The correspondence is called a refinement relation, and is particularly well-suited for theorem-provers. Since the method does not rely on enumerating all the states, it can be applied to systems with an infinite or unknown number of states. This substantially expands the class of hardware designs that can be formally verified. The method is illustrated by proving the consistency of a concurrent, non-deterministic model of cache memory. The proof is carried out using the HOL (higher-order logic) theorem-prover.>

This research extends CTL model-checking to the analysis of real-time systems, whose correctness depends on the magnitudes of the timing delays. For specifications, the syntax of CTL is extended to allow quantitative temporal operators. The formulas of the resulting logic, TCTL, are interpretation over continuous computation trees, trees in which paths are maps from the set of nonnegative reals to system states. To model finite-state systems the notion of timed graphs is introduced-state-transition graphs extended with a mechanism that allows the expression of constant bounds on the delays between the state transition. As the main result, an algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with respect to a timed graph. It is argued that choosing a dense domain, instead of a discrete domain, to model time does not blow up the complexity of the model-checking problem. On the negative side, it is shown that the denseness of the underlying time domain makes TCTL II/sub 1//sup 1/-hard. The question of deciding whether a given TCTL formula is implementable by a timed graph is also undecidable.>

A general method that represents the state space symbolically instead of explicitly is described. The generality of the method comes from using a dialect of the mu-calculus as the primary specification language. A model-checking algorithm for mu-calculus formulas which uses R.E. Bryant's (1986) binary decision diagrams to represent relations and formulas symbolically is described. It is then shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata. This eliminates the need to describe complicated graph-traversal or nested fixed-point computations for each decision procedure. The authors illustrate the practicality of their approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline.>

A state-machine verifier is described for speed-independent control circuits, using as an example an arbiter with reject. User-level behavioral descriptions are given as Petri nets, which are translated into trace structures, which are then automatically compared. The example verifies in two ways: first, the entire implementation is compared with a specification; second, the circuit is verified hierarchically according to the structure of the design. Performance figures are given.>

Asynchronous designs are of increasing interest because of the cost of broadcasting clocks over large areas of a chip. A tool for comparing implementations of speed-independent circuits with specifications is described. Petri nets are used throughout as a user-level description language. These are translated into trace structures, which can then be processed by an existing automatic verifier. This tool is applied to a nontrivial self-timed queue design.>

Verifying the correctness of sequential circuits has been an important problem for a long time. But lack of any formal and efficient method of verification has prevented the creation of practical design aids for this purpose. Since all the known techniques of simulation and prototype testing are time consuming and not very reliable, there is an acute need for such tools. In this paper we describe an automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, our system does not require any user assistance and is quite fast—experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds!