Exploiting Logic Properties to Speedup SAT
In this chapter, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check determines if a
- PDF / 4,825,079 Bytes
- 162 Pages / 467.717 x 683.15 pts Page_size
- 27 Downloads / 265 Views
New Data Structures and Algorithms for Logic Synthesis and Verification
New Data Structures and Algorithms for Logic Synthesis and Verification
Luca Gaetano Amaru
New Data Structures and Algorithms for Logic Synthesis and Verification
123
Luca Gaetano Amaru Synopsys Inc. Santa Clara, CA USA
ISBN 978-3-319-43173-4 DOI 10.1007/978-3-319-43174-1
ISBN 978-3-319-43174-1
(eBook)
Library of Congress Control Number: 2016946018 © Springer International Publishing Switzerland 2017 This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissions that may have been made. Printed on acid-free paper This Springer imprint is published by Springer Nature The registered company is Springer International Publishing AG Switzerland
Success is not final, failure is not fatal: It is the courage to continue that counts. —Winston Churchill
To my parents
Preface
The strong interaction between Electronic Design Automation (EDA) tools and Complementary Metal-Oxide Semiconductor (CMOS) technology contributed substantially to the advancement of modern digital electronics. The continuous downscaling of CMOS Field Effect Transistor (FET) dimensions enabled the semiconductor industry to fabricate digital systems with higher circuit density at reduced costs. To keep pace with technology, EDA tools are challenged to handle both digital designs with growing functionality and device models of increasing complexity. Nevertheless, while the downscaling of CMOS technology requires more complex physical design models, the logic abstraction of a transistor as a switch has not changed even with the introduction of 3D FinFET technology. As a consequence, modern EDA tools are fine-tuned for CMOS technology and the underlying design methodologies are based on CMOS logic primitives, i.e., negative unate logic functions. While it is clear that CMOS logic primitives will be the ultimate building blocks for digital systems in the next 10 years, no evidence is provided that CMOS logic primitives are also the optimal basis for EDA software. In EDA, the effi
Data Loading...
