Intro
Preface
Contents
Arithmetic Satisfiability-Modulo-Theory Solving Applied to Non-Standard Analysis Problems of Cyber-Physical Systems
1 Introduction
2 iSAT and SiSAT
3 Sample Applications
3.1 Exact Monitoring of Cyber-Physical Systems Under Uncertainty
3.2 Quantitative Safety Analysis of BCI-Enabled Autonomous Systems
4 Conclusion
References
Fast AIG-Based Approximate Logic Synthesis
1 Introduction
2 Related Work
3 Background
3.1 Notation and Conventions
3.2 (XOR-)AND-Inverter Graphs
3.3 Error Metrics

4 Fast AIG Approximate Logic Synthesis
4.1 Bucket-Based Approximation Algorithm
4.2 Approximation Operations
4.3 Fast Computation of the Weighted Hamming Distance
4.4 Truth Density Computation
5 Experimental Evaluation
5.1 Experimental Setup
5.2 Scalability
5.3 Multi-Objective Optimization for Area and `3́9`42`""̇613A``45`47`""603Awhd
5.4 Truth Density Computation
6 Conclusion and Outlook
References
External Don't Cares in Logic Synthesis
1 Introduction
2 Background and Terminologies
2.1 Boolean Functions and Boolean Relations

2.2 Logic Networks and Functions in a Network
2.3 Don't-Care Conditions
3 Computation of Internal Don't Cares
4 Definition and Representation of External Don't Cares
4.1 External Controllability Don't Cares (External SDCs)
4.2 External Observability Don't Cares
4.3 Logic Synthesis from a Boolean Relation Perspective
4.4 Boolean Relation as Unified Representation of External Don't Cares
5 Optimization with External Don't Cares
6 Experimental Demonstration
7 Conclusion and Future Work
7.1 Multi-Target Resynthesis

7.2 Propagation and Management of Observability Equivalence Classes
References
Maiorana-McFarland Boolean Bent Functions Characterized by their Reed-Muller Spectra
1 Introduction
2 Formalisms
3 The Effect of a Subset of Spectral Invariant Operations
4 Closing Remarks
References
Toward System-Level Assertions for Heterogeneous Systems
1 Introduction
2 Related Work
3 Preliminaries
3.1 Assertion-Based Verification
3.2 System-Level Running Example
3.3 Assertions for System-Level Running Example
4 System-Level Assertions Library for Heterogeneous Systems

4.1 Overview
4.2 Application Programming Interface
4.3 Boolean Layer
4.4 Sequence Layer
4.4.1 Delay Operator
4.4.2 Repeat Operator
4.4.3 Sequence ``and/or'' Operators
4.5 Property Layer
4.5.1 Implication Operator
4.6 Verification Layer
5 Experiments
6 Conclusion
References
SAT-Based Key Determination Attack for Improving the Quality Assessment of Logic Locking Mechanisms
1 Introduction
2 Preliminaries
2.1 Reconfigurable Field-Effect Transistors
2.2 Boolean Satisfiability Problem
2.3 SAT-Based Attacks