| Nota di contenuto |
Intro -- Preface -- Contents -- Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey -- 1 Introduction -- 2 Circuit Verification Using Computer Algebra -- 2.1 Multiplier Circuits -- 2.2 Algebra -- 2.3 Circuit Verification Using Computer Algebra -- 2.4 Algebraic Proof Systems -- 3 Verification Tools -- 3.1 Algebraic RewriTing in ABC CiesielskiYuBrownLiuRossi-DAC15,YuBrownLiuRossiCieslieski-TCAD16,YuCiesielskiMishchenko-TCAD17,CiesielskiSuYasinYu-TCAD19 -- 3.2 AMulet KaufmannBiereKauers-FMCAD19 -- 3.3 PolyCleaner MahzoonGrosseDrechsler-ICCAD18 -- 3.4 RevSCA/RevSCA-2.0 MahzoonGrosseDrechsler-DAC19 -- 3.5 DyPoSub MahzoonGrosseSchollDrechsler-DATE20 -- 4 Benchmark Generators -- 4.1 Arithmetic Module Generator -- 4.2 GenMul -- 4.3 MultGen -- 4.4 EPFL Combinational Benchmark Suite -- 4.5 ABC/Boolector -- 4.6 Processing Verilog Benchmarks -- 4.7 Optimizing Benchmarks -- 5 Evaluation -- 5.1 Arithmetic Module Generator -- 5.2 GenMul -- 5.3 MultGen -- 5.4 EPFL Combinational Benchmark Suite -- 5.5 ABC/Boolector -- 5.6 Optimized Benchmarks -- 5.7 Proof Generation -- 6 Conclusion -- References -- The Vital Role of Machine Learning in Developing Emerging Technologies -- 1 Introduction -- 1.1 Machine Learning Transistor Model -- 1.2 Machine Learning Standard Cell Model -- 2 Related Work -- 3 Background -- 3.1 Compact Models -- 3.2 Negative Capacitance FinFET -- 3.3 Transistor Characteristics -- 4 Our Machine Learning Transistor Model -- 4.1 Experimental Setup -- 4.2 Data Scaling -- 4.3 Advantages of NN-Based Transistor Modeling -- 4.4 Disadvantages of NN-Based Transistor Modeling -- 4.5 Inference Accuracy and Training Time -- 4.6 Traditional Fitness Compared to Transistor Metric Fitness -- 4.7 Early Evaluation with Limited Data -- 4.8 Modeling NC-FinFET with NN-Based Transistor Models.
5 Our Proposed Machine Learning-Based Approach -- 5.1 ML for Library Characterization -- 5.1.1 Generation of Training Data -- 5.1.2 Training of ML Estimators -- 5.2 Design Technology Co-Optimization for NC-FinFET -- 6 Evaluation and Experimental Results -- 6.1 Accuracy of Cell Library Prediction -- 6.2 Accuracy of Prediction on System Level -- 6.3 DTCO Parameter Optimization -- 6.4 Improvement in Performance -- 7 Conclusion -- References -- Fast Optimal Synthesis of Symmetric Index Generation Functions -- 1 Introduction -- 2 Preliminaries -- 3 Linearity, Orthogonality, and Circuit Structures -- 4 The Task to Solve and the Used Approach -- 5 Analysis of the Properties of the Reverse Task -- 5.1 Trivial Solution for t=1 -- 5.2 Smallest Optimal Circuits L for a Fixed Value of t -- 5.3 Regions of Restrictions -- 5.4 Repeated Use of the Smallest Optimal Circuits -- 5.5 Missing Values nmax for Odd Values of t -- 5.6 Missing Values nmax for Even Values of t -- 5.7 Summary of the Analysis -- 6 Algorithms to Compute pmin and nmax -- 7 Experimental Results -- 8 Conclusion and Future Work -- References -- Axiomatizing Boolean Differentiation -- 1 Introduction -- 1.1 Our Approach -- 1.2 Applications of Axiomatizing Boolean Differentiation -- 1.3 Outline -- 2 Model-Theoretic Fundamentals -- 3 Axiomatizing=3=3= Boolean Differentiation -- 3.1 Boolean Functions, Rings, and Derivations -- 3.2 A Complete Axiomatization -- 4 Relationship to Finite Models and Immediate Consequences -- 5 Future Applications and Perspectives -- References -- Construction of Binary Bent Functions by FFT-Like Permutation Algorithms -- 1 Introduction -- 2 Walsh Transform -- 3 Spectral Invariant Operations in the Walsh Domain -- 4 Bent Functions and Walsh Transform -- 5 Essence of FFT -- 6 Permutation Matrices -- 7 Illustrative Examples -- 8 Algorithm for Constructing Bent Functions.
9 Closing Remarks -- References -- Nonlinear Codes for Test Patterns Compression: The Old School Way -- 1 Introduction -- 2 Proposed Approach -- 2.1 Expander Outputs as a Clique Cover Problem -- 2.2 Compatibility Graph Properties -- 2.3 Techniques for Minimum Clique Cover -- 2.4 Expander Input as an MV-Encoding Problem -- 2.5 Method Summary -- 3 Results -- 3.1 Implementation -- 3.2 Resulting Codes -- 3.3 Is Optimum MV Encoding Important? -- 3.4 Expander Synthesis -- 4 Future Directions -- 5 Conclusions -- References -- Translation Techniques for Reversible Circuit Synthesis with Positive and Negative Controls -- 1 Introduction -- 2 Background -- 2.1 Reversible Functions, Gates, and Circuits -- 2.2 Quantum Gates and Circuits -- 3 Function Translations -- 3.1 Function Inverse -- 3.2 Input-Output Negation -- 3.3 Input-Output Permutation -- 4 Transformation-Based Synthesis -- 5 Simplifying a Reversible Circuit -- 6 Mapping a Reversible Circuit to a Quantum Circuit -- 6.1 Negative Control CNOTs -- 6.2 NCV Realization of MPMCT Gates -- 6.3 MPP and MPIP Gate Cost and Substitution -- 6.4 Overall Simplification and Mapping Strategy -- 7 Experimental Results -- 8 Heuristic Selection of Function Translations -- 9 Discussion and Future Work -- References -- Hybrid Control of Toffoli and Peres Gates -- 1 Introduction -- 2 Hybrid-Controlled Gates -- 3 Scalability -- 4 Closing Remark -- References -- GenMul: Generating Architecturally Complex Multipliers to Challenge Formal Verification Tools -- 1 Introduction -- 2 Preliminaries -- 2.1 Multiplier Architectures -- 2.2 SCA Basics -- 2.3 SCA-Based Verification -- 3 Multiplier Generator GenMul -- 3.1 Overview and Data Structures -- 3.2 Generation of Multipliers -- 4 Challenges of Verifying Multipliers -- 5 Conclusion -- Appendix -- GenMulWebsite -- References -- Index.
|
Info
Enhanced virtual prototyping : featuring RISC-V case studies / / Vladimir Herdt, Daniel Grosse, Rolf Drechsler
