1 
The Binary Decision Diagram: Formal Verification of a Reference ImplementationRumreich, Laine 04 October 2021 (has links)
No description available.

2 
The Binary Decision Diagram: Abstraction and ImplementationAsim, Saad F., Asim 14 August 2018 (has links)
No description available.

3 
Formal Verification Techniques for Reversible CircuitsLimaye, Chinmay Avinash 27 June 2011 (has links)
As the number of transistors per unit chip area increases, the power dissipation of the chip becomes a bottleneck. New nanotechnology materials have been proposed as viable alternatives to CMOS to tackle area and power issues. The power consumption can be minimized by the use of reversible logic instead of conventional combinational circuits. Theoretically, reversible circuits do not consume any power (or consume minimal power) when performing computations. This is achieved by avoiding information loss across the circuit. However, use of reversible circuits to implement digital logic requires development of new Electronic Design Automation techniques. Several approaches have been proposed and each method has its own pros and cons. This often results in multiple designs for the same function. Consequently, this demands research in efficient equivalence checking techniques for reversible circuits.
This thesis explores the optimization and equivalence checking of reversible circuits. Most of the existing synthesis techniques work in two steps — generate an original, often suboptimal, implementation for the circuit followed optimization of this design. This work proposes the use of Binary Decision Diagrams for optimization of reversible circuits. The proposed technique identifies repeated gate (trivial) as well as noncontiguous redundancies in a reversible circuit. Construction of a BDD for a subcircuit (obtained by sliding a window of fixed size over the circuit) identifies redundant gates based upon the redundant variables in the BDD. This method was unsuccessful in identifying any additional redundancies in benchmark circuits; however, hidden noncontiguous redundancies were consistently identified for a family of randomly generated reversible circuits. As of now, several research groups focus upon efficient synthesis of reversible circuits. However, little work has been done in identification of redundant gates in existing designs and the proposed peephole optimization method stands among the few known techniques. This method fails to identify redundancies in a few cases indicating the complexity of the problem and the need for further research in this area.
Even for simple logical functions, multiple circuit representations exist which exhibit a large variation in the total number of gates and circuit structure. It may be advantageous to have multiple implementations to provide flexibility in choice of implementation process but it is necessary to validate the functional equivalence of each such design. Equivalence checking for reversible circuits has been researched to some extent and a few preprocessing techniques have been proposed prior to this work. One such technique involves the use of Reversible Miter circuits followed by SATsolvers to ascertain equivalence. The second half of this work focuses upon the application of the proposed reduction technique to Reversible Miter circuits as a preprocessing step to improve the efficiency of the subsequent SATbased equivalence checking. / Master of Science

4 
Logic Synthesis of HighPerformance Combinational Circuits Based on PassTransistor Cell LibraryWen, ChiaSheng 02 September 2003 (has links)
This thesis proposes a new variableorder prediction method to predict the Shannon expansion order during the BDD tree generator. Combining this method with the original minimum width method, we can generator a better BDD tree to be used in our passtransistor logic synthesizer. Also we propose two partitioning methods to reduce the length of the critical paths. The first method can effectively reduce the critical path delay at the cost of much higher area cost. The second method explores the common factors in the Boolean functions to reduce the critical path delay with reasonably increased area cost. Furthermore, we discuss the methods of inserting regenerating inverters/buffers along the path in BDD tree by selecting inverter cells and MUX cells of proper driving strength to optimize the area/cost/power performance. Finally, the automatic layout generation is considered to produce the physical layout more efficiently compared with that using commericial automatic placeandroute tools.

5 
Approaches to test set generation using binary decision diagramsWingfield, James 30 September 2004 (has links)
This research pursues the use of powerful BDDbased functional circuit analysis to evaluate some approaches to test set generation. Functional representations of the circuit allow the measurement of information about faults that is not directly available through circuit simulation methods, such as probability of random detection and testspace overlap between faults. I have created a software tool that performs experiments to make such measurements and augments existing test generation strategies with this new information. Using this tool, I explored the relationship of fault model difficulty to test set length through fortuitous detection, and I experimented with the application of functionbased methods to help reconcile the traditionally opposed goals of making test sets that are both smaller and more effective.

6 
Automated system design optimisationAstapenko, D. January 2010 (has links)
The focus of this thesis is to develop a generic approach for solving reliability design optimisation problems which could be applicable to a diverse range of real engineering systems. The basic problem in optimal reliability design of a system is to explore the means of improving the system reliability within the bounds of available resources. Improving the reliability reduces the likelihood of system failure. The consequences of system failure can vary from minor inconvenience and cost to significant economic loss and personal injury. However any improvements made to the system are subject to the availability of resources, which are very often limited. The objective of the design optimisation problem analysed in this thesis is to minimise system unavailability (or unreliability if an unrepairable system is analysed) through the manipulation and assessment of all possible design alterations available, which are subject to constraints on resources and/or system performance requirements. This thesis describes a genetic algorithmbased technique developed to solve the optimisation problem. Since an explicit mathematical form can not be formulated to evaluate the objective function, the system unavailability (unreliability) is assessed using the fault tree method. Central to the optimisation algorithm are newly developed fault tree modification patterns (FTMPs). They are employed here to construct one fault tree representing all possible designs investigated, from the initial system design specified along with the design choices. This is then altered to represent the individual designs in question during the optimisation process. Failure probabilities for specified design cases are quantified by employing Binary Decision Diagrams (BDDs). A computer programme has been developed to automate the application of the optimisation approach to standard engineering safety systems. Its practicality is demonstrated through the consideration of two systems of increasing complexity; first a High Integrity Protection System (HIPS) followed by a Fire Water Deluge System (FWDS). The technique is then furtherdeveloped and applied to solve problems of multiphased mission systems. Two systems are considered; first an unmanned aerial vehicle (UAV) and secondly a military vessel. The final part of this thesis focuses on continuing the development process by adapting the method to solve design optimisation problems for multiple multiphased mission systems. Its application is demonstrated by considering an advanced UAV system involving multiple multiphased flight missions. The applications discussed prove that the technique progressively developed in this thesis enables design optimisation problems to be solved for systems with different levels of complexity. A key contribution of this thesis is the development of a novel generic optimisation technique, embedding newly developed FTMPs, which is capable of optimising the reliability design for potentially any engineering system. Another key and novel contribution of this work is the capability to analyse and provide optimal design solutions for multiple multiphase mission systems. Keywords: optimisation, system design, multiphased mission system, reliability, genetic algorithm, fault tree, binary decision diagram

7 
Improvements to FieldProgrammable Gate Array Design Efficiency using Logic SynthesisLing, Andrew Chaang 18 February 2010 (has links)
As FieldProgrammable Gate Array (FPGA) capacity can now support several processors on a single device, the scalability of FPGA design tools and methods has emerged as a major obstacle for the wider use of FPGAs. For example, logic synthesis, which has traditionally been the fastest step in the FPGA ComputerAided Design (CAD) flow, now takes several hours to complete in a typical FPGA compile. In this work, we address this problem by focusing on two areas. First, we revisit FPGA logic synthesis and attempt to improve its scalability. Specifically, we look at a binary decision diagram (BDD) based logic synthesis flow, referred to as FBDD, where we improve its runtime by several fold with a marginal impact to the resulting circuit area. We do so by speeding up the classical cut generation problem by an orderofmagnitude which enables its application directly at the logic synthesis level. Following this, we introduce a guided partitioning technique using a fast global budgeting formulation, which enables us to optimize individual “pockets” within the circuit without degrading the overall circuit performance. By using partitioning we can significantly reduce the solution space of the logic synthesis problem and, furthermore, open up the possibility of parallelizing the logic synthesis step.
The second area we look at is the area of Engineering Change Orders (ECOs). ECOs are incremental modifications to a design late in the design flow. This is beneficial since
it is minimally disruptive to the existing circuit which preserves much of the engineering effort invested previously in the design. In a design flow where most of the steps are fully automated, ECOs still remain largely a manual process. This can often tie up a designer for weeks leading to missed project deadlines which is very detrimental to products whose lifecycle can span only a few months. As a solution to this, we show how we can leverage existing logic synthesis techniques to automatically modify a circuit in a minimally disruptive manner. This can significantly reduce the turnaround time when applying ECOs.

8 
Improvements to FieldProgrammable Gate Array Design Efficiency using Logic SynthesisLing, Andrew Chaang 18 February 2010 (has links)
As FieldProgrammable Gate Array (FPGA) capacity can now support several processors on a single device, the scalability of FPGA design tools and methods has emerged as a major obstacle for the wider use of FPGAs. For example, logic synthesis, which has traditionally been the fastest step in the FPGA ComputerAided Design (CAD) flow, now takes several hours to complete in a typical FPGA compile. In this work, we address this problem by focusing on two areas. First, we revisit FPGA logic synthesis and attempt to improve its scalability. Specifically, we look at a binary decision diagram (BDD) based logic synthesis flow, referred to as FBDD, where we improve its runtime by several fold with a marginal impact to the resulting circuit area. We do so by speeding up the classical cut generation problem by an orderofmagnitude which enables its application directly at the logic synthesis level. Following this, we introduce a guided partitioning technique using a fast global budgeting formulation, which enables us to optimize individual “pockets” within the circuit without degrading the overall circuit performance. By using partitioning we can significantly reduce the solution space of the logic synthesis problem and, furthermore, open up the possibility of parallelizing the logic synthesis step.
The second area we look at is the area of Engineering Change Orders (ECOs). ECOs are incremental modifications to a design late in the design flow. This is beneficial since
it is minimally disruptive to the existing circuit which preserves much of the engineering effort invested previously in the design. In a design flow where most of the steps are fully automated, ECOs still remain largely a manual process. This can often tie up a designer for weeks leading to missed project deadlines which is very detrimental to products whose lifecycle can span only a few months. As a solution to this, we show how we can leverage existing logic synthesis techniques to automatically modify a circuit in a minimally disruptive manner. This can significantly reduce the turnaround time when applying ECOs.

9 
Advances in Functional Decomposition: Theory and ApplicationsMartinelli, Andres January 2006 (has links)
Functional decomposition aims at finding efficient representations for Boolean functions. It is used in many applications, including multilevel logic synthesis, formal verification, and testing. This dissertation presents novel heuristic algorithms for functional decomposition. These algorithms take advantage of suitable representations of the Boolean functions in order to be efficient. The first two algorithms compute simpledisjoint and disjointsupport decompositions. They are based on representing the target function by a Reduced Ordered Binary Decision Diagram (BDD). Unlike other BDDbased algorithms, the presented ones can deal with larger target functions and produce more decompositions without requiring expensive manipulations of the representation, particularly BDD reordering. The third algorithm also finds disjointsupport decompositions, but it is based on a technique which integrates circuit graph analysis and BDDbased decomposition. The combination of the two approaches results in an algorithm which is more robust than a purely BDDbased one, and that improves both the quality of the results and the running time. The fourth algorithm uses circuit graph analysis to obtain nondisjoint decompositions. We show that the problem of computing nondisjoint decompositions can be reduced to the problem of computing multiplevertex dominators. We also prove that multiplevertex dominators can be found in polynomial time. This result is important because there is no known polynomial time algorithm for computing all nondisjoint decompositions of a Boolean function. The fifth algorithm provides an efficient means to decompose a function at the circuit graph level, by using information derived from a BDD representation. This is done without the expensive circuit resynthesis normally associated with BDDbased decomposition approaches. Finally we present two publications that resulted from the many detours we have taken along the winding path of our research.

10 
Safety system design optimisationPattison, Rachel Lesley January 2000 (has links)
This thesis investigates the efficiency of a design optimisation scheme that is appropriate for systems which require a high likelihood of functioning on demand. Traditional approaches to the design of safety critical systems follow the preliminary design, analysis, appraisal and redesign stages until what is regarded as an acceptable design is achieved. For safety systems whose failure could result in loss of life it is imperative that the best use of the available resources is made and a system which is optimal, not just adequate, is produced. The object of the design optimisation problem is to minimise system unavailability through manipulation of the design variables, such that limitations placed on them by constraints are not violated. Commonly, with mathematical optimisation problem; there will be an explicit objective function which defines how the characteristic to be minimised is related to the variables. As regards the safety system problem, an explicit objective function cannot be formulated, and as such, system performance is assessed using the fault tree method. By the use of house events a single fault tree is constructed to represent the failure causes of each potential design to overcome the time consuming task of constructing a fault tree for each design investigated during the optimisation procedure. Once the fault tree has been constructed for the design in question it is converted to a BDD for analysis. A genetic algorithm is first employed to perform the system optimisation, where the practicality of this approach is demonstrated initially through application to a HighIntegrity Protection System (HIPS) and subsequently a more complex Firewater Deluge System (FDS). An alternative optimisation scheme achieves the final design specification by solving a sequence of optimisation problems. Each of these problems are defined by assuming some form of the objective function and specifying a subregion of the design space over which this function will be representative of the system unavailability. The thesis concludes with attention to various optimisation techniques, which possess features able to address difficulties in the optimisation of safety critical systems. Specifically, consideration is given to the use of a statistically designed experiment and a logical search approach.

Page generated in 0.1481 seconds