دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
دانلود کتاب FM8501: A Verified Microprocessor
دانلود کتاب FM8501: یک ریزپردازنده تایید شده
مشخصات کتاب
FM8501: A Verified Microprocessor
دسته بندی: کامپیوتر ویرایش: 1 نویسندگان: Warren A. Hunt Jr. (eds.) سری: Lecture Notes in Computer Science 795 : Lecture Notes in Artificial Intelligence ISBN (شابک) : 3540579605, 9783540579601 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 1994 تعداد صفحات: 338 زبان: English فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 9 مگابایت
قیمت کتاب (تومان) : 45,000
کلمات کلیدی مربوط به کتاب FM8501: یک ریزپردازنده تایید شده: هوش مصنوعی (شامل رباتیک)، طراحی منطقی، منطق ریاضی و زبان های رسمی، ساختارهای حسابی و منطقی، ارتباطات ورودی/خروجی و داده، الکترونیک و میکروالکترونیک، ابزار دقیق
در صورت تبدیل فایل کتاب FM8501: A Verified Microprocessor به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب FM8501: یک ریزپردازنده تایید شده نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
توضیحاتی در مورد کتاب FM8501: یک ریزپردازنده تایید شده
ریزپردازنده FM 8501 به عنوان یک ریزپردازنده عمومی تا حدودی
شبیه به PDP-11 اختراع شد. ایده اصلی تلاش FM 8501 این بود که
ببینیم آیا می توان مشخصات سطح کاربر و اجرای طراحی را با
استفاده از یک منطق رسمی، منطق بویر مور بیان کرد یا خیر. این
رویکرد به اثبات مکانیکی کامل اجازه می دهد که پیاده سازی FM
8501 به طور کامل مشخصات خود را پیاده سازی کند. مدل پیاده‌سازی
FM 8501 برای طراحی سخت‌افزار صنعتی ناکافی بود، اما این تلاش
گام مهمی در تکامل روش تأیید طراحی بود که اکنون توسط نویسنده
استفاده می‌شود.
نسخه اصلی این تک‌نگاره به‌عنوان پایان‌نامه در دانشگاه ارائه
شد. دانشگاه تگزاس در آستین تحت مشاوره R. Boyer و J. Moore.
توضیحاتی درمورد کتاب به خارجی
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.
فهرست مطالب
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
نظرات کاربران
کتاب های مرتبط
دانلود کتاب Software Engineering 2: Specification of Systems and Languages
دانلود کتاب Blender 3D Printing Essentials
دانلود کتاب Gesture and Sign Language in Human-Computer Interaction: International Gesture Workshop, GW 2001 London, UK, April 18–20, 2001 Revised Papers
دانلود کتاب Speculative Execution in High Performance Computer Architectures (Chapman & Hall Crc Computer & Information Science Series)
دانلود کتاب Computer-Aided Fixture Design
دانلود کتاب The Digital Hand, Vol 3: How Computers Changed the Work of American Public Sector Industries
دانلود کتاب Introduction to Discrete Event Systems
دانلود کتاب Web-Age Information Management: 11th International Conference, WAIM 2010, Jiuzhaigou, China, July 15-17, 2010. Proceedings
