Geometric Characterization of Series-Parallel Variable Resistor Networks ∗ (2009)
Abstract—The range of operating conditions for a seriesparallel network of variable linear resistors, voltage sources, and current sources can be represented as a convex polygon in a Thevenin or...
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
We consider the satisfiability problem for Boolean combinations of unit two variable per inequality (UTVPI) constraints. A UTVPI constraint is a linear constraint containing at most two variables...
Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant
Symbolic non-deterministic planning represents action effects as sets of possible next states. In this paper, we move toward a more probabilistic uncertainty model by distinguishing between likely...
"PHDD: An Efficient Graph Representation for Floating Point Circuit Verification t (2008)
Yimg-an Chen, Randal E. Bryant
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. In this pape,: we propose a...
Abstract Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation* (2008)
Randal E. Bryant, Derek L. Beatty
Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabil-ities of symbolic logic simulation with some of the analytic methods found in...
Predicate Abstraction with Indexed Predicates SHUVENDU (2008)
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...
Formal Verification of Infinite State Systems Using Boolean Methods ⋆ (2008)
Most successful automated formal verification tools are based on a bit-level model of computation, where a set of Boolean state variables encodes the system state. Using powerful inference engines,...
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
We consider the satisfiability problem for Boolean combinations of unit two variable per inequality (UTVPI) constraints. A UTVPI constraint is linear constraint containing at most two variables with...
Predicate abstraction with indexed predicates (2008)
Shuvendu K. Lahiri, Randal E. Bryant
Reasoning about Programs—Invariants
Abstract Digital Circuit Verification using Partially-Ordered State Models (2008)
Many aspects of digital circuit operation can be efficiently verified by simulating circuit operation over “weakened ” state values. This technique has long been practiced with logic simulators,...
Data-Intensive Supercomputing:The case for DISC (2008)
When a teenage boy wants to find information about his idol by using Googlewith the search query "Britney Spears, " he unleashes the power of several hundred processors operating on...
Abstract Formal verification of PowerPC TM arrays using symbolic trajectory evaluation (2008)
Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant
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...
System Modeling and Verification with UCLID (2008)
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...
Efficient Modeling of MemoryArrays in Symbolic Simulation 1 (2008)
Miroslav N. Velev, Randal E. Bryant
Abstract. This paper enables symbolic simulation of systems with large embedded memories. Each memory array is replaced with a behavioral model, where the number of symbolic variables used to...
To appear at ASYNC’05 Modeling and Verifying Circuits Using Generalized Relative Timing (2008)
Sanjit A. Seshia, Randal E. Bryant
We propose a novel technique for modeling and verifying timed circuits based on the notion of generalized relative timing. Generalized relative timing constraints can express not just a relative...
Abstract Introducing Computer Systems from a Programmer’s Perspective (2008)
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...
Symbolic Verification of MOS Circuits 1 (2008)
The program MOSSYM simulates the behavior of a MOS circuit represented as a switch-level network symbolically. That is, during simulator operation the user can set an input to either 0, 1, or a...
Formal Verification of Infinite State Systems Using Boolean Methods ∗ (2008)
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 finitestate systems. The UCLID...
x86-64 Machine-Level Programming ∗ (2008)
Randal E. Bryant, David R. O’hallaron
Intel’s IA32 instruction set architecture (ISA), colloquially known as “x86”, is the dominant instruction format for the world’s computers. IA32 is the platform of choice for most Windows and...
x86-64 Machine-Level Programming ∗ (2008)
Randal E. Bryant, David R. O’hallaron
Intel’s IA32 instruction set architecture (ISA), colloquially known as “x86”, is the dominant instruction format for the world’s computers. IA32 is the platform of choice for most Windows,...
Alpha Assembly Language Guide (2007)
Randal Bryant Carnegie, Randal E. Bryant
This document provides an overview of the Alpha instruction set and assembly language programming conventions. The Alpha architecture was formulated by Digital Equipment Corporation as a second...
Alpha Assembly Language Guide (2007)
Randal Bryant Carnegie, Randal E. Bryant
This document provides an overview of the Alpha instruction set and assembly language programming conventions. The Alpha architecture was formulated by Digital Equipment Corporation as a second...
-740 Basic Computer Systems Fall 1997 Syllabus (2007)
Electronic Connections Much, Randal E. Bryant, Bruce M. Maggs, Joan Maddamma
with TCP/IP Volume 1: Principles, Protocols, and Architecture, Prentice-Hall, 1995. This is a new edition. There should be reference copies in the E&S Library by the time we need them. Non-CS...
Geometric Characterization of Series-Parallel Variable Resistor Networks # (2007)
Randal E. Bryant, J. D. Tygar, Lawrence P. Huang
The range of operating conditions for a series-parallel network of variable linear resistors, voltage sources, and current sources can be represented as a convex polygon in a Thevenin or Norton...
Reducing separation formulas to propositional logic (2007)
Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
We show a reduction to propositional logic from a Boolean combination of inequalities of the form v i v j + c and v i> v j + c, where c is a constant and v i; v j are variables of type real or...
Randal E. Bryant, David R. O'hallaron
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...
Geometric Characterization of Series-Parallel Variable Resistor Networks # (2007)
Randal E. Bryant, J. D. Tygar, Lawrence P. Huang
Abstract---The range of operating conditions for a seriesparallel network of variable linear resistors, voltage sources, and current sources can be represented as a convex polygon in a Thevenin or...
Symbolic Verification of MOS Circuits 1 (2007)
The program MOSSYM simulates the behavior of a MOS circuit represented as a switch-level network symbolically. That is, during simulator operation the user can set an input to either 0, 1, or a...
Abstract Introducing Computer Systems from a Programmer’s Perspective (2007)
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...
Miroslav N. Velev, Randal E. Bryant
is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or...
Comparing Techniques for Out-of-Order Processor Verification in UCLID (2007)
Shuvendu K. Lahiri, Sanjit A. Seshia, Randal E. Bryant, Al E. Bryant
In this paper, we show the verification of out-of-order processors in a tool called UCLID. The processor is modeled using the Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted...
Effective Use of Boolean Satisfiability Procedures in the Formal Verification (2007)
Of Superscalar And, Miroslav N. Velev, Randal E. Bryant
We compare SAT-checkers and decision diagrams on the evaluation of Boolean formulas produced in the formal verification of both correct and buggy versions of superscalar and VLIW microprocessors. We...
1 CMOS Circuit Verification with Symbolic Switch-Level Timing Simulation (2007)
Clayton B. Mcdonald, Randal E. Bryant
Symbolic switch-level simulation has been extensively applied to the functional verification of CMOS circuitry. We have extended this technique to account for real-valued, data-dependent delay...
Amit Goel, Gagan Hasteer, Randal E. Bryant
Binary Decision Diagrams (BDDs) often fail to exploit sharing between Boolean functions that di#er only in their support variables. In a memory circuit, for example, the functions for the di#erent...
Miroslav N. Velev, Randal E. Bryant
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...
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it...
1 Formal Verification of a Superscalar Execution Unit (2007)
Kyle L. Nelson, Alok Jain, Randal E. Bryant
Abstract. 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...
1 Formal Verification of an ARM processor (2007)
Vishnu A. Patankar, Alok Jain, Randal E. Bryant
This paper presents a detailed description of the application of a formal verification methodology to an ARM processor. The processor, a hybrid between the ARM7 and the StrongARM processors, uses...
Formal Methods for Functional Verification (2007)
Randal E. Bryant, James H. Kukula
Formal hardware verification ranges from proving that two combinational circuits compute the same functions to the much more ambitious task of proving that a sequential circuit obeys some abstract...
On Solving Boolean Combinations of Generalized 2SAT Constraints (2007)
Seshia, Sanjit A., Subramani, K., Bryant, Randal E.
We consider the satisfiability problem for Boolean combinations of generalized 2 SAT constraints, which are linear constraints with at most two, possibly unbounded, integer variables having...
A Boolean Approach to Unbounded, Fully Symbolic Model Checking of Timed Automata (2007)
Seshia, Sanjit A., Bryant, Randal E.
We present a new approach to unbounded, fully symbolic model checking of timed automata that is based on an efficient translation of quantified separation logic to quantified Boolean logic. Our...
Data-Intensive Supercomputing: The Case for DISC (2007)
Google and its competitors have created a new class of large-scale computer systems to support Internet search. These “Data-Intensive Super Computing ” (DISC) systems differ from conventional...
Model Checking, Abstraction, and Compositional Verification (2006)
Long, David E., Clarke, Edmund M., Bryant, Randal E., Brookes, Stephen D., Grumberg, Orna
Because of the difficulty of adequately simulating large digital designs, there has been a recent surge of interest in formal verification, in which a mathematical model of the design is proved to...
A Methodology for Formal Hardware Verification, with Application to Microprocessors. (2006)
Beatty, Derek L., Bryant, Randal E., Fisher, Allan L., Seger, Carl-Johan H.
Microprocessors are now ubiquitous, but their design is not without difficulties. Numerous microprocessors have been introduced only to find- sometimes years later-that they contain mistakes. The...
Verification of Arithmetic Functions with Binary Moment Diagrams (2006)
Bryant, Randal E., Chen, Yirng-An
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...
On Solving Boolean Combinations of UTVPI Constraints (2006)
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
We consider the satisfiability problem for Boolean combinations of unit two variable per inequality (UTVPI) constraints. A UTVPI constraint is linear constraint containing at most two variables with...
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds (2005)
Seshia, Sanjit A., Bryant, Randal E.
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...
Semantics-Aware Malware Detection (2005)
Mihai Christodorescu, Somesh Jha, Sanjit A, Seshia Dawn Song, Randal E. Bryant
2 Semantics of malware detection
x86-64 Machine-Level Programming ∗ (2005)
Randal E. Bryant, David R. O’hallaron
Intel’s IA32 instruction set architecture (ISA), colloquially known as “x86”, is the dominant instruction format for the world’s computers. IA32 is the platform of choice for most Windows and...
Term-Level Verification of a Pipelined CISC (2005)
Microprocessor Randal Bryant, Randal E. Bryant
By abstracting the details of the data representations and operations in a microprocessor, term-level verification can formally prove that a pipelined microprocessor faithfully implements its...
Term-level verification of a pipelined CISC microprocessor (2005)
UCLID term-level verifier. Unlike many case studiesfor term-level verification, this processor was not designed specifically for formal verification. In addition, most of the control logic was given...
Term-level verification of a pipelined CISC microprocessor (2005)
By abstracting the details of the data representations and operations in a microprocessor, term-level verification can formally prove that a pipelined microprocessor faithfully implements its...
Modeling and verifying circuits using generalized relative timing (2005)
Sanjit A. Seshia, Randal E. Bryant, Pentium R
We propose a novel technique for modeling and verifying timed circuits based on the notion of generalized relative timing. Generalized relative timing constraints can express not just a relative...
Predicate Abstraction with Indexed Predicates (2004)
Lahiri, Shuvendu K., Bryant, Randal E.
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...
Deciding quantifier-free Presburger formulas using parameterized solution bounds (2004)
Sanjit A. Seshia, Randal E. Bryant
Given a formula # in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to #, there is one whose size, measured in bits, is polynomially bounded in the...
Deciding quantifier-free Presburger formulas using parameterized solution bounds (2004)
Sanjit A. Seshia, Randal E. Bryant
Given a formula in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to , there is one whose size, measured in bits, is polynomially bounded in the size...
Deciding quantifier-free Presburger formulas using parameterized solution bounds (2004)
Sanjit A. Seshia, Randal E. Bryant
Given a formula # in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to #, there is one whose size, measured in bits, is polynomially bounded in the...
Revisiting positive equality (2004)
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur
This paper provides a stronger result for exploiting positive equality in the logic of Equality with Uninterpreted Functions (EUF). Positive equality analysis is used to reduce the number of...
Constructing Quantified Invariants via Predicate Abstraction (2004)
Shuvendu K. Lahiri, Randal E. Bryant, Al E. Bryant
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...
Indexed Predicate Discovery for Unbounded System Verification (2004)
Shuvendu K. Lahiri, Randal E. Bryant, Al E. Bryant
Predicate abstraction has been proved effective for verifying several infinite-state systems. In predicate abstraction, an abstract system is automatically constructed given a set of predicates....
Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant
Symbolic non-deterministic planning represents action effects as sets of possible next states. In this article, we move toward a more probabilistic uncertainty model by distinguishing between likely...
Deciding quantifier-free Presburger formulas using parameterized solution bounds (2004)
Sanjit A. Seshia, Randal E. Bryant
Given a formula Φ in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to Φ, there is one whose size, measured in bits, is polynomially bounded in the...
Rune M. Jensen, Manuela M. Veloso, Randal E. Bryant
Symbolic non-deterministic planning represents action effects as sets of possible next states. In this article, we move toward a more probabilistic uncertainty model by distinguishing between likely...
On solving Boolean combinations of generalized 2SAT constraints (2004)
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
We consider the satisfiability problem for Boolean combinations of generalized 2SAT constraints, which are linear constraints with at most two, possibly unbounded, integer variables having...
Deciding quantifier-free Presburger formulas using parameterized solution bounds (2004)
Sanjit A. Seshia, Randal E. Bryant
Given a formula ¢ in quantifier-free Presburger arithmetic, it is well known that, if there is a satisfying solution to ¢ , there is one whose size, measured in bits, is polynomially bounded in the...
On solving Boolean combinations of generalized 2SAT constraints (2004)
Sanjit A. Seshia, K. Subramani, Randal E. Bryant
Abstract We consider the satisfiability problem for Boolean combinations of generalized 2SAT constraints, which arelinear constraints with at most two, possibly unbounded, integer variables having...
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions (2003)
Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
SAT-based decision procedures for quantifier-free fragments of firstorder logic have proved to be useful in formal verification. These decision procedures are either based on encoding atomic...
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis (2003)
Symbolic techniques usually use characteristic functions for representing sets of states. Boolean functional vectors provide an alternate set representation which is suitable for symbolic simulation....
A Boolean approach to unbounded, fully symbolic model checking of timed automata (2003)
Sanjit A. Seshia, Randal E. Bryant
We present a new approach to unbounded, fully symbolic model checking of timed automata that is based on an e#cient translation of quantified separation logic to quantified Boolean logic. Our...
A User's Guide to UCLID version 1.0 (2003)
Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
This document is intended to serve as an overview of UCLID, as a tutorial, and as a reference manual for the UCLID user. In Section 2, we describe the syntax and semantics of the UCLID language. In...
Convergence Testing in Term-Level Bounded Model Checking (2003)
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
We consider the problem of bounded model checking of systems expressed in a decidable fragment of rst-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it...
Convergence Testing in Term-Level Bounded Model Checking (2003)
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it...
A Symbolic Approach to Predicate Abstraction (2003)
Shuvendu K. Lahiri, Randal E. Bryant, Al E. Bryant, Byron Cook
Predicate abstraction is a useful form of abstraction for the veri cation of transition systems with large or in nite state spaces. One of the main bottlenecks of this approach is the extremely large...
Reducing separation formulas to propositional logic (2003)
Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
A short version of this report titled ‘Deciding Separation Formulas with SAT ’ appeared
Miroslav N. Velev, Randal E. Bryant
TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories
A hybrid SAT-based decision procedure for separation logic with uninterpreted functions (2003)
Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
SAT-based decision procedures for quantifier-free fragments of firstorder logic have proved to be useful in formal verification. These decision procedures are either based on encoding atomic...
Convergence testing in term-level bounded model checking (2003)
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
Abstract We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary...
Deductive Verification of Advanced Out-of-Order Microprocessors (2003)
Shuvendu K. Lahiri, Randal E. Bryant, Al E. Bryant
This paper demonstrates the modeling and deductive verification of out-of-order microprocessors of varying complexities using a logic of Counter Arithmetic with Lambda Expressions and Uninterpreted...
A Boolean approach to unbounded, fully symbolic model checking of timed automata (2003)
Sanjit A. Seshia, Randal E. Bryant
We present a new approach to unbounded, fully symbolic model checking of timed automata that is based on an efficient translation of quantified separation logic to quantified Boolean logic. Our...
Concurrent Programming, (2002)
Bryant,Randal E., Dennis,Jack B.
Concurrency of activities has long been recognized as an important feature in many computer systems. These systems allow concurrent operations for a number of reasons on which three are particularly...
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
Abstract. In this paper, we present the logic of Counter arithmetic with Lambda expressions and Uninterpreted functions (CLU). CLU generalizes the logic of equality with uninterpreted functions (EUF)...
Deciding separation formulas with SAT (2002)
Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
Abstract. We show a reduction to propositional logic from a Boolean combination of inequalities of the form v i v j + c and v i> v j + c, where c is a constant and v i; v j are variables of type...
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
Abstract. In this paper, we present the logic of Counter arithmetic with Lambda expressions and Uninterpreted functions (CLU). CLU generalizes the logic of equality with uninterpreted functions (EUF)...
Deciding CLU Logic formulas via Boolean and Pseudo-Boolean encodings (2002)
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
Abstract. UCLID is a tool for specifying and verifying systems expressed in a quantier-free rst-order logic, called CLU logic, that includes uninterpreted functions, equality, ordering, constrained...
Ordererd Binary Decision Diagrams in Electronic Design Automation, chapter 11 (2002)
Randal E. Bryant, Christoph Meinel
Abstract Ordered Binary Decision Diagrams (OBDDs) play a key role in the automated synthesis and formal verication of digital systems. They are the state-of-the-art data structure for representing...
Deciding CLU Logic formulas via Boolean and Pseudo-Boolean encodings (2002)
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
Abstract. UCLID is a tool for specifying and verifying systems expressed in a quantifier-free first-order logic, called CLU logic, that includes uninterpreted functions, equality, ordering,...
SetA* Applied to Channel Routing (2002)
Rune M. Jensen, Randal E. Bryant, Manuela M. Veloso
This report describes an application of the SetA* algorithm to VLSI channel routing. We consider an extended form of the classical routing problem where pins of nets can occur anywhere within the...
State-Set Branching: Leveraging OBDDs for Heuristic Search (2002)
Rune M. Jensen, Randal E. Bryant, Manuela M. Veloso
In this paper, we introduce a framework called state-set branching that combines symbolic search based on the reduced Ordered Binary Decision Diagram (OBDD) with classical heuristic search, such as...
Miroslav N. Velev, Randal E. Bryant
personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the...
Randal E. Bryant, Steven German, Miroslav N. Velev
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...
Verification of Arithmetic Circuits Using Binary Moment Diagrams (2001)
Randal E. Bryant, Al E. Bryant, Yirng-an Chen
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...
Computing Logic-Stage Delays Using Circuit Simulation and Symbolic Elmore Analysis (2001)
Clayton B. Mcdonald, Randal E. Bryant
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...
Limitations and Challenges of Computer-Aided Design Technology for CMOS VLSI (2001)
Randal E. Bryant, Kwang-Ting Cheng, Andrew B. Kahng, Kurt Keutzer, Wojciech Maly, Richard Newton
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...
Symbolic Simulation Using Automatic Abstraction of Internal Node Values (2001)
James Christopher Wilson, David L. Dill, Mark Horowitz, Randal E. Bryant
In recent years, veri cation has emerged as a major portion of the eort in designing large, complex chips. Simulation-based methods such as directed and random testing are the most widely used veri...
An Efficient Graph Representation for Arithmetic Circuit Verification (2001)
Yirng-an Chen, Randal E. Bryant, Al E. Bryant
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...
Boolean Satisfiability with Transitivity Constraints (2000)
Bryant, Randal E., Velev, Miroslav N.
We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements....
Formal Verification of Superscalar Microprocessors with Multicycle Functional Units (2000)
Miroslav N. Velev, Randal E. Bryant
classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To...
Boolean satisfiability with transitivity constraints (2000)
Randal E. Bryant, Miroslav N. Velev
Abstract. We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula F sat encode a symmetric, transitive, binary relation over N...
A Theory of Consistency for Modular Synchronous Systems (2000)
Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel
Abstract. We propose a model for modular synchronous systems with combinational dependencies and define consistency using this model. We then show how to derive this model from a modular...
Symbolic Timing Simulation Using Cluster Scheduling (2000)
Clayton Mcdonald Randal, Clayton B. Mcdonald, Randal E. Bryant
We recently introduced symbolic timing simulation (STS) using data-dependent delays as a tool for verifying the timing of fullcustom transistor-level circuit designs, and for the functional...
Boolean Satisfiability with Transitivity Constraints (2000)
Randal E. Bryant, Miroslav N. Velev
We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula F sat encode a symmetric, transitive, binary relation over N elements....
Boolean satisfiability with transitivity constraints (2000)
Randal E. Bryant, Miroslav N. Velev
We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements....
Bryant, Randal E., German, Steven, Velev, Miroslav N.
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...
Miroslav N. Velev, Randal E. Bryant
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...
Miroslav N. Velev, Randal E. Bryant
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...
Exploiting positive equality in a logic of equality with uninterpreted functions (1999)
Randal E. Bryant, Steven German, Miroslav N. Velev
Abstract. In using the logic of equality with unininterpreted functions to verify hardware systems, specific characteristics of the formula describing the correctness condition can be exploited when...
Optimizing Symbolic Model Checking for Constraint-Rich Models (1999)
Bwolen Yang, Reid Simmons, Randal E. Bryant, Al E. Bryant, David R. O'Hallaron
. This paper presents optimizations for verifying systems with complex time-invariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the...
Optimizing Symbolic Model Checking for Constraint-Rich Models (1999)
Bwolen Yang, Reid Simmons, Randal E. Bryant, David R. O'hallaron
This paper presents optimizations for verifying systems with complex timeinvariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the...
Optimizing Symbolic Model Checking for Constraint-Rich Models (1999)
Bwolen Yang Reid, Reid Simmons, David R. O’hallaron, Randal E. Bryant
This paper presents optimizations for verifying systems with complex timeinvariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the...
Optimizing Symbolic Model Checking for Constraint-Rich Models (1999)
Bwolen Yang, Reid Simmons, Randal E. Bryant, David R. O’Hallaron
This paper presents optimizations for verifying systems with complex time-invariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the...
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions (1999)
Randal E. Bryant, Steven German, Miroslav N. Velev
. In using the logic of equality with unininterpreted functions to verify hardware systems, specific characteristics of the formula describing the correctness condition can be exploited when deciding...
Formal verification of an ARM processor (1999)
Vishnu A. Patankar, Alok Jain, Randal E. Bryant
This paper presents a detailed description of the application of a formal verification methodology to an ARM processor. The processor, a hybrid between the ARM7 and the StrongARM processors, uses...
Partial order reduction for verification of timed systems (1999)
Marius Minea, Randal E. Bryant, Jeannette M. Wing
conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of SRC, NSF, DARPA, or the United States Government.
Optimizing Symbolic Model Checking for Constraint-Rich Models (1999)
Bwolen Yang, Reid Simmons, David R. O’hallaron, Randal E. Bryant
representing the official policies or endorsements,either expressed or implied, of the Advanced
Randal E. Bryant, Steven German, Miroslav N. Velev
Modern processors have relatively simple specifications based on their instruction set architectures. Their implementations, however, are very complex, especially with the advent of...
Partial order reduction for verification of timed systems (1999)
Marius Minea, Randal E. Bryant, Jeannette M. Wing
conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of SRC, NSF, DARPA, or the United States Government.
Randal E. Bryant, Steven German, Miroslav N. Velev
. Modern processors have relatively simple specificationsbased on their instruction set architectures. Their implementations, however, are very complex, especially with the advent of...
A Methodology for Hardware Verification Based on Logic Simulation. (1998)
A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits implementing the system specification will produce particular response to a sequence of...
Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams, (1998)
Ordered Binary Decision Diagrams OBDDs represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satisfiability and...
Work Efficient Hashing on Parallel and Vector Computers, (1998)
Sheffler, Thomas J., Bryant, Randal E.
Hashing techniques have long been used to efficiently store and locate data indexed by key. Recently, parallel hashing algorithms have been developed that allow table insertion of many keys in a few...
Bit-Level Analysis of an SRT Divider Circuit. (1998)
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...
Verification of Floating-Point Adders (1998)
Chen, Yirng-An, Bryant, Randal E.
The floating-point division bug in Intel's Pentium processor and the overflow flag erratum of the FIST instruction in Intel's Pentium Pro and Pentium II processor have demonstrated the importance and...
Optimizing Symbolic Model Checking for Constraint-Rich Models (1998)
Yang, Bwolen, Simmons, Reid, Bryant, Randal E., O'Hallaron, David R.
This paper presents optimizations for verifying systems with complex time- invariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the...
Bryant, Randal E., German, Steven, Velev, Miroslav N.
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...
Optimizing Model Checking Based on BDD Characterization. (1998)
Yang, Bwolen, O'Hallaron, David R., Bryant, Randal E., Clarke, Edmund M., Gross, Thomas R.
Symbolic model checking has been successfully applied in verification of various finite state systems, ranging from hardware circuits to software protocols. A core technology underlying this success...
A Switch-Level Model and Simulator for MOS Digital Systems (1998)
The switch-level model describes the logical behavior of digital systems implemented in metal oxide semiconductor (MOS) technology. In this model a network consist of a set of nodes connected by...
Miroslav N. Velev, Randal E. Bryant
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...
Miroslav N. Velev, Randal E. Bryant
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...
A Performance Study of BDD-Based Model Checking (1998)
Bwolen Yang, Randal E. Bryant, Al E. Bryant, David R. O'Hallaron, Armin Biere, Olivier Coudert, ...
We present a study of the computational aspects of model checking based on binary decision diagrams (BDDs). By using a tracebased evaluation framework, we are able to generate realistic benchmarks...
Space- and Time-Efficient BDD Construction via Working Set Control (1998)
Bwolen Yang, Yirng-an Chen, Randal E. Bryant, David R. O'Hallaron
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...
This paper presents lower bound results on Boolean function complexity under two different models. The first is an abstraction of tradeoffs between chip area and speed in very large scale integrated...
Verification of Floating-Point Adders (1998)
Yirng-an Chen, Randal E. Bryant, Al E. Bryant
. In this paper, we present a "black box" version of verification of FP adders. In our approach, FP adders are verified by an extended word-level SMV using reusable specifications without...
Space- and Time-Efficient BDD Construction via Working Set Control (1998)
Bwolen Yang, Yirng-an Chen, Randal E. Bryant, David R. O'hallaron
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...
Verification of Floating-Point Adders (1998)
Yirng-an Chen, Randal E. Bryant
The floating-point division bug in Intel's Pentium processor and the overflow flag erratum of the FIST instruction in Intel's Pentium Pro and Pentium II processor have demonstrated the...
Alpha Assembly Language Guide (1998)
This document provides an overview of the Alpha instruction set and assembly language programming conventions. The Alpha architecture was formulated by Digital Equipment Corporation as a second...
PBHD: An Efficient Graph Representation for Floating Point Circuit Verification, (1997)
Chen, Yirng-An, Bryant, Randal E.
*BMDs, HDDs, and K*BMDs provide compact representations for functions which map Boolean vectors into integer values, but not floating point values. In this paper, we propose a new data structure,...
Breadth-First with Depth-First BDD Construction: A Hybrid Approach, (1997)
Chen, Yirng-An, Yang, Bwolen, Bryant, Randal E.
This paper presents the technique of operator sifting as a new way of understanding both breadth-first and depth-first approaches to BDD construction. A new algorithm is also proposed to capture the...
PHDD: An efficient graph representation for floating point circuit verification (1997)
Yirng-an Chen, Randal E. Bryant
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. In this paper, we propose a...
PHDD: An efficient graph representation for floating point circuit verification (1997)
Yirng-an Chen, Randal E. Bryant
compact representations for functions which map Boolean vectors into integer values, but not floating point values. In this paper, we propose a new data structure, called Multiplicative Power Hybrid...
Formal verification of content addressable memories using symbolic trajectory evaluation (1997)
Manish Pandey, Richard Raimi, Randal E. Bryant, Magdy S. Abadir
In this paper we report on new techniques for verifying content addressable memories (CAMs), and demonstrate that these techniques work well for large industrial designs. It was shown in [6], that...
Formal Verification of a Superscalar Execution Unit (1997)
Kyle L. Nelson, Alok Jain, Randal E. Bryant
Abstract. 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...
*PBHD: An Efficient Graph Representation for Floating Point Circuit Verification (1997)
*BMDs, HDDs, and K*BMDs provide compact representations for functions which map Boolean vectors into integer values, but not floating point values. In this paper, we propose a new data structure,...
Breadth-First with Depth-First BDD Construction: A Hybrid Approach (1997)
Yirng-an Chen, Randal E. Bryant
This paper presents the technique of operator sifting as a new way of understanding both breadth-first and depth-first approaches to BDD construction. A new algorithm is also proposed to capture the...
Breadth-First with Depth-First BDD Construction: A Hybrid Approach (1997)
Yirng-an Chen, Bwolen Yang, Randal E. Bryant
This paper presents the technique of operator sifting as a new way of understanding both breadth-first and depth-first approaches to BDD construction. A new algorithm is also proposed to capture the...
Formal verification of PowerPC arrays using symbolic trajectory evaluation (1997)
Manish Pandey, Richard Raimi, Derek L. Beatty, Randal E. Bryant
assertions IMPLEMENTATION switch-level Figure 4: Tool organization for our verification experiments.
*PBHD: An Efficient Graph Representation for Floating Point Circuit Verification (1997)
Yirng-an Chen, Randal E. Bryant
*BMDs, HDDs, and K*BMDs provide compact representations for functions which map Boolean vectors into integer values, but not floating point values. In this paper, we propose a new data structure,...
*PHDD: An Efficient Graph Representation for Floating Point Circuit Verification (1997)
Yirng-an Chen, Randal E. Bryant
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. In this paper, we propose a...
Formal Verification of a Superscalar Execution Unit (1997)
Kyle L. Nelson, Alok Jain, Randal E. Bryant
Abstract. 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...
Bit-level analysis of an srt divider circuit (1996)
Abstract--- 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...
Verifying Nondeterministic Implementations of Deterministic Systems (1996)
Alok Jain, Kyle Nelson, Randal E. Bryant
Abstract. Some modern systems with a simple deterministic high-level specification have implementations that exhibit highly nondeterministic behavior. Such systems maintain a simple operation...
ACV: An Arithmetic Circuit Verifier (1996)
Yirng-an Chen, Randal E. Bryant
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...
Verifying Nondeterministic Implementations of Deterministic Systems (1996)
Alok Jain, Kyle Nelson, Randal E. Bryant
Abstract. Some modern systems with a simple deterministic high-level specification have implementations that exhibit highly nondeterministic behavior. Such systems maintain a simple operation...
ACV: An Arithmetic Circuit Verifier (1996)
Yirng-an Chen, Randal E. Bryant
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...
ACV: An Arithmetic Circuit Verifier (1996)
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...
Verification of arithmetic functions with binary moment diagrams (1995)
Randal E. Bryant, Yirng-an Chen
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...
Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification (1995)
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...
Bit-Level Analysis of an SRT Divider Circuit (1995)
Randal Bryant April, Randal E. Bryant
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...
Verification of Arithmetic Functions with Binary Moment Diagrams (1995)
Randal E. Bryant, Yirng-an Chen
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...
Bit-Level Analysis of an SRT Divider Circuit (1995)
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...
Bit-Level Analysis of an SRT Divider Circuit (1995)
Randal Bryant April, Randal E. Bryant
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...
Formal Verification by Symbolic Evaluation of Partially-Ordered (1995)
Symbolic trajectory evaluation provides a means to formally verify properties of a sequential system by a modified form of symbolic simulation. The desired system properties are expressed in a...
Binary Decision Diagrams and Beyond: (1995)
Enabling Technologies For, Randal E. Bryant
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...
Digital Circuit Verification using Partially-Ordered State Models (1994)
Many aspects of digital circuit operation can be efficiently verified by simulating circuit operation over "weakened " state values. This technique has long been practiced with...
Formally Verifying a Microprocessor Using a Simulation Methodology (1994)
Derek L. Beatty, Randal E. Bryant
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.,...
On Sept. 7, 1993, U. S. Patent Number 5,243,538 was awarded to four Hitachi employees for a technique for comparing logic circuits using Binary Decision Diagrams (BDDs). Although the U. S. patent...
On Sept. 7, 1993, U. S. Patent Number 5,243,538 was awarded to four Hitachi employees for a technique for comparing logic circuits using Binary Decision Diagrams (BDDs). Although the U. S. patent...
Lawrence P. Huang, Randal E. Bryant, J. D. Tygar
The range of operating conditions for a series-parallel network of variable linear resistors, voltage sources, and current sources can be represented as a convex polygon in a Thevenin or Norton...
Randal E. Bryant, J. D. Tygar, Lawrence P. Huang
The range of operating conditions for a series-parallel network of variable linear resistors, voltage sources, and current sources can be represented as a convex polygon in a Thevenin or Norton...
Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories (1993)
Symbolic trajectory evaluation provides a means to formally verify properties of a sequential system by a modified form of symbolic simulation. The desired system properties are expressed in a...
Symbolic Analysis Methods (1993)
For Masks Circuits, Randal E. Bryant
Symbolic representations of systems can achieve a high degree of compaction relative to more explicit forms. By casting an analysis task in terms of operations on a symbolic representation, large and...
Model Checking, Abstraction, and Compositional Verification (1993)
Randal E. Bryant, Stephen D. Brookes, Orna Grumberg, The Technion, C Fl, David E. Long, ...
ion, and Compositional Verification David E. Long July 1993 Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy Thesis Committee: Edmund M. Clarke, Chair...
Symbolic Boolean manipulation with ordered binary-decision diagrams (1992)
Ordered Binary-Decision Diagrams (OBDDS) represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satmfiability...
A methodology for hardware verification based on logic simulation (1991)
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...
Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis (1991)
The program TRANALYZE generates a gate-level representation of an MOS transistor circuit. The resulting model contains only four-valued unit and zero delay logic primitives, suitable for evaluation...
Formal verification of memory circuits by switch-level simulation (1991)
A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits implementing the system specification will produce a particular response to a sequence of...
Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation (1991)
Randal E. Bryant, Derek L. Beatty
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...
Formal verification of memory circuits by switch-level simulation (1991)
A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits implementing the system specification will produce a particular response to a sequence of...
Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis (1991)
The program TRANALYZE generates a gate-level representation of an MOS transistor circuit. The resulting model contains only four-valued unit and zero delay logic primitives, suitable for evaluation...
Formal Verification of Digital Circuits Using Symbolic Ternary System Models (1990)
Randal E. Bryant, Carl-johan Seger
Ternary system modeling involves extending the traditional set of binary values f0; 1g with a third value X indicating an unknown or indeterminate condition. By making this extension, we can model a...
Formal Verification of Digital Circuits Using Symbolic Ternary System Models (1990)
Randal E. Bryant, Carl-johan Seger
Ternary system modeling involves extending the traditional set of binary values ¡ 0 ¢ 1 £ with a third value X indicating an unknown or indeterminate condition. By making this extension, we can...
Symbolic Simulation-Techniques and Applications (1990)
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...
Verification of Synchronous Circuits by Symbolic Logic Simulation (1989)
Abstract. A logic simulator can prove the correctness of a digital circuit when it can be shown that only circuits implementing the system specification will produce a particular response to a...
Test Pattern Generation for Sequential MOS Circuits by Symbolic Fault Simulation (1989)
Kyeongsoon Cho, Randal E. Bryant
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...
Verifying a Static RAM Design (1988)
Logic Simulation Randal, Randal E. Bryant
this paper, it is backed up by a more formal theory and proof [5]. Of course, this style of verification proves the correctness of the actual circuit only if the simulator faithfully models the...
Data Parallel Switch-Level Simulation (1988)
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...
Boolean analysis of MOS circuits (1987)
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...
Algorithmic aspects of symbolic switch network analysis (1987)
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...
Cosmos: A compiled simulator for mos circuits (1987)
Randal E. Bryant, Derek Beatty, Karl Brace, Kyeongsoon Cho, Thomas Sheffler
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 analysis of MOS circuits (1987)
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...
Algorithmic aspects of symbolic switch network analysis (1987)
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...
Graph-based algorithms for Boolean function manipulation (1986)
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...
Graph-Based Algorithms for Boolean Function Manipulation (1986)
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...
Graph-Based Algorithms for Boolean Function Manipulation* (1986)
Randal Brya Nt, Randal E. Bryant
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...
Graph-based algorithms for Boolean function manipulation (1986)
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...
Symbolic manipulation of boolean functions using a graphical representation (1985)
In this paper we describe a data structure for representing Boolean functions and an associated set of manipulation algorithms. Functions are represented by directed, acyclic graphs in a manner...
Symbolic Manipulation of Boolean Functions Using a Graphical Representation (1985)
In this paper we describe a data structure for representing Boolean functions and an associated set of manipulation algorithms. Functions are represented by directed, acyclic graphs in a manner...
Switch-Level Model and Simulator for MOS Digital Systems (1983)
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...