Modern SAT solvers are based on the conflict-driven clause learning (CDCL) paradigm, which can be simulated by the resolution proof system. This limits solver effectiveness on instances known to be hard for resolution. Certain approaches, such as parity reasoning, have been shown to be effective in this context, but are hard to integrate with CDCL, in particular, with mainstream proof certificates. The powerful yet simple Extended Resolution (ER) proof system provides an alternative but is not widely used in SAT solving despite having proof certificates for decades and using it effectively remains an open challenge. This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL. We further propose a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally. Previous work on bounded variable addition focused on AND gates and original clauses only. Our experimental evaluation shows substantial improvements on hard combinatorial benchmark families without performance degradation on the SAT Competition.

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision decomposable negation normal form (decision-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from decision-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

Abstract Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form. Cardinality constraints appear frequently in problem descriptions: over $$64\%$$ 64 % of the SAT Competition formulas contain at least one cardinality constraint, while over $$17\%$$ 17 % contain many large cardinality constraints. Allowing general cardinality constraints as input would simplify encodings and enable the solver to handle constraints natively or to encode them using different (and possibly dynamically changing) clausal forms. We modify the modern SAT solver CaDiCaL to handle cardinality constraints natively. Unlike the stronger cardinality reasoning in pseudo-Boolean (PB) or other systems, our incremental approach with cardinality-based propagation requires only moderate changes to a SAT solver, preserves the ability to run important inprocessing techniques, and is easily combined with existing proof-producing and validation tools. Our experimental evaluation on SAT Competition formulas shows our solver configurations with cardinality support consistently outperform other SAT and PB solvers.

Abstract The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven clause learning (CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solver SaDiCaL incorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We present PReLearn, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large portion of SAT competition benchmarks we found that preprocessing with PReLearn improves solver performance. In addition, there were several satisfiable and unsatisfiable formulas that could only be solved after preprocessing with PReLearn. PReLearn supports proof logging, giving a high level of confidence in the results. Lastly, we tested the robustness of PReLearn by applying other forms of preprocessing as well as by randomly permuting variable names in the formula before running PReLearn, and we found PReLearn performed similarly with and without the changes to the formula.

In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a BDD-based solver, implemented by extending an existing BDD package, to several challenging Boolean satisfiability problems. Our results demonstrate scaling for parity formulas as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers.

Abstract When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.

Abstract Augmenting problem variables in a quantified Boolean formula with definition variables enables a compact representation in clausal form. Generally these definition variables are placed in the innermost quantifier level. To restore some structural information, we introduce a preprocessing technique that moves definition variables to the quantifier level closest to the variables that define them. We express the movement in the QRAT proof system to allow verification by independent proof checkers. We evaluated definition variable movement on the QBFEVAL’20 competition benchmarks. Movement significantly improved performance for the competition’s top solvers. Combining variable movement with the preprocessorBloqqerimproves solver performance compared to usingBloqqeralone.

Abstract Existing proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false (refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single dual proof as it operates, supporting either outcome. This form consists of a sequence of equivalence-preserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.

Abstract In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in theextended resolutionlogical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such proofs indicate that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a prototype solver to obtain polynomially sized proofs on benchmarks for the mutilated chessboard and pigeonhole problems—ones that are very challenging for search-based SAT solvers.

The articles in this month’s special issue provide insight into future computing technologies such as novel architectures, spintronic memories, and quantum computing.

The future of computing is at crossroads. The technological advances that have sustained the exponential growth of computing performance over the last several decades are slowing and the roadmap for future advances is uncertain. The phenomenal expansion of computing power has made computers ubiquitous, spawned a $300 billion semiconductor industry, enabled unprecedented global economic growth, and transformed many aspects of society at large. Emerging technologies are placing an ever-growing and changing demand on computing, especially the profusion of data from the Internet of Things, large-scale scientific experiments (high-energy physics, astronomy, and genomics), autonomous vehicles, social media (including video), national security systems, and the finance sector. Transmitting, storing, processing, and analyzing this data explosion with the requisite speed and performance—and enabling significant processing and analysis to occur locally or at network nodes (i.e., edge computing)—may require a radical departure from the traditional computing paradigm of von Neumann computing architectures running on CMOS-based digital logic. New paradigms will likely require a range of new devices, software, design and simulation tools, and benchmarking, and may ultimately require rethinking the tasks that computing machines undertake. Recently, government, industry, and academia collectively have recognized that the future of computing requires a new, multidisciplinary research and development agenda.

This work describes our experience in revising one of the major programming assignments for the second-year course Introduction to Computer Systems, in which students implement a version of the malloc memory allocator. The revisions involved fully supporting a 64-bit address space, promoting a more modern programming style, and creating a set of benchmarks and grading standards that provide an appropriate level of challenge. With this revised assignment, students were able to implement more sophisticated allocators than they had in the past, and they also achieved higher performance on the related questions on the final exam.

Multithreaded programs are hard to get right. A key reason is that the contract between developers and runtimes grants exponentially many schedules to the runtimes. We present Parrot, a simple, practical runtime with a new contract to developers. By default, it orders thread synchronizations in the well-defined round-robin order, vastly reducing schedules to provide determinism (more precisely, deterministic synchronizations) and stability (i.e., robustness against input or code perturbations, a more useful property than determinism). When default schedules are slow, it allows developers to write intuitive performance hints in their code to switch or add schedules for speed. We believe this "meet in the middle" contract eases writing correct, efficient programs.

Abstraction plays a central role in formal verification. Term-level abstraction is a technique for abstracting word-level designs in a formal logic, wherein data is modeled with abstract terms, functional blocks with uninterpreted functions, and memories with a suitable theory of memories. A major challenge for any abstraction technique is to determine what components can be safely abstracted. We present an automatic technique for term-level abstraction of hardware designs, in the context of equivalence and refinement checking problems. Our approach is hybrid, involving a combination of random simulation and static analysis. We use random simulation to identify functional blocks that are suitable for abstraction with uninterpreted functions. Static analysis is then used to compute conditions under which such function abstraction is performed. The generated term-level abstractions are verified using techniques based on Boolean satisfiability (SAT) and satisfiability modulo theories (SMT). We demonstrate our approach for verifying processor designs, interface logic, and low-power designs. We present experimental evidence that our approach is efficient and that the resulting term-level models are easier to verify even when the abstracted designs generate larger SAT problems.

Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the first-order state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol.

The UCLID project seeks to develop formal verification tools for infinite-state systems having a degree of automation comparable to that of model checking tools for finite-state systems. The UCLID modeling language describes systems where the state variables are Booleans, integers, and functions mapping integers to integers or Booleans. The verifier supports several forms of verification for proving safety properties. They rely on a decision procedure that translates a quantifier-free formula into an equi-satisfiable Boolean formula and then applies a Boolean satisfiability solver. UCLID has successfully verified a number of hardware designs and protocols

We argue that finding vulnerabilities in software components is different from finding exploits against them. Exploits that compromise security often use several low-level details of the component, such as layouts of stack frames. Existing software analysis tools, while effective at identifying vulnerabilities, fail to model low-level details, and are hence unsuitable for exploit-finding.We study the issues involved in exploit-finding by considering application programming interface (API) level exploits. A software component is vulnerable to an API-level exploit if its security can be compromised by invoking a sequence of API operations allowed by the component. We present a framework to model low-level details of APIs, and develop an automatic technique based on bounded, infinite-state model checking to discover API-level exploits.We present two instantiations of this framework. We show that format-string exploits can be modeled as API-level exploits, and demonstrate our technique by finding exploits against vulnerabilities in widely-used software. We also use the framework to model a cryptographic-key management API (the IBM CCA) and demonstrate a tool that identifies a previously known exploit.

A malware detector is a system that attempts to determine whether a program has malicious intent. In order to evade detection, malware writers (hackers) frequently use obfuscation to morph malware. Malware detectors that use a pattern-matching approach (such as commercial virus scanners) are susceptible to obfuscations used by hackers. The fundamental deficiency in the pattern-matching approach to malware detection is that it is purely syntactic and ignores the semantics of instructions. In this paper, we present a malware-detection algorithm that addresses this deficiency by incorporating instruction semantics to detect malicious program traits. Experimental evaluation demonstrates that our malware-detection algorithm can detect variants of malware with a relatively low run-time overhead. Moreover our semantics-aware malware detection algorithm is resilient to common obfuscations used by hackers.

Given a formula in quantifier-free Presburger arithmetic, if it has a satisfying solution, there is one whose size, measured in bits, is polynomially bounded in the size of the formula. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints are difference (separation) constraints, and the non-difference constraints are sparse. This class has been observed to commonly occur in software verification. We derive a new solution bound in terms of parameters characterizing the sparseness of linear constraints and the number of non-difference constraints, in addition to traditional measures of formula size. In particular, we show that the number of bits needed per integer variable is linear in the number of non-difference constraints and logarithmic in the number and size of non-zero coefficients in them, but is otherwise independent of the total number of linear constraints in the formula. The derived bound can be used in a decision procedure based on instantiating integer variables over a finite domain and translating the input quantifier-free Presburger formula to an equi-satisfiable Boolean formula, which is then checked using a Boolean satisfiability solver. In addition to our main theoretical result, we discuss several optimizations for deriving tighter bounds in practice. Empirical evidence indicates that our decision procedure can greatly outperform other decision procedures.

This tutorial describes automatic techniques for formally verifying hardware and software by creating Boolean abstractions of the underlying unbounded system state variables.

Given a formula /spl Phi/ in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to /spl Phi/, there is one whose size, measured in bits, is polynomially bounded in the size of /spl Phi/. In this paper, we consider a special class of quantifier-free Presburger formulas in which most linear constraints are separation (difference-bound) constraints, and the nonseparation constraints are sparse. This class has been observed to commonly occur in software verification problems. We derive a solution bound in terms of parameters characterizing the sparseness of linear constraints and the number of nonseparation constraints, in addition to traditional measures of formula size. In particular, the number of bits needed per integer variable is linear in the number of nonseparation constraints and logarithmic in the number and size of nonzero coefficients in them, but is otherwise independent of the total number of linear constraints in the formula. The derived bound can be used in a decision procedure based on instantiating integer variables over a finite domain and translating the input quantifier-free Presburger formula to an equisatisfiable Boolean formula, which is then checked using a Boolean satisfiability solver. We present empirical evidence indicating that this method can greatly outperform other decision procedures.

Formal verification has had a significant impact on the semiconductor industry, particularly for companies that can devote significant resources to creating and deploying internally developed verification tools. Most existing verifiers model system operation at a detailed bit level. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is expressive enough to model a wide range of systems, but it still permits a decision procedure where we transform the formula into propositional logic and then use either binary decision diagrams (BDD) or a Boolean satisfiability (SAT) solver.

Binary Decision Diagrams (BDDs) often fail to exploit sharing between Boolean functions that differ only in their support variables. In a memory circuit, for example, the functions for the different bits of a word differ only in the data bit while the address decoding part of the function is identical. We present a symbolic representation approach using ordered function templates to exploit such regularity.Templates specify functionality without being bound to a specific set of variables. Functions are obtained by instantiating templates with a list of variables. We ensure canonicity of the representation by requiring that templates are normalized and argument lists are ordered. We also present algorithms for performing Boolean operations using this representation. Experiments with a prototype implementation built on top of CUDD indicate that function templates can dramatically reduce memory requirements for symbolic simulation of regular circuits.

SAT-based decision procedures for quantifier-free fragments of first-order logic have proved to be useful in formal verification. These decision procedures are either based on encoding atomic subformulas with Boolean variables, or by encoding integer variables as bit-vectors. Based on evaluating these two encoding methods on a diverse set of hardware and software benchmarks, we conclude that neither method is robust to variations in formula characteristics. We therefore propose a new hybrid technique that combines the two methods. We give experimental results showing that the hybrid method can significantly outperform either approach as well as other decision procedures.

We consider a variant of the Boolean satisfiability problem where a subset ε of the propositional variables appearing in formula F sat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, e i,j , for 1 ≤ i < j ≤ N , expresses whether or not the relation holds between elements i and j . The task is to either find a satisfying assignment to F sat that also satisfies all transitivity constraints over the relational variables (e.g., e 1,2 ∧ e 2,3 ⇒ e 1,3 ), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. This procedure forms the core of our tool for verifying pipelined microprocessors.To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing F sat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables.To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets ε, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of F sat , our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem.

The computation of logic-stage delays is a fundamental sub-problem for many EDA tasks. Although accurate delays can be obtained via circuit simulation, we must estimate the input assignments that will maximize the delay. With conventional methods, it is not feasible to estimate the delay for all input assignments on large sub-networks, so previous approaches have relied on heuristics. We present a symbolic algorithm that enables efficient computation of the Elmore delay under all input assignments and delay refinement using circuit-simulation. We analyze the Elmore estimate with three metrics using data extracted from symbolic timing simulations of industrial circuits. 1.

We compare SAT-checkers and decision diagrams on the evalua-tion of Boolean formulas produced in the formal verification of both correct and buggy versions of superscalar and VLIW micro-processors. We identify one SAT-checker that significantly out-performs the rest. We evaluate ways to enhance its performance by variations in the generation of the Boolean correctness formu-las. We reassess optimizations previously used to speed up the formal verification and probe future challenges.

We present a methodology for generating black-box timing models for full-custom transistor-level CMOS circuits. Our approach utilizes transistor-level ternary symbolic timing simulation to explore the input arrival time space and determine the input arrival time windows that result in proper operation. This approach integrates symbolic timing simulation into existing static timing analysis flows and allows automated modelling of the timing behavior of aggressive full-custom circuit design styles.

The course "Introduction to Computer Systems" at Carnegie Mellon University presents the underlying principles by which programs are executed on a computer. It provides broad coverage of processor operation, compilers, operating systems, and networking. Whereas most systems courses present material from the perspective of one who designs or implements part of the system, our course presents the view visible to application programmers. Students learn that, by understanding aspects of the underlying system, they can make their programs faster and more reliable. This approach provides immediate benefits for all computer science and engineering students and also prepares them for more advanced systems courses. We have taught our course for five semesters with enthusiastic responses by the students, the instructors, and the instructors of subsequent systems courses.

As manufacturing technology moves toward fundamental limits of silicon CMOS processing, the ability to reap the full potential of available transistors and interconnect is increasingly important. Design technology (DT) is concerned with the automated or semi-automated conception, synthesis, verification, and eventual testing of microelectronic systems. While manufacturing technology faces fundamental limits inherent in physical laws or material properties, design technology faces fundamental limitations inherent in the computational intractability of design optimizations and in the broad and unknown range of potential applications within various design processes. In this paper, we explore limitations to how design technology can enable the implementation of single-chip microelectronic systems that take full advantage of manufacturing technology with respect to such criteria as layout density performance, and power dissipation.

In this paper, we propose a new data structure called multiplicative power hybrid decision diagrams (*PHDDs) to provide a compact representation for functions that map Boolean vectors into integer or floating-point (FP) values. The size of the graph to represent the IEEE FP encoding is linear with the word size. The complexity of FP multiplication grows linearly with the word size. The complexity of FP addition grows exponentially with the size of the exponent part, but linearly with the size of the mantissa part. We applied *PHDDs to verify integer multipliers and FP multipliers before the rounding stage, based on a hierarchical verification approach. For integer multipliers, our results are at least six times faster than binary moment diagrams. Previous attempts at verifying FP multipliers required manual intervention, but we verified FP multipliers before the rounding stage automatically.

Symbolic switch-level simulation has been extensively applied to the functional verification of complementary metal-oxide-semiconductor (CMOS) circuitry. We have extended this technique to account for real-valued data-dependent delay values and have developed a novel mechanism for symbolically computing data-dependent Elmore delays. We present our symbolic simulation and delay calculation algorithms and discuss their application to the timing and functional verification of full-custom transistor-level CMOS circuitry.

The logic of Equality with Uninterpreted Functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. By reducing formulas in this logic to propositional formulas, we can apply Boolean methods such as ordered Binary Decision Diagrams (BDDs) and Boolean satisfiability checkers to perform the verification. We can exploit characteristics of the formulas describing the verification conditions to greatly simplfy the propostional formulas generated. We identify a class of terms we call “p-terms” for which equality comparisons can only be used in monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. A decision procedure can exploit the restricted uses of p-terms by considering only “maximally diverse” interpretations of the associated function symbols, where every function application yields a different value execept when constrainted by functional consistency. We present two methods to translate formulas in EUF into propositional logic. The first interprets the formula over a domain of fixed-length bit vectors and uses vectors of propositional variables to encode domain variables. The second generates formulas encoding the conditions under which pairs of terms have equal valuations, introducing propostional variables to encode the equality relations between pairs of terms. Both of these approaches can exploit maximal diversity to greatly reduce the number of propositional variables that need to be introduced and to reduce the overall formula sizes. We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. Exploiting positive equality allows us to overcome the experimental blow-up experienced previously when verifying microprocessors with load, store, and branch instructions.

We recently introduced symbolic timing simulation (STS) using data-dependent delays as a tool for verifying the timing of full-custom transistor-level circuit designs, and for the functional verification of delay-dependent logic. While STS leverages efficient symbolic encodings to yield huge gains over conventional simulation methodologies, it still suffers from a problem known as event multiplication. We discuss this problem and present an event-list management technique based on event-clusters, and a new simulator which utilizes this technique. Finally, we demonstrate substantial speedups on a wide range of test cases, including exponential improvement on a simple logic chain.

We extend the Burch and Dill flushing technique [6] for formal verification of microprocessors to be applicable to designs where the functional units and memories have multicycle and possibly arbitrary latency. We also show ways to incorporate exceptions and branch prediction by exploiting the properties of the logic of Positive Equality with Uninterpreted Functions [4][5]. We study the modeling of the above features in different versions of dual-issue superscalar processors.

We study the applicability of the logic of Positive Equality with Uninterpreted Functions (PEUF) [2][3] to the verification of pipelined microprocessors with very large Instruction Set Architectures (ISAs). Abstraction of memory arrays and functional units is employed, while the control logic of the processors is kept intact from the original gate-level designs. PEUF is an extension of the logic of Equality with Uninterpreted Functions, introduced by Burch and Dill [4], that allows us to use distinct constants for the data operands and instruction addresses needed in the symbolic expression for the correctness criterion.We present several techniques that make PEUF scale very efficiently for the verification of pipelined microprocessors with large ISAs.These techniques are based on allowing a limited form of non-consistency in the uninterpreted functions, representing initial memory state and ALU behaviors.Our tool required less than 30 seconds of CPU time and 5 MB of memory to verify a 5-stage MIPS-like pipelined processor that implements 191 instructions of various classes.The verification was done by correspondence checking -a formal method, where a pipelined microprocessor is compared against a non-pipelined specification.

We introduce a new method of verifying the timing of custom CMOS circuits. Due to the exponential number of patterns required, traditional simulation methods are unable to exhaustively verify a medium-sized modern logic block. Static analysis can handle much larger circuits but is not robust with respect to variations from standard circuit structures. Our approach applies symbolic simulation to analyze a circuit over all input combinations without these limitations. We present a prototype simulator (SirSim) and experimental results. We also discuss using SirSim to verify an industrial design which previously required a special-purpose verification methodology.

We describe the use of symmetry for verification of transistor-level circuits by symbolic trajectory evaluation (STE). We present a new formulation of STE which allows a succinct description of symmetry properties in circuits, Symmetries in circuits are classified as structural symmetries, arising from similarities in circuit structure, data symmetries, arising from similarities in the handling of data values, and mixed structural-data symmetries. We use graph isomorphism testing and symbolic simulation to verify the symmetries in the original circuit, Using conservative approximations, we partition a circuit to expose the symmetries in its components, and construct reduced system models which can be verified efficiently, Introducing X-drivers into switch-level circuits simplifies the task of creating conservative approximations of switch-level circuits, Our empirical results show that exploiting symmetry with conservative approximations can allow one to verify systems several orders of magnitude larger than otherwise possible. We present results of verifying static random access memory circuits with up to 1.5 Million transistors,.

Binary decision diagrams (BDDs) have been shown to be a powerful tool in formal verification. Efficient BDD construction techniques become more important as the complexity of protocol and circuit designs increases. This paper addresses this issue by introducing three techniques based on working set control. First, we introduce a novel BDD construction algorithm based on partial breadth-first expansion. This approach has the good memory locality of the breadth-first BDD construction while maintaining the low memory overhead of the depth-first approach. Second, we describe how memory management on a per-variable basis can improve spatial locality of BDD construction at all levels, including expansion, reduction, and rehashing. Finally, we introduce a memory compacting garbage collection algorithm to remove unreachable BDD nodes and minimize memory fragmentation. Experimental results show that when the applications fit in physical memory, our approach has speedups of up to 1.6 in comparison to both depth-first (CUDD) and breadth-first (GAL) packages. When the applications do not fit into physical memory, our approach outperforms both CUDD and CAL by up to an order of magnitude. Furthermore, the good memory locality and low memory overhead of this approach has enabled us to be the first to have successfully constructed the entire C6288 multiplication circuit from the ISCAS85 benchmark set using only conventional BDD representations.

Formal Verification is a “hot topic” for the user and vendor community. It has moved from the research community to the industrial domain in a very short time. Everyone wants to know more about how effective the techniques are. This experienced user panel will attempt to address your concerns in an open and frank way. They will give their personal opinions and not the commercial hype that so often heralds a new era.

This paper introduces the four timing constraints of setup time, hold time, minimum delay, and maximum delay in the efficient memory model (EMM). The EMM is a behavioral model, where the number of symbolic variables used to characterize the initial state of the memory is proportional to the number of distinct symbolic memory locations accessed. The behavioral model provides a conservative approximation of the replaced memory array, while allowing the address and control inputs of the memory to accept symbolic ternary values. If a circuit has been formally verified with the behavioral model, the system is guaranteed to function correctly with any memory implementation whose timing parameters are bounded by the ones used in the verification.

. Many modern systems are designed as a set of interconnected reactive subsystems. The subsystem verification task is to verify an implementation of the subsystem against the simple deterministic high-level specification of the entire system. Our verification methodology, based on Symbolic Trajectory Evaluation, is able to bridge the wide gap between the abstract specification and the implementation specific details of the subsystem. This paper presents a detailed description of an industrial application of this methodology to the fixed point execution unit of the PowerPC processor. We were able to verify a representative instruction under all possible stall, bypass, pipeline conditions and under all possible timings for interface to other functional units in the processor. 1. Introduction Some modern systems with a simple deterministic high-level specification have implementations that exhibit highly nondeterministic behaviors. A large class of systems that exhibit such...

In this paper we report on new techniques for verifying contentaddressable memories (CAMs), and demonstrate that these techniqueswork well for large industrial designs. It was shown in [Formal verification of PowerPC(TM) arrays using symbolic trajectory evaluation], that theformal verification technique of symbolic trajectory evaluation (STE)could be used successfully on memory arrays. We have extended thatwork to verify what are perhaps the most combinatorially difficultclass of memory arrays, CAMs. We use new Boolean encodings toverify CAMs, and show that these techniques scale well, in that spacerequirements increase linearly, or sub-linearly, with the various CAMsize parameters.In this paper, we describe the verification of two CAMs froma recentPowerPC microprocessor design, a Block Address Translation unit(BAT), and a Branch Target Address Cache unit (BTAC). The BATis a complex CAM, with variable length bit masks. The BTAC is a64-entry, 64-bits per entry, fully associative CAM and is part of thespeculative instruction fetch mechanism of the microprocessor. Webelieve that ours is the first work on formally verifying CAMs, and webelieve our techniques make it feasible to efficiently verify the varietyof CAMs found on modern processors.

Data structures such as *BMDs, HDDs, and K*BMDs provide compact representations for functions which map Boolean vectors into integer values, but not floating point values. We propose a new data structure, called Multiplicative Power Hybrid Decision Diagrams (*PHDDs), to provide a compact representation for functions that map Boolean vectors into integer or floating point values. The size of the graph to represent the IEEE floating point encoding is linear with the word size. The complexity of floating point multiplication grows linearly with the word size. The complexity of floating point addition grows exponentially with the size of the exponent part, but linearly with the size of the mantissa part. We applied *PHDDs to verify integer multipliers and floating point multipliers before the rounding stage, based on a hierarchical verification approach. For integer multipliers, our results are at least 6 times faster than *BMDs. Previous attempts at verifying floating point multipliers required manual intervention. We verified floating point multipliers before the rounding stage automatically.

It is impractical to verify multiplier or divider circuits entirely at the bit-level using ordered Binary Decision Diagrams (BDDs), because the BDD representations for these functions grow exponentially with the word size.It is possible, however, to analyze individual stages of these circuits using BDDs.Such analysis can be helpful when implementing complex arithmetic algorithms.As a demonstration, we show that Intel could have used BDDs to detect erroneous lookup table entries in the Pentium(TM) floating point divider.Going beyond verification, we show that bit-level analysis can be used to generate a correct version of the table.'0101.011 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 '0101.0102,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2,1,0 2

Verifying memory arrays such as on-chip caches and register files is a difficult part of designing a microprocessor.Current tools cannot verify the equivalence of the arrays to their behavioral or RTL models, nor their correct functioning at the transistor level.It is infeasible to run the number of simulation cycles required, and most formal verification tools break down due to the enormous number of state-holding elements in the arrays.The formal method of symbolic trajectory evaluation (STE) appears to offer a solution, however.STE verifies that a circuit satisfies a formula in a carefully restricted temporal logic.For arrays, it requires only a number of variables approximately logarithmic in the number of memory locations.The circuit is modeled at the switch level, so the verification is done on the actual design.We have used STE to verify two arrays from PowerPC microprocessors: a register file, and a data cache tag unit.The tag unit contains over 12,000 latches.We believe it is the largest circuit to have been formally verified, without abstracting away significant detail, in the industry.We also describe an automated technique for identifying state-holding elements in the arrays, a technique which should greatly assist the widespread application of STE.

Based on a hierarchical verification methodology, we present an arithmetic circuit verifier ACV, in which circuits expressed in a hardware description language, also called ACV, are symbolically verified using binary decision diagrams for Boolean functions and multiplicative binary moment diagrams (BMDs) for word-level functions. A circuit is described in ACV as a hierarchy of modules. Each module has a structural definition as an interconnection of logic gates and other modules. Modules may also have functional descriptions, declaring the numeric encodings of the inputs and outputs, as well as specifying their functionality in terms of arithmetic expressions. Verification then proceeds recursively, proving that each module in the hierarchy having a functional description, including the top-level one, realizes its specification. The language and the verifier contain additional enhancements for overcoming some of the difficulties in applying BMD-based verification to circuits computing functions such as division and square root. ACV has successfully verified a number of circuits, implementing such functions as multiplication, division, and square root, with word sizes up to 256 bits.

Binary Moment Diagrams (BMDs) provide a canonical representations for linear functions similar to the way Binary Decision Diagrams (BDDs) represent Boolean functions. Within the class of linear functions, we can embed arbitrary functions from Boolean variables to integer values. BMDs can thus model the functionality of data path circuits operating over word-leveldata. Many important functions, including integer multiplication, that cannot be represented efficiently at the bit level with BDDs have simple representations at the word level with BMDs. Furthermore,BMDs can represent Boolean functions with around the same complexity as BDDs.\nWe propose a hierarchical approach to verifying arithmetic circuits, where component modulesare firstshownto implement their word-level specifications. The overall circuit functionality is thenverified by composing the component functions and comparing the result to the word-level circuit specification. Multipliers with word sizes of up to 256 bits have been verified by this technique.

Our goal is to transform a low-level circuit design into a more abstract representation. This is done in two stages. Tranalyze, an existing analysis tool, takes a switch-level circuit and generates a functionally equivalent gate-level representation. The thesis focuses on the second stage, which takes a gate-level sequential circuit and performs a temporal analysis that abstracts the clocks from

Ordered Binary Decision Diagrams (OBDDs) have found widespread use in CAD applications such as formal verification, logic synthesis, and test generation. OBDDs represent Boolean functions in a form that is both canonical and compact for many practical cases. They can be generated and manipulated by efficient graph algorithms. Researchers have found that many tasks can be expressed as series of operations on Boolean functions, making them candidates for OBDD-based methods. The success of OBDDs has inspired efforts to improve their efficiency and to expand their range of applicability. Techniques have been discovered to make the representation more compact and to represent other classes of functions. This has led to improved performance on existing OBDD applications, as well as enabled new classes of problems to be solved. This paper provides an overview of the state of the art in graph-based function representations. We focus on several recent advances of particular importance for formal verification and other CAD applications.

The paper describes a new technique for extracting clock level finite state machines (FSMs) from transistor netlists using symbolic simulation. The transistor netlist is preprocessed to produce a gate level representation of the netlist. Given specifications of the circuit clocking and input and output timing, simulation patterns are derived for a symbolic simulator. The result of the symbolic simulation and extraction process is the next state and output function of the equivalent FSM, represented as Ordered Binary Decision Diagrams. Compared to previous techniques, our extraction process yields an order of magnitude improvement in both space and time, is fully automated and can handle static storage structures and time multiplexed inputs and outputs

Formal verification is becoming a useful means of validating designs. We have developed a methodology for formally verifying dataintensive circuits (e.g., processors) with sophisticated timing (e.g., pipelining) against high-level declarative specifications. Previously, formally verifying a microprocessor required the use of an automatic theorem prover, but our technique requires little more than a symbolic simulator. We have formally verified a pre-existing 16-bit CISC microprocessor circuit extracted from the fabricated layout. Introduction Previously, symbolic switch-level simulation has been used to verify some small or simple data-intensive circuits (RAMs, stacks, register files, ALUs, and simple pipelines) [2, 3]. In doing so, the necessary simulation patterns were developed by hand or by using ad-hoc techniques, and it was then argued that the patterns were sufficient, and that their generation could be automated. We have developed sufficient theory to fully support such claims...

We look at the problem of inverter minimization in multi-level logic networks. The network is specified in terms of a set of base functions and the inversion operation. The library is specified as a set of allowed permutations of phase assignments on each base function. Traditional approaches to this problem have been limited to greedy heuristics based on local information. Our approach takes a more global view and maps the problem of inverter minimization into a problem of removing a minimum of vertices from a graph, so as to make the remaining graph two-colorable. This approach has the flexibility of capturing a variety of design-specific features that are relevant to the problem of inverter minimization. Although, in general the problem is NP-complete, we have developed several good heuristic and branch and bound search techniques.

Symbolic representations of systems can achieve a high degree of compaction relative to more explicit forms. By casting and analysis task in terms of operations on a symbolic representation, large and complex systems can be analyzed efficiently. This paper summarizes research in applying symbolic analysis methods to systems at several levels of abstraction.>

Parallel hashing is well-known in the folklore of parallel computing, but there has been a remarkable dearth of literature describing it in detail. Because many parallel algorithms such as histogramming, set intersection and dictionary lookup can make use of hashing as a core step, hashing is a fundamental parallel operation. This paper sheds light on the performance that may be achieved using parallel hashing algorithms and should lend credibility to their use.

The linear switch-level model represents a MOS transistor as a voltage-controlled linear resistor and a storage node as a grounded, linear capacitor. For logic simulation, the linear switch-level model offers an attractive tradeoff between resolution/accuracy and computational complexity over gate-level and circuit-level models. However, analysis of MOS networks using the linear switch-level model becomes increasingly difficult in the presence of unknown values, and heuristic methods are often employed. It is shown that the complexity of computing maximum and minimum steady-state voltages of a general MOS network using the linear switch-level model in the presence of unknown values is NP-complete. These results partially justify the use of heuristic methods when unknown values are present.>

Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers.We have created such an evaluator by extending the symbolic switch-level simulator COSMOS.This program gains added efficiency by exploiting the ability of COSMOS to evaluate circuit operation over a ternary logic model, where the third value X represents an unknown logic value.This program can formally verify systems containing complex featurea such as switch-level models, detailed timing, and pipelining.

In this paper, we present a framework for performing switchlevel simulation on hardware accelerators.A symbolic analyzer preprocesses the MOS network into a functionally equivalent Boolean representation.The analyzer thus converts switch-level simulation into a task of evaluating Boolean expressions.Our approach maps the Boolean representation into the instruction set of the hardware accelerator.The resultant framework supports switch level simulation on a class of hardware accelerators that traditionally have been limited to gate-level simulation.1.

The program TRANALYZE generates a gate-level representation of an MOS transistor circuit. The results model contains only four-valued unit and zero delay logic primitives, suitable for evaluation by conventional gate-level simulators and hardware simulation accelerators. TRANALYZE has the same generality and accuracy as switch-level simulation, generating models for a wide range of technologies and design styles, while expressing the detailed effects of bidirectional transistors, stored charge, and multiple signal strengths. It produces models with size comparable to ones generated by hand.>

A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits fulfilling the system specification will produce a particular response to a sequence of simulation commands.This style of verification has advantages over the other proof methods in being readily automated and requiring less attention on the part of the user to the low-level details of the design. It has advantages over other approaches to simulation in providing more reliable results, often at a comparable cost. This paper presents the theoretical foundations of several related approaches to circuit verification based on logic simulation. These approaches exploit the three-valued modeling capability found in most logic simulators, where the third-value X indicates a signal with unknown digital value. Although the circuit verification problem is NP-hard as measured in the size of the circuit description, several techniques can reduce the simulation complexity to a manageable level for many practical circuits.

Lower-bound results on Boolean-function complexity under two different models are discussed. The first is an abstraction of tradeoffs between chip area and speed in very-large-scale-integrated (VLSI) circuits. The second is the ordered binary decision diagram (OBDD) representation used as a data structure for symbolically representing and manipulating Boolean functions. The lower bounds demonstrate the fundamental limitations of VLSI as an implementation medium, and that of the OBDD as a data structure. It is shown that the same technique used to prove that any VLSI implementation of a single output Boolean function has area-time complexity AT/sup 2/= Omega (n/sup 2/) also proves that any OBDD representation of the function has Omega (c/sup n/) vertices for some c>1 but that the converse is not true. An integer multiplier for word size n with outputs numbered 0 (least significant) through 2n-1 (most significant) is described. For the Boolean function representing either output i-1 or output 2n-i-1, where 1>

An N-bit RAM can be verified by simulating just O(N log N) patterns. This approach to verification is fast, requires minimal attention on the part of the user to the circuit details, and can utilize more sophisticated circuit models than other approaches to formal verification. The technique has been applied to a CMOS static RAM design using the COSMOS switch-level simulator. By simulating many patterns in parallel, a massively parallel computer can verify a 4K RAM in under 6 min.>

The feasibility of mapping the COSMOS switch-level simulator onto a computer with thousands of simple processors is addressed. COSMOS preprocesses transistor networks into Boolean behavioral models, capturing the switch-level behavior of a circuit in a set of Boolean formulas. A class of massively parallel computers and a mapping of COSMOS onto these computers are described. The factors affecting the performance of such a massively parallel simulator are discussed, including: the amount of parallelism in the simulation model, performance measures for massively parallel machines, and the impact of event scheduling on simulator performance. Compilation tools that automatically map a MOS circuit onto a massively parallel computer have been developed. Techniques for restructuring Boolean expressions for greater parallelism and mapping Boolean expressions for evaluation on massively parallel machines are described. Massively parallel switch-level simulation is illustrated by a pilot implementation on a 32k-processor Thinking Machines Connection Machine system.>

Efficient manipulation of Boolean functions is an important component of many computer-aided design tasks. This paper describes a package for manipulating Boolean functions based on the reduced, ordered, binary decision diagram (ROBDD) representation. The package is based on an efficient implementation of the if-then-else (ITE) operator. A hash table is used to maintain a strong canonical form in the ROBDD, and memory use is improved by merging the hash table and the ROBDD into a hybrid data structure. A memory function for the recursive ITE algorithm is implemented using a hash-based cache to decrease memory use. Memory function efficiency is improved by using rules that detect when equivalent functions are computed. The usefulness of the package is enhanced by an automatic and low-cost scheme for recycling memory. Experimental results are given to demonstrate why various implementation trade-offs were made. These results indicate that the package described here is significantly faster and more memory-efficient than other ROBDD implementations described in the literature.

Symbolic simulation involves evaluating circuit behavior using special symbolic values to encode a range of circuit operating conditions. In one simulation run, a symbolic simulator can compute what would require many runs of a traditional simulator. Symbolic simulation has applications in both logic and timing verification, as well as sequential test generation.

The COSMOS symbolic fault simulator generates test sets for combinational and sequential MOS circuits represented at the switch level. All aspects of switch-level networks including bidirectional transistors, stored charge, different signal strengths, and indeterminate (X) logic values are captured. To generate tests for a circuit, the program derives Boolean functions representing the behavior of the good and faulty circuits over a sequence of symbolic input patterns. It then determines a set of assignments to the input variables that will detect all faults. Symbolic simulation provides a natural framework for the user to supply an overall test strategy, letting the program determine the detailed conditions to detect a set of faults. Symbolic preprocessing of switch-level networks, combined with efficient Boolean manipulation makes this approach feasible.

This work addresses the feasibility of mapping the COSMOS switch-level simulator onto a computer with thousands of simple processors. COSMOS preprocesses transistor networks into Boolean behavioral models, capturing the switch-level behavior of a circuit in a set of Boolean formulas. We describe a class of massively parallel computers and a mapping of COSMOS onto these computers. We discuss the factors affecting the performance of such a massively parallel simulator including: the amount of parallelism in the simulation model, performance measures for massively parallel machines, and the impact of event scheduling on simulator performance. We have developed compilation tools which automatically map a MOS circuit onto a massively parallel computer. Massively parallel switch-level simulation is illustrated by describing our pilot implementation on a 32k processor Thinking Machines Connection Machine System.

This work examines the mapping of logic simulation onto massively parallel computer architectures. We discuss alternative communication primitives for a massively parallel instruction set architecture and the impact of the choice of communication primitives on logic simulation. We have developed compilation tools to automatically map the simulation of an MOS transistor circuit onto a massively parallel computer. We analyze the efficiency of this mapping as a function of the available communication primitives. The compilation process is illustrated by describing our pilot implementation on a 32k processor Connection Machine.

Data-parallel simulation involves simulating the behavior of a circuit over a number of test sequences simultaneously. Compared to other parallel simulation techniques, data-parallel simulation requires less overhead for synchronization and communication, and it permits higher degrees of parallelism. Two data-parallel versions of the switch-level simulator COSMOS have been implemented. The first runs on conventional machines, exploiting the bit parallelism of machine-level logic operations. This version runs 20-30 times faster than sequential simulation on the same machine. The second runs on a massively parallel SIMD machine, with each processor simulating the circuit behavior for a single test sequence. A simulator running on a 32768-processor machine runs up to 33000 times faster than a sequential simulator on a workstation computer.>

The COSMOS simulator provides fast and accurate switch-level modeling of MOS digital circuits. It attains high performance by preprocessing the transistor network into a functionally equivalent Boolean representation. This description, produced by the symbolic analyzer ANAMOS, captures all aspects of switch-level networks including bidirectional transistors, stored charge, different signal strengths, and indeterminate (X) logic values. The LGCC program translates the Boolean representation into a set of machine language evaluation procedures and initialized data structures. These procedures and data structures are compiled along with code implementing the simulation kernel and user interface to produce the simulation program. The simulation program runs an order of magnitude faster than our previous simulator MOSSIM II.

A network of switches controlled by Boolean variables can be represented as a system of Boolean equations. The solution of this system gives a symbolic description of the conducting paths in the network. Gaussian elimination provides an efficient technique for solving sparse systems of Boolean equations. For the class of networks that arise when analyzing digital metal-oxide semiconductor (MOS) circuits, a simple pivot selection rule guarantees that most s-switch networks encountered in practice can be solved with O(s) operations. When represented by a directed acyclic graph, the set of Boolean formulas generated by the analysis has total size bounded by the number of operations required by the Gaussian elimination. This paper presents the mathematical basis for systems of Boolean equations, their solution by Gaussian elimination, and data structures and algorithms for representing and manipulating Boolean formulas.

The switch-level model represents a digital metal-oxide semiconductor (MOS) circuit as a network of charge storage nodes connected by resistive transistor switches. The functionality of such a network can be expressed as a series of systems of Boolean equations. Solving these equations symbolically yields a set of Boolean formulas that describe the mapping from input and current state to the new network states. This analysis supports the same class of networks as the switch-level simulator MOSSIM II and provides the same functionality, including the handling of bidirectional effects and indeterminate (X) logic values. In the worst case, the analysis of an n-node network can yield a set of formulas containing a total of O(n /sup 3/) operations. However, all but a limited set of dense, pass-transistor networks give formulas with O(n) total operations. The analysis can serve as the basis of efficient programs for a variety of logic design tasks, including logic simulation (on both conventional and special-purpose computers), fault simulation, test generation, and symbolic verification.

In this paper we present a new data structure for representing Boolean functions and an associated set of manipulation algorithms. Functions are represented by directed, acyclic graphs in a manner similar to the representations introduced by Lee [1] and Akers [2], but with further restrictions on the ordering of decision variables in the graph. Although a function requires, in the worst case, a graph of size exponential in the number of arguments, many of the functions encountered in typical applications have a more reasonable representation. Our algorithms have time complexity proportional to the sizes of the graphs being operated on, and hence are quite efficient as long as the graphs do not grow too large. We present experimental results from applying these algorithms to problems in logic design verification that demonstrate the practicality of our approach.

Binary decision diagrams provide a data structure for representing and manipulating Boolean functions in symbolic form.They have been especially effective as the algorithmic basis for symbolic model checkers.A binary decision diagram represents a Boolean function as a directed acyclic graph, corresponding to a compressed form of decision tree.Most commonly, an ordering constraint is imposed among the occurrences of decision variables in the graph, yielding ordered binary decision diagrams (OBDD).Representing all functions as OBDDs with a common variable ordering has the advantages that (1) there is a unique, reduced representation of any function, (2) there is a simple algorithm to reduce any OBDD to the unique form for that function, and (3) there is an associated set of algorithms to implement a wide variety of operations on Boolean functions represented as OB-DDs.Recent work in this area has focused on generalizations to represent larger classes of functions, as well on scaling implementations to handle larger and more complex problems.

This paper presents measurements obtained while performing fault simulations of MOS circuits modeled at the switch level.In

The Mossim Simulation Engine (MSE) is a hardware accelerator for performing switch-level simulation of MOS VLSI circuits [1], [2]. Functional partitioning of the MOSSIM algorithm and specialized circuitry are used by the MSE to achieve a performance improvement of /spl gt/ 300 over a VAX 11/780 executing the MOSSIM II program. Several MSE processors can be connected in parallel to achieve additional speedup. A virtual processor mechanism allows the MSE to simulate large circuits with the size of the circuit limited only by the amount of backing store available to hold the circuit description.

The switch-level model describes the logical behavior of digital systems implemented in metal oxide semiconductor (MOS) technology. In this model a network consists of a set of nodes connected by transistor "switches" with each node having a state 0, 1, or X (for invalid or uninitialized), and each transistor having a state "open," "closed," or "indeterminate." Many characteristics of MOS circuits can be modeled accurately, including: ratioed, complementary, and precharged logic; dynamic and static storage; (bidirectional) pass transistors; buses; charge sharing; and sneak paths. In this paper we present a formal development of the switch-level model starting from a description of circuit behavior in terms of switch graphs. Then we describe an algorithm for a logic simulator based on the switch-level model which computes the new state of the network by solving a set of equations in a simple, discrete algebra. This algorithm has been implemented in the simulator MOSSIM II and operates at speeds approaching those of conventional logic gate simulators. By developing a formal theory of MOS logic circuits, we have achieved a greater degree of generality and accuracy than is found in other logic simulators for MOS.