ebook ebooks e-book e-books downloaden bei MyEbooks.ch downloaden

Design and Verification of Microprocessor Systems for High-Assurance Applications

:	Torben Amtoft, Selly Browning, Jared Davis, Anthony C. J. Fox, David A. Greve, Michael J. C. Gordon
:	David S. Hardin
:	Design and Verification of Microprocessor Systems for High-Assurance Applications
:	Springer-Verlag
:	9781441915399
:	1
:	CHF 96.70
:

:	Elektronik, Elektrotechnik, Nachrichtentechnik
:	English

:	436
:	Wasserzeichen/DRM
:	PC/MAC/eReader/Tablet
:	PDF

Microprocesso s increasingly control and monitor our most critical systems, including automobiles, airliners, medical systems, transportation grids, and defense systems. The relentless march of semiconductor process technology has given engineers exponentially increasing transistor budgets at constant recurring cost. This has encouraged increased functional integration onto a single die, as well as increased architectural sophistication of the functional units themselves. Additionally, design cycle times are decreasing, thus putting increased schedule pressure on engineers. Not surprisingly, this environment has led to a number of uncaught design flaws. Traditional simulation-based design verification has not kept up with the scale or pace of modern microprocessor system design. Formal verification methods offer the promise of improved bug-finding capability, as well as the ability to establish functional correctness of a detailed design relative to a high-level specification. However, widespread use of formal methods has had to await breakthroughs in automated reasoning, integration with engineering design languages and processes, scalability, and usability.

This book presents several breakthrough design and verification techniques that allow these powerful formal methods to be employed in the real world of high-assurance microprocessor system design.

	Preface	6
	Contents	9
	ACL2 and Its Applications to Digital System Verification	13
	1 Introduction	13
	2 Some Basic Decisions	13
	3 ACL2	15
	3.1 A Programming Language	16
	3.2 A Logical Theory	18
	3.3 A Mechanical Theorem Prover and Proof Environment	20
	3.4 Efficiency	22
	4 A Simple Microprocessor Model	23
	5 Variations on the Theme	29
	6 Summary	30
	References	31
	A Mechanically Verified Commercial SRT Divider	34
	1 Introduction	34
	2 SRT Division	37
	3 Quotient Digit Selection	42
	4 Implementation	47
	4.1 Analysis of Operands	48
	4.2 Iteration	52
	4.3 Final Computation	58
	References	64
	Use of Formal Verification at Centaur Technology	75
	1 Introduction	75
	1.1 Overview of Verification Methodology	75
	1.2 Timeline	76
	1.3 Centaur Media Unit	78
	2 Modeling Effort	79
	2.1 Conversion to the EMOD Language	80
	2.1.1 Unparameterization	81
	2.1.2 Declaring Implicit and Port Wires	81
	2.1.3 Standardizing Argument Lists	81
	2.1.4 Resolving Ranges	81
	2.1.5 Operator Rewriting	82
	2.1.6 Sign and Width Computation	82
	2.1.7 Expression Splitting	82
	2.1.8 Making Truncation Explicit	82
	2.1.9 Eliminating Assignments	83
	2.1.10 Eliminating Instance Arrays	83
	2.1.11 Eliminating Higher-Arity Gates	83
	2.2 Modeling Flow	84
	3 Verification Method	84
	3.1 Case-Splitting and Parametrization	86
	3.2 Symbolic Simulation of the Hardware Model	86
	3.3 Symbolic Simulation of Specification	87
	3.4 Comparison of Specification to Hardware Model	88
	4 Mechanisms Used to Achieve the Verification	89
	4.1 EMOD Symbolic Simulator	89
	4.2 BDDs and AIGs	90
	4.3 Parametrization	90
	4.4 AIG-to-BDD Translation	91
	4.5 GL Symbolic Execution Framework	92
	5 Verification Results and Observations	95
	6 Related Work	96
	7 Conclusion	97
	References	97
	Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol	99
	1 Introduction	99
	1.1 Outline	100
	2 Cryptol Overview	100
	2.1 Language Features	100
	2.1.1 Function Values and Anonymous Functions	100
	2.1.2 Types and Polymorphism	101
	2.1.3 Type Aliases and Records	103
	2.1.4 Enumerations	104
	2.1.5 Index Operators	104
	2.1.6 Sequence Operations and Transformations	105
	2.2 Cryptol Interpreter	106
	2.3 Cryptol Interpreter Modes for Hardware Design	107
	2.4 Equivalence Checking	108
	3 Cryptol for Hardware Design	109
	3.1 Issues and Limitations	109
	3.1.1 Supported Subset	109
	3.1.2 Inefficient Sequence Comprehensions	110
	3.2 Combinatorial and Sequential Circuits in Cryptol	111
	3.3 Delays and Undelays	113
	3.4 Space–Time Tradeoffs via par and seq Pragmas	114
	3.4.1 Example 1: Parallel Sequence Comprehension	115
	3.4.2 Example 2: Sequential Sequence Comprehension	117
	3.5 Pipelining	118
	3.5.1 Example 1: Combinatorial Circuit	119
	3.5.2 Pipelining via the reg Pragma	122
	4 AES Specification	123
	4.1 API	123
	4.2 Types	124
	4.3 Conversions Between Types	126
	4.4 Constructors for the Duo Type	126
	4.5 Mathematical Preliminaries	126
	4.5.1 Addition	126
	4.6 Multiplication	127
	4.6.1 Multiplication by x	127
	4.7 Polynomials with Coefficients in GF(28)	127
	4.8 Algorithm Specification	128
	4.9 Cipher	128
	4.9.1 SubBytes() Transformation	129
	4.9.2 ShiftRows() Transformation	130
	4.9.3 MixColumns() Transformation	130
	4.9.4 AddRoundKey() Transformation	131
	4.10 Key Expansion	131
	4.11 Inverse Cipher	132
	4.11.1 InvShiftRows() Transformation	132
	4.11.2 InvSubBytes() Transformation	132
	4.11.3 InvMixColumns() Transformation	133
	4.11.4 Equivalent Inverse Cipher	133
	4.12 Auxiliary Definitions	134
	4.13 Key Expansion Example: 12