Cover Image

New data structures and algorithms for logic synthesis and verification

This book introduces new logic primitives for electronic design automation tools. The author approaches fundamental EDA problems from a different, unconventional perspective, in order to demonstrate the key role of rethinking EDA solutions in overcoming technological limitations of present and futur...

Full description

Main Author: Amaru, Luca Gaetano,
Other Authors: SpringerLink (Online service)
Format: eBook
Language: English
Published: Switzerland : Springer, [2016]
Physical Description: 1 online resource (xvi, 156 pages) : illustrations (some color)
Subjects:
Data structures (Computer science)
Logic circuits.
Table of Contents:
  • Preface
  • Acknowledgments
  • Contents
  • 1 Introduction
  • 1.1 Electronic Design Automation
  • 1.2 Modern EDA Tools and Their Logic Primitives
  • 1.2.1 Logic Synthesis
  • 1.2.2 Formal Methods
  • 1.3 Research Motivation
  • 1.3.1 Impact on Modern CMOS Technology
  • 1.3.2 Impact on Beyond CMOS Technologies
  • 1.4 Contributions and Position with Respect to Previous Work
  • 1.4.1 Logic Representation, Manipulation and Optimization
  • 1.4.2 Boolean Satisfiability and Equivalence Checking
  • 1.5 Book Organization
  • References
  • Part I Logic Representation, Manipulation and Optimization
  • 2 Biconditional Logic
  • 2.1 Introduction
  • 2.2 Background and Motivation
  • 2.2.1 Binary Decision Diagrams
  • 2.2.2 Emerging Technologies
  • 2.3 Biconditional Binary Decision Diagrams
  • 2.3.1 Biconditional Expansion
  • 2.3.2 BBDD Structure and Ordering
  • 2.3.3 BBDD Reduction
  • 2.3.4 BBDD Complemented Edges
  • 2.3.5 BBDD Manipulation
  • 2.4 BBDD Representation: Theoretical and Experimental Results
  • 2.4.1 Theoretical Results
  • 2.4.2 Experimental Results
  • 2.5 BBDD-based Synthesis and Verification
  • 2.5.1 Logic Synthesis
  • 2.5.2 Formal Equivalence Checking
  • 2.5.3 Case Study: Design of an Iterative Product Code Decoder
  • 2.6 BBDDs as Native Design Abstraction for Nanotechnologies
  • 2.6.1 Reversible Logic
  • 2.6.2 NEMS
  • 2.7 Summary
  • References
  • 3 Majority Logic
  • 3.1 Introduction
  • 3.2 Background and Motivation
  • 3.2.1 Logic Representation
  • 3.2.2 Logic Optimization
  • 3.2.3 Notations and Definitions
  • 3.3 Majority-Inverter Graphs
  • 3.3.1 MIG Logic Representation
  • 3.3.2 MIG Boolean Algebra
  • 3.3.3 Inserting Safe Errors in MIG
  • 3.4 MIG Algebraic Optimization
  • 3.4.1 Size-Oriented MIG Algebraic Optimization
  • 3.4.2 Depth-Oriented MIG Algebraic Optimization
  • 3.4.3 Switching Activity-Oriented MIG Algebraic Optimization.
  • 3.5 MIG Boolean Optimization
  • 3.5.1 Identifying Advantageous Orthogonal Errors in MIGs
  • 3.5.2 Depth-Oriented MIG Boolean Optimization
  • 3.5.3 Size-Oriented MIG Boolean Optimization
  • 3.6 Experimental Results
  • 3.6.1 Methodology
  • 3.6.2 Optimization Case Study: Adders
  • 3.6.3 General Optimization Results
  • 3.6.4 ASIC Results
  • 3.6.5 FPGA Results
  • 3.7 MIGs as Native Design Abstraction for Nanotechnologies
  • 3.7.1 MIG-Based Synthesis
  • 3.7.2 Spin-Wave Devices
  • 3.7.3 Resistive RAM
  • 3.8 Extension to MAJ-n Logic
  • 3.8.1 Generic MAJ-n/INV Axioms
  • 3.8.2 Soundness
  • 3.8.3 Completeness
  • 3.9 Summary
  • References
  • Part II Logic Satisfiability and Equivalence Checking
  • 4 Exploiting Logic Properties to Speedup SAT
  • 4.1 Introduction
  • 4.2 Background and Motivation
  • 4.2.1 Notation
  • 4.2.2 Tautology Checking
  • 4.2.3 Motivation
  • 4.3 Properties of Logic Circuits
  • 4.4 From Tautology to Contradiction and Back
  • 4.4.1 Boolean SAT and Tautology/Contradiction Duality
  • 4.5 Experimental Results
  • 4.5.1 Verification of SAT Solving Advantage on the Dual Circuit
  • 4.5.2 Results for Concurrent Regular/Dual SAT Execution
  • 4.6 Summary
  • References
  • 5 Majority Normal Form Representation and Satisfiability
  • 5.1 Introduction
  • 5.2 Background and Motivation
  • 5.2.1 Notations and Definitions
  • 5.2.2 Two-Level Logic Representation
  • 5.2.3 Satisfiability
  • 5.3 Two-Level Majority Representation Form
  • 5.3.1 Majority Normal Form Definition and Properties
  • 5.3.2 Representation Examples with DNF, CNF and MNF
  • 5.4 Majority Satisfiability
  • 5.4.1 Complexity of Unrestricted MNF-SAT
  • 5.4.2 Complexity of Some Restricted MNF-SAT
  • 5.5 Algorithm to Solve MNF-SAT
  • 5.5.1 One-Level Majority-SAT
  • 5.5.2 Decide Strategy for MNF-SAT
  • 5.6 Discussion and Future Work
  • 5.7 Summary
  • References.
  • 6 Improvements to the Equivalence Checking of Reversible Circuits
  • 6.1 Introduction
  • 6.2 Background
  • 6.2.1 Reversible Circuits
  • 6.2.2 Boolean Satisfiability
  • 6.3 Mapping Combinational Equivalence Checking for Reversible Circuits to XOR-CNF SAT
  • 6.3.1 Creating an Identity Miter
  • 6.3.2 XOR-CNF Formulation
  • 6.4 Experimental Results
  • 6.4.1 Methodology and Setup
  • 6.4.2 Results
  • 6.5 Discussion
  • 6.5.1 Application to the Verification of Conventional Circuits
  • 6.5.2 Easy Exploitation of Parallelism
  • 6.6 Summary
  • References
  • 7 Conclusions
  • 7.1 Overview of Book Contributions
  • 7.2 Open Problems
  • 7.3 Concluding Remarks
  • References
  • Index.

In Prospector

Similar Items