خط مشی دسترسیدرباره ما
ثبت نامثبت نام
راهنماراهنما
فارسی
ورودورود
صفحه اصلیصفحه اصلی
جستجوی مدارک
تمام متن
منابع دیجیتالی
رکورد قبلیرکورد بعدی
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]
 
 
 
(در صورت عدم وضوح تصویر اینجا را کلیک نمایید)