عنوان پایان‌نامه
ارزیابی کارآیی و درستی¬سنجی مدارهای ناهمگام سراسری همگام محلی با استفاده از وارسی مدل
- رشته تحصیلی
- مهندسی کامپیوتر-معماری کامپیوتر
- مقطع تحصیلی
- دکتری تخصصی PhD
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2933;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 74654
- تاریخ دفاع
- ۱۸ خرداد ۱۳۹۵
- دانشجو
- مهدی مصفا
- استاد راهنما
- سیامک محمدی, سعید صفری
- چکیده
- با پیشرفت فن آوری استفاده از سیستم های چند پردازنده ای روی تراشه بسیار مورد توجه قرار گرفته است. به منظور اتصال واحدهای مختلف روی تراشه (اعم از پردازنده و حافظه) شبکه های روی تراشه بدلایلی مانند کاهش سیم کشی میان این واحدها و بهبود پارامترهای عملکردی مانند توان مصرفی و تأخیر بسیار مورد توجه قرار گرفته است. به دلیل افزایش سرعت مدارهای دیجیتال و پیشرفت فن آوری ، طراحی مدارهای کاملاً همگام به دلیل مشکلاتی مانند توزیع و انحراف پالس ساعت با چالش های زیادی مواجه شده است. از این رو روش های ناهمگام در طراحی شبکه روی تراشه در سال های اخیر مورد توجه قرار گرفته است. طراحی این دسته از شبکه های ارتباطی که بنام شبکه های ناهمگام سراسری همگام محلی شناخته می شوند، یکی از موضوعات تحقیقاتی مورد توجه است. اما این سیستم ها با چند چالش عمده روبرو شده¬اند: ارزیابی کارآیی در مراحل اولیه طراحی جهت انتخاب پارامترهای مناسب، درستی-سنجی این سیستم ها و مسئله تغییرپذیری ساخت. در بحث ارزیابی کارآیی معیارهایی مانند تأخیر، توان مصرفی و قابلیت اطمینان بسیار مورد توجه بوده است به دلیل پیشرفت مدل های ریاضی صوری از جهت تخمین توابع هزینه مختلف از یک طرف و بررسی برقرار بودن خواص در یک مدل به منظور درستی-سنجی از طرف دیگر، این روش ها به عنوان راه حلی به منظور حل چالش های مطرح شده مورد توجه قرار گرفته اند. در این رساله سعی شده است مدل هایی صوری با استفاده از روش وارسی مدل ارائه شود که ارزیابی کارآیی و نیز درستی سنجی این سیستم ها در حضور تغییرپذیری به طور همزمان مورد بحث و بررسی قرار گیرد. به منظور نیل به این هدف اجزای مختلف شبکه های روی تراشه ناهمگام سراسری همگام محلی با استفاده از روش های صوری مدل شده و سپس با استفاده از ابزارهای مناسب به ارزیابی سیستم در گام اول و درستی سنجی در گام بعد با در نظر گرفتن تغییرپذیری پرداخت. در این رساله بجز نوآوری در ترکیب حل چالش های مطرح شده در یک مدل، مفاهیم مختلف زمانی همگام و ناهمگام با توجه به جزئیات تأخیر نسبت به کارهای پیشین ارائه شده است. این کار باعث افزایش دقت مدل های صوری در مقایسه با سایر روش ها شده است. در سه سطح مختلف این چالش ها مورد بحث و بررسی قرار گرفته است: با استفاده از شبیه سازی Hspice سطح پایین، مدل صوری شبکه پتری بعنوان مدل میانی، و مدل صوری مبتنی بر بازیگر در سطح بالا. با توجه به نتایج بدست آمده با استفاده از مدل سازی دقیق جزئیات تأخیر در سطوح بالاتر از سطح پایین Hspice ، می توان به ابزاری دست یافت که با دقت مناسب و سرعت بالاتر ارزیابی کارآیی و درستی سنجی احتمالی با در نظر گرفتن تغییرپذیری انجام داد.
- Abstract
- Due to the shrinkage of technology, Multi Processor System on a Chip (MPSoC) has gained importance in computer architecture. The interconnection of different components in this architecture is done through Network on Chip (NoC) due to its lower wiring between components and its improvement of power consumption and delay. However, using a fully synchronous design for this architecture faces some challenges such as clock distribution and clock skew. Thereby, Globally Asynchronous Locally Synchronous (GALS) as a well-known structure can be used to overcome these challenges. Nevertheless, GALS NoC faces new challenges such as performance evaluation, verification and process variation. Formal methods can be used to overcome these challenges simultaneously. Formal models have suitable capabilities in modeling time and events with deterministic or probabilistic delays. In this thesis formal methods have been applied for performance evaluation of timed metrics and verification of GALS NoC circuits in presence of variation. Due to power of model checking approach in generation of state space, this method has been used for modeling of GALS NoC circuit. For this purpose first GALS NoC circuit and its components have been introduced. Next in three levels, performance evaluation and verification of this circuit have been done with variation challenge: using low level Hspice simulation for improvement of this circuit behavior with variation consideration, we have developed a new Generalized Stochastic Petri Net (GSPN) as an intermediate formal model for analysis of a GALS NoC, we have also used Rebecca as a high level formal modeling for the same analysis.
