دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1 نویسندگان: George J. Milne (auth.), Miriam Leeser, Geoffrey Brown (eds.) سری: Lecture Notes in Computer Science 408 ISBN (شابک) : 3540972269, 9783540972266 ناشر: Springer-Verlag New York سال نشر: 1990 تعداد صفحات: 408 زبان: English فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 4 مگابایت
کلمات کلیدی مربوط به کتاب مشخصات سخت افزار، تأیید و ترکیب: جنبه های ریاضی: کارگاه مؤسسه علوم ریاضی دانشگاه کرنل، ایتاکا، نیویورک، ایالات متحده آمریکا 5-7 ژوئیه، 1989 مجموعه مقالات: ساختارهای کنترل و ریزبرنامه ریزی، ساختارهای حسابی و منطقی، طراحی منطقی، الکترونیک و میکروالکترونیک، ابزار دقیق، محاسبات با دستگاه های انتزاعی، جبر
در صورت تبدیل فایل کتاب Hardware Specification, Verification and Synthesis: Mathematical Aspects: Mathematical Sciences Institute Workshop Cornell University, Ithaca, New York, USA July 5–7, 1989 Proceedings به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب مشخصات سخت افزار، تأیید و ترکیب: جنبه های ریاضی: کارگاه مؤسسه علوم ریاضی دانشگاه کرنل، ایتاکا، نیویورک، ایالات متحده آمریکا 5-7 ژوئیه، 1989 مجموعه مقالات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
تحقیقات فعلی در مورد روشهای رسمی برای طراحی سخت افزار در مقالات این جلد ارائه شده است. به دلیل پیچیدگی مدارهای VLSI، اطمینان از اعتبار طراحی قبل از ساخت مدارها ضروری است. هدف تحقیق در این زمینه توسعه روش هایی برای بهبود فرآیند طراحی و کیفیت طرح های حاصل است. روند اصلی که در این کارگاه آشکار می شود این است که محققان با هزینه هنگفت خود به سرعت از تکنیک های اثبات post hoc دور می شوند. تعدادی مقاله ارائه شد که به مشکلات سنتز مدارهای صحیح و طراحی با هدف تأیید پرداختند. محققان همچنین شروع به پرداختن به مسائل نظری استدلال در مورد سیستم های همزمان و سیستم های ناهمزمان و معرفی ابزارهای منطقی جدید مانند نظریه نوع سازنده و نظریه دسته می کنند. بیشتر تحقیقات گزارش شده در ایالات متحده انجام شده است.
Current research into formal methods for hardware design is presented in the papers in this volume. Because of the complexity of VLSI circuits, assuring design validity before circuits are manufactured is imperative. The goal of research in this area is to develop methods of improving the design process and the quality of the resulting designs. The major trend apparent at the workshop is that researchers are rapidly moving away from post hoc proof techniques with their great expense. A number of papers were presented that dealt with problems of synthesizing correct circuits and of designing with the goal of verification. Researchers are also beginning to deal with the theoretical issues of reasoning about concurrent systems and asynchronous systems, and to introduce new logical tools such as constructive type theory and category theory. Most of the research reported was performed in the United States.
Design for verifiability....Pages 1-13
Verification of synchronous circuits by symbolic logic simulation....Pages 14-24
Constraints, abstraction, and verification....Pages 25-39
Formalising the design of an SECD chip....Pages 40-66
Reasoning about state machines in higher-order logic....Pages 67-89
A mechanically derived systolic implementation of pyramid initialization....Pages 90-105
Behavior-preserving transformations for high-level synthesis....Pages 106-128
From programs to transistors: Verifying hardware synthesis tools....Pages 129-151
Combining engineering vigor with mathematical rigor....Pages 152-176
Totally verified systems: Linking verified software to verified hardware....Pages 177-201
What's in a timing discipline? Considerations in the specification and synthesis of systems with interacting asynchronous and synchronous components....Pages 202-223
Complete trace structures....Pages 224-243
The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation....Pages 244-259
Manipulating logical organization with system factorizations....Pages 260-281
The verification of a bit-slice ALU....Pages 282-306
Verification of a pipelined microprocessor using clio....Pages 307-332
Verification of combinational logic in Nuprl....Pages 333-357
Veritas + : A specification language based on type theory....Pages 358-379
Categories for the working hardware designer....Pages 380-402