عنوان پایان‌نامه
تشخیص و تصحیح خطای طراحی سیستم¬های دیجیتال
- رشته تحصیلی
- مهندسی کامپیوتر-معماری کامپیوتر
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2513;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 64460
- تاریخ دفاع
- ۲۰ شهریور ۱۳۹۲
- دانشجو
- پیمان به نام
- استاد راهنما
- زین العابدین نوابی شیرازی, بیژن علیزاده ملفه
- چکیده
- با افزایش روزافزون پیچیدگی سیستم‌ها، درستی‌سنجی و عیب‌یابی تبدیل به یک بخش عمده و زمان‌بر در روند طراحی شده است. در این پایان‌نامه به موضوع تشخیص و تصحیح خطای طراحی سیستم‌های دیجیتال در سطوح مختلف طراحی پرداخته شده است. به این منظور روش‌هایی در سطح گیت با استفاده از حل‌کننده‌های صدق‌پذیر، آزمون جهش و روش‌های احتمالاتی جهت تولید مثال نقص مناسب و هم‌چنین پیدا کردن محل وقوع عیب یا اشکال و تصحیح آن‌ها پیشنهادشده است. در سطح انتقال ثبات برای مدارات حسابی با مسیر داده بزرگ از دیاگرام تصمیم‌گیری سطح بالا، برش ایستا و پیمایش مسیروآزمون جهش برای پیشنهاد روشی جهت پیدا کردن مکان‌های محتمل وقوع عیب، رده‌بندی و تصحیح آن‌ها استفاده شده است. سرانجام در سطح سیستم نیز یک چارچوب برای خودکار کردن روند بررسی برابری با استفاده از دیاگرام‌های تصمیم گیری سطح بالا پیشنهاد شده است. روش ارائه شده برای بررسی برابری مخصوص طراحی‌هایی است که قرار است حلقه‌های آن با استفاده از ابزار سنتز سطح بالا به‌صورت خط لوله سنتز شوند. نتایج به دست آمده کارایی روش‌های ارائه شده را برای درستی‌سنجی، عیب‌یابی و تصحیح دسته‌ای از مدارهای دیجیتال نشان می‌دهد.
- Abstract
- By increasing complexity of digital systems, verification and debugging of such systems have become a major problem and economic issue. Although many computer-aided design solutions have been suggested to enhance the efficiency of existing debugging approaches, they are still suffering from the lack of providing a small set of potential error locations and also automatic correction mechanisms. Hence in response to rapid growth of the semiconductor industry, proposing scalable and precise verification and debugging methods are necessary. This thesis presents several verification and debugging methods in different abstraction levels of design. At gate level, by using a SAT-based framework, mutation testing, and probabilistic methods some solutions for generating counterexamples, design error diagnosis, and correction have been proposed. The focus at register transfer level is on computer graphics and embedded applications that can be modeled as polynomial computations in their datapath designs. To do so, the traditional static slicing method is enhanced by combining backward and forward path tracing incorporating MHED to reduce its disadvantages and making it efficient for debugging of polynomial datapaths. Finally at high level, an efficient formal approach using M-HED is presented to check the equivalence of synthesized RTL against high level specification in the presence of pipelining transformations.
