Decision Directed Timing Recovery Algorithm (2009)
Max Grade, Daifeng Wang, Diptendu Ghosh, Adnan Aziz
The objective of Lab 4 is to study and implement a decision-directed timing-recovery algorithm at receiver in the baseband communication system. Timing recovery guarantees that the receiver samples...
Time Domain: Z-Domain: Filter Specification: (2009)
Max Grade, Diptendu Ghosh, Daifeng Wang, Adnan Aziz
The objective of this assignment is to analyze the effects round-off errors due to quantization of the of the filter coefficients and outputs of the arithmetic units; i.e., adders and multipliers in...
VLSI Communication Systems – Lab3 LMS Based Adaptive Equalizer (2009)
Max Grade, Diptendu Ghosh, Daifeng Wang, Adnan Aziz
The objective of this assignment is to study and implement an LMS based adaptive equalizer for BPSK modulation in the presence of multipath. We consider a simple BPSK Transmitter-Receiver system...
Packet routing problem Array routing (2009)
Resolving Contention, Adnan Aziz
Route packets along shortest path (not always unique) • linear array: greedy algorithm moves packets left/right as needed – assume: start with at most 1 packet at each node, 1-to-1 routing –...
Objective: VLSI Communication Systems – Lab3 (2009)
Diptendu Ghosh, Daifeng Wang, Adnan Aziz
The objective of this assignment is to study and implement an LMS based adaptive equalizer for BPSK modulation in the presence of multipath. We consider a simple BPSK Transmitter-Receiver system...
We address the problem of checking whether two combinational designs are equivalent. We first show that this problem is intimately connected to the notion of composition. We then prove some Boolean...
• signaling for set up and tear down (significant delay/overhead for short connections) • each switch needs state for each VC • small identifier reduces overhead (fast classification algorithms...
Interconnection Networks Butterfly routing 3 of 15 Butterfly routing (2009)
Note there exists a unique path from any level 0 vertex to
3 Now at Lattice Semiconductor Contents (2008)
Adnan Aziz, Robert Brayton, Stephen Edwards, Sunil Khatri, Yuji Kukimoto, Abelardo Pardo, ...
Time Domain: Z-Domain: Filter Specification: (2008)
Diptendu Ghosh, Daifeng Wang, Adnan Aziz
The objective of this assignment is to analyze the effects round-off errors due to quantization of the of the filter coefficients and outputs of the arithmetic units; i.e., adders and multipliers in...
Optimizing Designs Containing Black Boxes*t (2008)
Tai-hung Liu, Khurram Sajid, Adnan Aziz
We define a notion of equivalence for designs containing black boxes i.e., components whose functionality is not known: these arise naturally in the course of hierarchi-cal design. Using this notion,...
Praveen Yalagandula, Vigyan Singhal, Adnan Aziz, Andreas Kuehlmann
We introduce SImulation Verification with Augmentation (SIVA), a tool for coverage-directed state space search on digital hardware designs. SIVA tightly integrates simulation with symbolic techniques...
Will study classification based on header fields • IP src/dest addresses, protocol, TCP src/dest ports Syntactically, rule is (predicate, action) pair • predicate is sequence of prefixes, one per...
Abstract Sequential Synthesis UsingS1S � (2008)
Adnan Aziz, Felice Balarin, Robert Brayton, Alberto Sangiovanni-vincentelli, Computer Sciences
We present a mathematical framework for analyzing the synthesis of interacting finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in...
Exploiting Constraints in Transformation-Based Verification (2008)
Hari Mony, Jason Baumgartner, Adnan Aziz
Abstract. The modeling of design environments using constraints has gained widespread industrial application, and most verification languages include constructs for specifying constraints. It is...
Amit Prakash, Ramakrishna Kotla, Tanmoy Mandal, Adnan Aziz
A reconfigurable architecture and associated
My current research focuses on Graph Algorithms and Machine Learning techniques for Web Search applications. I work on hyper-link analysis, query independent ranking of documents, and web-spam...
Abstract Efficient BDD Algorithms for FSM Synthesis and Verification (2008)
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley
We describe a set of BDD based algorithms for efficient FSM synthesis and verification. We establish that the core computation in both synthesis and verification is forming the image and pre-image of...
Vigyan Singhal, Carl Pixley, Adnan Aziz, Shaz Qadeer, Robert Brayton
We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions...
Abstract Hybrid Techniques for Fast Functional Simulation (2008)
Yufeng Luo, Tjahjadi Wongsonegoro, Adnan Aziz
We implement and experiment with techniques for the functional simulation of very large digital systems. We consider techniques that are a hybrid of classical compiled code simulation and recent...
Scheduling Traffic Matrices On General Switch Fabrics (2008)
Xiang Wu, Amit Prakash, Marghoob Mohiyuddin, Adnan Aziz
A traffic matrix is an |S|×|T | matrix M,whereMij is a non-negative integer encoding the number of packets to be transferred from source i to sink j. Chang et al. [2] have shown how to efficiently...
Ramakrishna Rao Kotla, Michael D. Dahlin, Lorenzo Alvisi, Vijay Garg, Adnan Aziz, Thomas W. Keller, ...
To my beloved grand father (Thathayya), Bhujanga Rao Boinpalli.
Abstract Hybrid Techniques for Fast Functional Simulation (2007)
Yufeng Luo, Tjahjadi Wongsonegoro, Adnan Aziz
We implement and experiment with techniques for the functional simulation of very large digital systems. We consider techniques that are a hybrid of classical compiled code simulation and recent...
Lecture 9 -- Mathematical Logic I Sets and Propositional Logic (2007)
. In this lecture, we introduce the basic elements of mathematical logic. Specifically, we review some basic definitions related to sets, and then develop propositional logic. Elements of Set Theory...
Heuristic Symmetry Reduction for Invariant Verification (2007)
William Hung, Adnan Aziz, Ken Mcmillan
We describe techniques that use symmetry to perform efficient invariant checking. We start by developing the theory needed to exploit symmetry for designs specified at the gate level. This is...
Notes on Boolean Functions (2007)
. This note covers some basic definitions, terminology, and results on Boolean functions. Details are available in [1, 2]. 1 Introduction A Boolean function is a function whose domain is B n (for...
An Efficient Deterministic Algorithm for the Resource Discovery Problem (2007)
We address the problem of how best to get a group of machines on a network to learn of each others existence; this is referred to as the Resource Discovery Problem (RDP). Straightforward algorithms...
Lucent Technologies and (2007)
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert Brayton
We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov...
Acknowledgement of Support (2007)
Praveen Yalagandula, Adnan Aziz, Andreas Kuehlmann, Vigyan Singhal
We introduce SImulation Verification with Augmentation (SIVA), a tool for coverage-directed state space search on digital hardware designs. SIVA tightly integrates simulation with symbolic techniques...
Praveen Yalagandula, Adnan Aziz, Andreas Kuehlmann, Vigyan Singhal
We introduce SImulation Verification with Augmentation (SIVA), a tool for coverage-directed state space search on digital hardware designs. SIVA tightly integrates simulation with symbolic techniques...
EE382N, Topic 3 – Interconnection Networks Spring 2002 (2007)
We aim to study issues related to the design of high-performance interconnection networks. The course will begin with a review of the basics of packet switched networks, with an emphasis on...
Hai Zhou, Vigyan Singhal, Adnan Aziz
This paper is about exploring the power of retiming and resynthesis. We show that there exists a pair of "sequentially equivalent " designs so that one cannot be obtained from...
Enhancements to Invariant Verication using SIVA (2007)
Simulation is simple and scales well but suers from low design space coverage. To compensate for low coverage, SIVA, the invariant verication tool, uses symbolic computations. We discuss strategies...
Heuristic Symmetry Reduction for Invariant Verification (2007)
William Hung Adnan, William Hung, Adnan Aziz, Ken Mcmillan
We describe techniques that use symmetry to perform efficient invariant checking. We start by developing the theory needed to exploit symmetry for designs specified at the gate level. This is...
Generation of Efficient Codes for Realizing Boolean Functions in Nanotechnologies (2007)
Singh, Ashish Kumar, Aziz, Adnan, Vishwanath, Sriram, Orshansky, Michael
We address the challenge of implementing reliable computation of Boolean functions in future nanocircuit fabrics. Such fabrics are projected to have very high defect rates. We overcome this...
Ashish Kumar Singh, Michael Orshansky Supervisor, Adnan Aziz, Sani Nassif, Sanjay Shakkottai, Nur Touba, ...
The Dissertation Committee for Ashish Kumar Singh Certifies that this is the approved version of the following dissertation:
Floating-Point Fused Multiply-Add Architectures (2007)
Eric Charles Quinnell, Earl E. Swartzl, Jacob Abraham, Tony Ambler, Jason Arbaugh, Adnan Aziz, ...
For my wife Eres mi vida, mi alma, y mi corazón. Acknowledgements This work on the design and implementation of the new floating-point fused multiply-add architectures would not be possible without...
A Theory for the Design and Analysis of Firewalls (2006)
Mohamed G. Gouda, Adnan Aziz, Benjamin Kuipers, Simon S. Lam, Charles Gregory Plaxton, ...
Dedicated with love and respect to my parents Shuxiang Wang and Yuhai Liu (God rest his soul), to my family Huibo Heidi Ma, Max Boyang and Louis Boyang, to whom I owe all that I am and all that I...
To my supervising professor, Nur A. Touba. (2006)
Jinkyu Lee, Nur A. Touba, Tony Ambler, Adnan Aziz, David Z. Pan, Jinkyu Lee
version of the following dissertation:
Haoxing Ren, David Z. Pan, Jacob Abraham, Charles J. Alpert, Adnan Aziz, Nur Touba, ...
To my mother and father
Deductive Mechanical Verification of Concurrent Systems (2005)
Robert W. Sumners, Jacob A. Abraham, J Strother Moore, Adnan Aziz, Donald S. Fussell, Warrent A. Hunt, ...
In the tenure of a graduate student, one often has the distinct pleasure to interact and work with a number of different colleagues with different perspectives in general and on research problems in...
Robert Henry Bell, Lizy K. John, Earl E. Swartzlander, Douglas C. Burger, Adnan Aziz, Lieven Eeckhout, ...
This work would not have been possible without the support of many people. I would like to thank my advisor, Dr. Lizy Kurian John, for her advice, support, wisdom, and guidance. Dr. John had a...
Amit Prakash, Adnan Aziz, Vijaya Ramachandran
We present new results and numerical studies of very fast schedulers for SMS (Switch-Memory-Switch) routers, which emulate output-queuing by buffering packets in a partitioned shared-memory located...
Synthesizing Interconnect-Efficient Low Density Parity Check Codes (2004)
Marghoob Mohiyuddin, Amit Prakash, Adnan Aziz, Wayne Wolf
and storage applications. Codec complexity has usually been measured with a software implementation in mind. A recent hardware implementation of a Low Density Parity Check code (LDPC) indicates that...
Automatic Verification of Arithmetic Circuits in RTL using Term Rewriting Systems (2003)
Shobha Vasudevan, Jacob A. Abraham, Nur A. Touba, Adnan Aziz
for being my quest... for showing me the way... Acknowledgments I’d like to thank my advisor, Dr. Jacob Abraham for his invaluable support and guidance through the course of this work. His novel...
Non-Binary Capacitor Array Calibration for a High Performance Successive Approximation (2003)
Jianhua Gan, Jacob Abraham Supervisor, Shouli Yan Supervisor, Anthony Ambler, Adnan Aziz, Shaochen Chen, ...
Dedicated to my wife Erxiang. Acknowledgments I wish to thank many people who taught and helped me. I would like to thank my supervisor Prof. Jacob Abraham for his invaluable guidance. His...
A near optimal scheduler for switchmemory-switch routers (2003)
Adnan Aziz, Amit Prakash, Vijaya Ramachandran
Routers are ubiquitous in modern computing, appearing in wide-area networks, multiprocessor servers, and data storage systems. Modern routers achieve high performance by solving computationally...
A near optimal scheduler for switchmemory-switch routers (2003)
Adnan Aziz, Amit Prakash, Vijaya Ramach, Ran Electrical, Computer Engineering, Computer Sciences
We show that the total amount of buffer memory required by our algorithm is close to the minimum required. We also show that the number of buffer memories is within an fflN additive term of 2N \Gamma...
An abstraction algorithm for the verification of level-sensitive latch-based netlists (2003)
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz
Abstract. High-performance hardware designs often intersperse combinational logic freely between level-sensitive latch layers (wherein each layer is transparent during only one clock phase), rather...
Automatic Structural Abstraction Techniques for Enhanced Verification (2002)
Jacob Abraham Supervisor, Andreas Kuehlmann, Adnan Aziz, E. Allen Emerson, Lizy Kurian John, Jason Raymond Baumgartner, ...
To my wife Shelly, to my parents, to my grandmothers and the memory of my grandfathers, to the memory of Clover, and to the semi-formal team at IBM Acknowledgments This acknowledgment is partitioned...
Dedication To My Parents Acknowledgements (2002)
Ranganathan Sankaralingam, Nur A. Touba, Anthony A. Ambler, Adnan Aziz, Douglas C. Burger, Margarida F. Jacome, ...
the approved version of the following dissertation:
Multicast scheduling for switches with multiple input-queues (2002)
Shashank Gupta, Andiamo Systems, Adnan Aziz
We address the problem of serving multicast traffic in input-queued packet switches. Head-of-line blocking is a major problem in input-queued switches. It can be avoided in unicast switches by...
A middle ground between CAMs and DAGs for high-speed packet classification (2002)
Packet classification is a computationally intensive task that routers need to perform at high speed to implement features such as QoS, access control, and VPNs. A classification rule-set consists of...
Rarity based guided state space search. GLSVLSI (2001)
State explosion is a common problem when verifying large designs. Partial state exploration using guided techniques has become a subject of wide research. We propose a rarity-based metric for state...
Integrated Power Supply Planning and Floorplanning (2001)
I-min Liu, Hung-ming Chen, Tan-li Chou, Adnan Aziz, D. F. Wong
One of the most challenging issues in today’s high-performance VLSI design is to ensure high-quality power supply to each individual circuit blocks. Reduced power supply voltage can result in...
Meeting delay constraints in DSM by minimal repeater insertion (2000)
We address the problem of inserting repeaters, selected from a library, at feasible locations in a placed and routed network to meet user-specified delay constraints. We use minimal repeater area by...
SIVA: A System for Coverage-Directed State Space Search (2000)
Malay Ganai, Praveen Yalagandula, Adnan Aziz, Andreas Kuehlmann, Vigyan Singhal
Sequential synthesis using s1s (2000)
Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto Sangiovanni-vincentelli
Abstract—We propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this leads to simple and mathematically elegant...
Meeting Delay Constraints in DSM by Minimal Repeater Insertion (2000)
Min Liu Adnan, I-min Liu, Adnan Aziz, D. F. Wong
We address the problem of selecting repeater sizes and inserting at feasible locations in a placed and routed network to meet delay constraints using minimal repeater area, taking the advantage of...
Automatic Lighthouse Generation for Directed State Space Search (2000)
Praveen Yalagandula, Vigyan Singhal, Adnan Aziz
Previous researchers have suggested the use of "lighthouses" to act as guides in directed state space search. The drawback of using lighthouses is that the user has to manually derive them,...
Simultaneous routing and bu er insertion with restrictions on bu er Locations (1999)
Hai Zhou, D. F. Wong, I-min Liu, Adnan Aziz
During the routing of global interconnects, macro blocks form useful routing regions which allow wires to go through but forbid bu ers to be inserted. They give restrictions on bu er locations. In...
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz
Abstract. A common technique in high-performance hardware design is to intersperse combinatorial logic freely between level-sensitive latch layers (wherein one layer is transparent during the “high...
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz
Abstract. A common technique in high-performance hardware design is to intersperse combinatorial logic freely between level-sensitive latch layers (wherein one layer is transparent during the...
Simultaneous Routing and Buffer Insertion with Restrictions on Buffer Locations (1999)
Hai Zhou, D. F. Wong, I-min Liu, Adnan Aziz
During the routing of global interconnects, macro blocks form useful routing regions which allow wires to go through but forbid buffers to be inserted. They give restrictions on buffer locations. In...
An Efficient Buffer Insertion Algorithm for Large Networks Based on Lagrangian Relaxation (1999)
I-min Liu, Adnan Aziz, D. F. Wong, Hai Zhou
We propose a novel buffer insertion algorithm for handling more general networks, whose underlying topology is a directed acyclic graph rather than just a RC tree. The algorithm finds a global...
Modeling Design Constraints and Biasing in Simulation Using BDDs (1999)
Jun Yuan, Kurt Shultz, Carl Pixley, Hillel Miller, Adnan Aziz
this paper we provide an alternative approach to environment modeling --- we introduce a tool, SimGen, and an associated methodology which employs user-specified constraints to model the interaction...
Formal Verification of a Snoop-based Cache Coherence Protocol using Symbolic Model Checking (1999)
Srivatsan Srinivasan, Parminder Singh Chhabra, Praveen Kumar Jaini, Adnan Aziz, Lizy John
Formal verification of cache coherence in a multiprocessor environment is essential in ascertaining the validity of a cache coherence protocol. Although a number of cache coherence verification...
Enhancing Simulation with BDDs and ATPG (1999)
We introduce SImulation Verification with Augmentation (SIVA), a tool for checking safety properties on digital hardware designs. SIVA integrates simulation with symbolic techniques for vector...
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz
Abstract. A common technique in high-performance hardware design is to intersperse combinatorial logic freely between level-sensitive latch layers (wherein one layer is transparent during the...
Jason Baumgartner, Tamir Heyman, Vigyan Singhal, Adnan Aziz
Abstract. A common technique in high-performance hardware design is to intersperse combinatorial logic freely between level-sensitive latch layers (wherein one layer is transparent during the...
Efficient Coverage Directed State Space Search (1998)
We develop techniques for eciently searching the state space of control dominated hardware designs. Heuristics are used to guide the search to uncovered portions of the state space; mechanisms...
Hybrid verification using saturated simulation (1998)
Adnan Aziz, Jim Kukula, Tom Shiple
Abstract — We develop a verification paradigm called saturated simulation, that is applicable to designs which can be decomposed into a set of interacting controllers. The core procedure is a...
Buffer Minimization in Pass Transistor Logic (1998)
Hai Zhou, Synopsys Inc, Adnan Aziz
With the shrinking feature sizes and increasing transistor counts on chips, the push for higher speed and lower power makes it necessary to look for alternative design styles which offer better...
Hybrid Techniques for Fast Functional Simulation (1998)
Yufeng Luo, Tjahjadi Wongsonegoro, Adnan Aziz
We implement and experiment with techniques for the functional simulation of very large digital systems. We consider techniques that are a hybrid of classical compiled code simulation and recent...
Performance Driven Synthesis for Pass-Transistor Logic (1998)
Tai-Hung Liu, Malay K. Ganai, Adnan Aziz, Jeffrey L. Burns
For many digital designs, implementation in passtransistor logic (PTL) has been shown to be superior in terms of area, timing, and power characteristics to static CMOS. Binary Decision Diagrams...
Simultaneous PTL Buffer Insertion and Sizing for Minimizing Elmore Delay (1998)
Min Liu, Tai-hung Liu, Hai Zhou, Adnan Aziz
For many digital designs, implementation in pass transistor logic (PTL) has been shown to be superior in terms of area, timing, and power characteristics to static CMOS. One problem with PTL circuits...
Buffer Minimization in Pass Transistor Logic (1998)
Since the technical limits of existing circuit families, such as static CMOS, alternative circuit families are pursued for the development of chips that can operate at speeds significantly above 500...
Performance Driven Synthesis for Pass-Transistor Logic (1998)
Tai-Hung Liu, Adnan Aziz, Jeffrey L. Burns
For many digital designs, implementation in pass-transistor logic (PTL) has been shown to be superior in terms of area, timing, and power characteristics to static CMOS. Binary Decision Diagrams...
Buffer Minimization in Pass Transistor Logic (1998)
With the shrinking feature sizes and increasing transistor counts on chips, the push for higher speed and lower power makes it necessary to look for alternative design styles which offer better...
Area-Oriented Synthesis for Pass-Transistor Logic (1998)
Rajat Chaudhry, Tai-Hung Liu, Adnan Aziz, Jeffrey L. Burns
Pass Transistor Logic (PTL) circuits have been successfully used to implement digital ICs which are smaller, faster, and more energy efficient that static CMOS implementations of the same designs....
Implicit State Enumeration for FSMs with Datapaths (1998)
James H. Kukula, Thomas R. Shiple, Adnan Aziz
We show how the classic BDD-based technique of implicit state enumeration for FSMs can be generalized to an automata-based approach for implicit state enumeration of FSMs interacting with datapaths...
Hybrid Verification Using Saturated Simulation (1998)
Adnan Aziz, Jim Kukula, Tom Shiple
We develop a verification paradigm called saturated simulation, that is applicable to designs which can be decomposed into a set of interacting controllers. The core procedure is a symbolic algorithm...
How Powerful is Retiming? (1998)
Hai Zhou, Vigyan Singhal, Adnan Aziz
This paper is about exploring the power of retiming and resynthesis. We show that there exists a pair of "sequentially equivalent" designs so that one cannot be obtained from another by a...
Hybrid verification using saturated simulation (1998)
Adnan Aziz, Jim Kukula, Tom Shiple
Abstract — We develop a verification paradigm called saturated simulation, that is applicable to designs which can be decomposed into a set of interacting controllers. The core procedure is a...
Optimizing Designs Containing Black Boxes (1997)
Tai-hung Liu, Avanti Corp, Adnan Aziz, Vigyan Singhal, Tempus Fugit Inc
We are concerned with optimizing gate-level netlists containing “black boxes”, i.e., components whose functionality is not available to the optimization tool. We establish a notion of equivalence...
On combining formal and informal verification (1997)
Jian Shen, Jacob Abraham, Adnan Aziz
Abstract. We propose algorithms which combine simulation with symbolic methods for the verification of invariants. The motivation is twofold. First, there are designs which are too complex to be...
Optimizing Designs Containing Black Boxes (1997)
Tai-hung Liu, Khurram Sajid, Adnan Aziz, Vigyan Singhal
We define a notion of equivalence for designs containing black boxes i.e., components whose functionality is not known; these arise naturally in the course of hierarchical design. Using this notion,...
Verifying Designs Containing Black Boxes (1997)
Tai-Hung Liu, Khurram Sajid, Adnan Aziz, Vigyan Singhal
We define a notion of equivalence for designs containing black boxes. This notion is applicable to both gate-level designs, as well as designs operating on integer variables. Using this notion, we...
Optimizing Designs Containing Black Boxes (1997)
Tai-Hung Liu, Khurram Sajid, Adnan Aziz, Vigyan Singhal
We define a notion of equivalence for designs containing black boxes i.e., components whose functionality is not known; these arise naturally in the course of hierarchical design. Using this notion,...
Optimizating Designs Containing Black Boxes (1997)
Tai-Hung Liu, Khurram Sajid, Adnan Aziz, Vigyan Singhal.
We define a notion of equivalence for designs containing black boxes. Using this notion, we describe a sound and complete methodology for optimizing designs containing black boxes, i.e. components...
On Combining Formal and Informal Verification (1997)
Jun Yuan, Jian Shen, Jacob Abraham, Adnan Aziz
. We propose algorithms which combine simulation with symbolic methods for the verification of invariants. The motivation is two-fold. First, there are designs which are too complex to be formally...
Formal methods in VLSI system design /--by Adnan Aziz. (1996)
Thesis (Ph. D. in Electrical Engineering and Computer Sciences)--Universisty of California, Berkeley, May 1996.
Vis: A system for verification and synthesis (1996)
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-vincentelli, Fabio Somenzi, Adnan Aziz, Szu-tsung Cheng, ...
Sunil Khatri Yuji Kukimoto Abelardo Pardo y Shaz Qadeer Rajeev K. Ranjan
Vis: A system for verification and synthesis (1996)
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-vincentelli, Fabio Somenzi, Adnan Aziz, Szu-tsung Cheng, ...
Sunil Khatri Yuji Kukimoto Abelardo Pardo y Shaz Qadeer Rajeev K. Ranjan
Vis: A system for verification and synthesis (1996)
Robert K. Brayton, Gary D. Hachtel, Alberto Sangiovanni-vincentelli, Fabio Somenzi, Adnan Aziz, Szu-tsung Cheng, ...
Sunil Khatri Yuji Kukimoto Abelardo Pardo y Shaz Qadeer Rajeev K. Ranjan
VIS: A System for Verification and Synthesis (1996)
Alberto Sangiovanni-Vincentelli, Adnan Aziz, Szu-Tsung Cheng, Stephen Edwards, Sunil Khatri, Yuji Kukimoto, ...
ion Manual abstraction can be performed by giving a file containing the names of variables to abstract. For each variable appearing in the file, a new primary input node is created to drive all the...
Formal Methods in VLSI System Design (1996)
Adnan Aziz, Adnan Aziz, Adnan Aziz
Formal Methods in VLSI System Design by Adnan Aziz Doctor of Philosophy in Engineering -- Electrical Engineering and Computer Sciences University of California at Berkeley Professor Robert K....
Verifying Continuous Time Markov Chains (1996)
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, Robert Brayton
. We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov...
It usually works: The temporal logic of stochastic systems (1995)
Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton
is defined. pCTL expresses quantitative bounds on the probabilities of correct behavior; it can be interpreted over discrete Markov processes. A bisimulation relation is defined on finite Markov...
Efficient BDD Algorithms for FSM Synthesis and Verification (1995)
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley
We describe a set of BDD based algorithms for efficient FSM synthesis and verification. We establish that the core computation in both synthesis and verification is forming the image and pre-image of...
Sequential Synthesis Using S1S (1995)
Adnan Aziz, Felice Balarin, Robert Brayton, Alberto Sangiovanni-Vincentelli
In this paper we propose the use of the logic S1S as a mathematical framework for studying the synthesis of sequential designs. We will show that this will lead to simple, rigorous, and constructive...
Exploiting Power-up Delay for Sequential Optimization (1995)
Vigyan Singhal, Carl Pixley, Adnan Aziz, Robert K. Brayton
Recent work has identified the notion of safe replacement for sequential synchronous designs that may not have reset hardware or even explicitly known initial states. Safe replacement requires that a...
Timing-Safe Replaceability for Combinational Designs (1995)
Adnan Aziz, Robert K. Brayton, Felice Balarin, Vigyan Singhal
This paper addresses the problem of verifying that a combinational design is a timing-safe replacement for an existing design without making any assumptions about the environment of the design. A...
Multi-level Synthesis for Safe Replaceability (1994)
Carl Pixley, Vigyan Singhal, Adnan Aziz, Robert K. Brayton
We describe the condition that a sequential digital design is a safe replacement for an existing design without making any assumptions about a known initial state of the design or about its...
Equivalences for fair kripke structures (1994)
Adnan Aziz, Vigyan Singhal, Felice Balarin
Abstract. We extend the notion of bisimulation to Kripke structures with fairness. We define equivalences that preserve fairness and are akin to bisimulation. Specifically we define an equivalence...
BDD variable ordering for interacting finite state machines (1994)
Adnan Aziz, Serdar Tas, Robert K. Brayton
We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting nite state machines (FSMs). Orderings are derived from the communication structure...
Multi-level Synthesis for Safe Replaceability (1994)
Carl Pixley, Vigyan Singhal, Adnan Aziz, Robert K. Brayton
We describe the condition that a sequential digital design is a safe replacement for an existing design without making any assumptions about a known initial state of the design or about its...
Synthesizing Interacting Finite State Machines (1994)
Adnan Aziz, Felice Balarin, Robert K. Brayton, Alberto Sangiovanni-vincentelli
We present a mathematical framework for analyzing the synthesis of interacting finite state systems. The logic S1S is used to derive simple, rigorous, and constructive solutions to problems in...
Adnan Aziz, Vigyan Singhal, Gitanjali M. Swamy, Robert K. Brayton
We address the problem of compositional minimization of collections of interacting finite state machines that arise in the context of formal verification of hardware designs by language containment....
Formula-Dependent Equivalence for Compositional CTL Model Checking (1994)
Adnan Aziz, Thomas R. Shiple, Vigyan Singhal
. We present a state equivalence that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser...
Efficient Formal Design Verification: Data Structure + Algorithms (1994)
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Bernard Plessier, Carl Pixley
We describe a data structure and a set of BDD based algorithms for efficient formal design verification. We argue that hardware designs should be translated into an intermediate hierarchical netlist...
BDD Variable Ordering for Interacting Finite State Machines (1994)
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
We address the problem of obtaining good variable orderings for the BDD representing the transition relation of a system of interacting finite state machines. We obtain orderings based only on the...
Equivalences for fair Kripke structures (1994)
Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton
. We extend the notion of bisimulation to Kripke structures with fairness. We define equivalences that preserve fairness and are akin to bisimulation. Specifically we define an equivalence and show...
BDD Variable Ordering for Interacting Finite State Machines (1994)
Adnan Aziz, Serdar Tasiran, Robert K. Brayton
We address the problem of obtaining good variable orderings for the BDD representation of a system of interacting finite state machines (FSMs). Orderings are derived from the communication structure...
Formal Design Verification of Digital Systems (1993)
Thomas Shiple, Adnan Aziz, Felice Balarin, Szu-Tsung Cheng, Ramin Hojati, Timothy Kam, ...
We address the problem of formally proving properties of digital sequential systems. Specifically, our research is focused on building an integrated framework, called HSIS, for supporting automatic...
Verifying Interacting Finite State Machines : Complexity Issues (1993)
Adnan Aziz, Vigyan Singhal, Robert K. Brayton
. In this report we carry out a computational complexity analysis of a simple model of concurrency consisting of interacting finite state machines with fairness constraints (IFSMs). This model is...
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal
. The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for...
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal
. The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for...