عنوان پایان‌نامه
مدلسازی صوری و آنالیز شبکه های روی تراشه
- رشته تحصیلی
- مهندسی کامپیوتر -نرم افزار
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2337;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 59990
- تاریخ دفاع
- ۳۰ مرداد ۱۳۹۲
- دانشجو
- زینب شریفی
- استاد راهنما
- سیامک محمدی
- چکیده
- با افزایش تعداد ترانزیستورها بر روی تراشه ها، ایده ی شبکه ی روی تراشه به عنوان زیرساخت ارتباطی مناسب بسیار مورد توجه قرار گرفت. به دلیل مشکلات بسیار در طراحی کاملا همگام این شبکه ها رویکرد ناهمگام در طراحی آنها به کار گرفته شد. دو چالش عمده در طراحی این شبکه ها که به نام شبکه های ناهمگام سراسری همگام محلی شناخته میشوند عبارتند از: 1) ارزیابی کارایی در مراحل اولیه ی طراحی جهت انتخاب پارامترهای مناسب و 2) درستی یابی عملکردی. روشهای صوری و به خصوص روش وارسی مدل به دلیل اینکه قابلیت تخمین توابع هزینه ی مختلف را دارند و همچنین قادر به انجام درستی یابی جامع در سیستم جهت بررسی برقراری خواص مورد انتظار سیستم هستند، برای برطرف ساختن چالشهای مورد بحث مناسب میباشند. استفاده از این روش ها به جهت توانایی آنها در مجتمع ساختن دو نوع آنالیز عملکردی و کارایی بر روی یک مدل واحد از سیستم از جدیدترین ایده ها در طراحی و درستی یابی شبکه های روی تراشه است. این طرح با استفاده از روش وارسی مدل به درستی یابی عملکردی و تخمین کارایی (معیار تاخیر) در شبکه های روی تراشه ی ناهمگام سراسری همگام محلی می پردازد. در این راستا در گام اول به بررسی اجزای این سیستم ها می پردازد. سپس با استفاده از یک زبان مدل سازی مناسب مدلی برای شبکه های روی تراشه ی ناهمگام سراسری همگام محلی ارائه خواهد شد. مدل ارائه شده به جهت در نظر گرفتن رفتارهای زمانی و عملکردی سیستم قابلیت بکارگیری برای درستی یابی عملکردی و ارزیابی کارایی را داراست. زبان مورد استفاده در این طرح ربکای زمان دار است که مبتنی بر مدل بازیگر بوده و به همین دلیل امکان ارائه ی مدل ساده از ارتباطات ناهمگام در این شبکه ها را فراهم می آورد. یکی از مشکلات درستی یابی خودکار و جامع در سیستم ها انفجار فضای حالت است. این مسئله اندازه ی شبکه های روی تراشه ی قابل بررسی با استفاده از روش وارسی مدل را محدود میکند. در راستای بهبود این مشکل، در این طرح روشی مبتنی بر ترکیب برای درستی یابی شبکه هایی که از الگوریتم مسیریابی XY استفاده میکنند ارائه خواهد شد.
- Abstract
- Network on Chip (NoC) is a promising interconnection network for today's many core systems on chips (SoCs). Fully synchronous design of such systems face problems such as clock skew. To overcome these problems asynchronous paradigm has been applied in designing NoCs. Thus, Globally Asynchronous Locally Synchronous (GALS) NoC has gained attention. However, GALS NoCs encounter two main challenges: (1) functional verification, to check if the desired properties are met, and (2) performance evaluation in the early stages of the design process to choose the proper design parameters. Due to concurrent processing of cores in a GALS NoC, exhaustive methods are required to verify GALS systems by considering all possible permutation of process execution. Formal methods, especially model checking, are exhaustive and able to estimate different cost functions. In this thesis we use model checking to confront both challenges simultaneously and make use of one model for verifying both functional and performance properties. A formal model for GALS NoC is presented that can be used for estimating end-to-end packet latency, as well as checking functional properties like deadlock freedom, starvation freedom, mutual exclusion and successful arrival of packets to their destination. Functional and timing behaviors, communication protocol, routing and scheduling algorithms are considered in the model. Using an actor-based model with formal verification support allows us to model the asynchronous behavior of GALS NoC naturally. Here, Timed Rebeca (Reactive Objects Language) is used as modeling language. Timed Rebeca is an actor-based modeling language capable of modeling functionalities and timing behaviors of asynchronous systems. Due to the asynchronous communication, applying an exhaustive verification on large NoCs may result in state space explosion. To alleviate this problem we present a more scalable method based on compositional verification for analyzing NoCs that use XY routing algorithm. Results of verification are compared and matched to simulation results of HSPICE using 32nm technology.
