دانلود کتاب FM8501: A Verified Microprocessor
دسته: کامپیوتر
کتاب FM8501: یک ریزپردازنده تایید شده نسخه زبان اصلی
دانلود کتاب FM8501: یک ریزپردازنده تایید شده بعد از پرداخت مقدور خواهد بود
توضیحات کتاب در بخش جزئیات آمده است و می توانید موارد را مشاهده فرمایید
توضیحاتی در مورد کتاب FM8501: A Verified Microprocessor
نام کتاب : FM8501: A Verified Microprocessor
ویرایش : 1
عنوان ترجمه شده به فارسی : FM8501: یک ریزپردازنده تایید شده
سری : Lecture Notes in Computer Science 795 : Lecture Notes in Artificial Intelligence
نویسندگان : Warren A. Hunt Jr. (eds.)
ناشر : Springer-Verlag Berlin Heidelberg
سال نشر : 1994
تعداد صفحات : 338
ISBN (شابک) : 3540579605 , 9783540579601
زبان کتاب : English
فرمت کتاب : pdf
حجم کتاب : 9 مگابایت
بعد از تکمیل فرایند پرداخت لینک دانلود کتاب ارائه خواهد شد. درصورت ثبت نام و ورود به حساب کاربری خود قادر خواهید بود لیست کتاب های خریداری شده را مشاهده فرمایید.
توضیحاتی در مورد کتاب :
ریزپردازنده FM 8501 به عنوان یک ریزپردازنده عمومی تا حدودی شبیه به PDP-11 اختراع شد. ایده اصلی تلاش FM 8501 این بود که ببینیم آیا امکان بیان مشخصات سطح کاربر و اجرای طراحی با استفاده از منطق رسمی، منطق بویر مور وجود دارد یا خیر. این رویکرد به اثبات مکانیکی کامل اجازه می دهد که پیاده سازی FM 8501 به طور کامل مشخصات خود را پیاده سازی کند. مدل پیاده‌سازی FM 8501 برای طراحی سخت‌افزار صنعتی ناکافی بود، اما این تلاش گام مهمی در تکامل روش تأیید طراحی که اکنون توسط نویسنده استفاده می‌شود، بود.
نسخه اصلی این تک‌نگاره به‌عنوان پایان‌نامه در دانشگاه ارائه شد. دانشگاه تگزاس در آستین تحت مشاوره R. Boyer و J. Moore.
فهرست مطالب :
Introduction....Pages 1-4
A hardware model....Pages 5-11
Notation and bit vectors....Pages 13-18
Numeric definitions and operations....Pages 19-26
The verification approach....Pages 27-30
FM8501: A conventional description....Pages 31-39
Commonly used functions....Pages 41-53
The ALU....Pages 55-67
Instruction fields....Pages 69-71
Update and accessor functions....Pages 73-74
The FM8501 hardware interpreter....Pages 75-91
FM8501: A formal specification....Pages 93-102
Correctness of FM8501....Pages 103-110
Expansion of FM8501....Pages 111-142
Conclusions....Pages 143-145
توضیحاتی در مورد کتاب به زبان اصلی :
The FM 8501 microprocessor was invented as a generic microprocessor somewhat similar to a PDP-11. The principal idea of the FM 8501 effort was to see if it was possible to express the user-level specification and the design implementation using a formal logic, the Boyer-Moore logic; this approach permitted a complete mechanically checked proof that the FM 8501 implementation fully implemented its specification. The implementation model for the FM 8501 was inadequate for industrial hardware design but the effort was an important step in the evolution to the design verification methodology now employed by the author.
The original version of this monograph was submitted as a dissertation at the University of Texas at Austin under the advisorship of R. Boyer and J. Moore.