Algebraic Specificat ion and Verification of Processor Microarchitectures

دانشگاه آزاد اسلامی اصفهان(خوراسگان)

منو

رکورد قبلی

رکورد بعدی

" Algebraic Specificat ion and Verification of Processor Microarchitectures "

Document Type	:	Latin Dissertation
Language of Document	:	English
Record Number	:	151600
Doc. No	:	ET23392
Main Entry	:	John Robert hlatthews
Title Proper	:	Algebraic Specificat ion and Verification of Processor Microarchitectures
Note	:	This document is digital این مدرک بصورت الکترونیکی می باشد
Abstract	:	The Huuk language is a domain-specific extension of the pure functional language Haskcll.and is used to specify and reason about processor microarchitectures at a high level ofabstract ion. We apply functional lar~guage technology and reasoning principles to conciselyspecify pipelined microarchitect tires in Hawk and verify them through a domain-specificmicroarchitecture ulgebra. We develop a remarkably simple set of local equational lawsgoverning processor components such as register files? bypass logic, and execution units.Many of these laws are verified in Isabelle, a higher order logic theorem prover. Thelaws are used to incrementally simplify a complex pipelined microarchitecture, removingpipeline stages and simplifying control logic? while retaining cycle-accurate behavior withrespect to the original pipelined design.Proving these laws requires defining mutually recursive functions over coinduct ivelydefined streams. Such definitions are not directly supported in current theorem provers.We develop a generalization of well-founded recursion. called Converging Equivalence Re-lations, that allows these definitions to be added conservatively in a straightforward andmodular fashion......-....,....-...,..tested for theQ1 PC1 bus cardBoth these projects mere sofixare des elopment efforts tonards contributing to dlfferentaspects of Roboucs and lZ1echatronics projects m the Controls and Roboucs Group..
Subject	:	Electericl tess
	:	برق
electronic file name	:	TL46631.pdf
Title and statement of responsibility and	:	Algebraic Specificat ion and Verification of Processor Microarchitectures [Thesis]