عنوان پایان‌نامه
بررسی روشهای درستی یابی رسمی مدارهای محاسباتی بر اساس روش جبر کامپیوتری نمادین
- رشته تحصیلی
- مهندسی کامپیوتر-معماری کامپیوتر
- مقطع تحصیلی
- کارشناسی ارشد
- محل دفاع
- کتابخانه مرکزی پردیس 2 فنی شماره ثبت: E 2256;کتابخانه مرکزی -تالار اطلاع رسانی شماره ثبت: 58395
- تاریخ دفاع
- ۱۲ مرداد ۱۳۹۲
- دانشجو
- فریماه فرهمندی
- استاد راهنما
- زین العابدین نوابی شیرازی, بیژن علیزاده ملفه
- چکیده
- امروزه، مدارهای حسابی اجزایی حیاتی در بسیاری از طراحیهای عملی از جمله کاربردهای پردازش سیگنال و مالتی مدیا می باشند. در نتیجه مدارهای حسابی قسمت اصلی مسیرهای داده ی این کاربردها را تشکیل می دهند. در این نوع کاربردها، اندازه مسیر داده ی مدار می تواند خیلی بزرگ باشد و ابزارهای درستی یابی موجود تقریبا قادر به درستی یابی این گونه مدارها در زمان و حافظه مصرفی بهینه نیستند. در این پایان نامه تلاش می شود تا با تبدیل مدارهای حسابی در سطح گیت به یک فرم انتزاعی سطح بالاتر و با استفاده از روش جبر کامپیوتری نمادین راه حلی جدید برای درستی یابی مدارهای حسابی پس از سنتز به دست آورده شود. در واقع برای درستی یابی، مدار حسابی در سطح گیت و اطلاعاتی از سطح بالاتر (توصیف سطح بالای مدار) را داریم و سعی می کنیم برابری آن ها را تایید کنیم. برای این منظور، پیاده سازی سطح گیت مدار حسابی و مشخصه ی آن به چندجمله ای ها مدل می شوند و مساله درستی یابی به صورت آزمون عضویت چندجمله ای مشخصه در ایده آل تولید شده توسط چندجمله ای های مدار فرموله میشود. آزمون عضویت نیازمند محاسبه ی گرابنر بیسیس ایده آل ایجاد شده می باشد. برای غلبه بر محاسبات پرهزینه گرابنر بیسیس، توپولوژی مدار را تجزیه تحلیل می کنیم و یک ترتیب مونومیال برای نمایش چندجمله ای بدست می آوریم. با استفاده از این ترتیب، چندجمله ای های مدار خود گرابتر بیسیس می شوند و محاسبات گرابنر بیسیس حذف خواهد شد. در نتیجه، مساله درستی یابی تبدیال به کاهش چندجمله ای مشخصه ی مدار روی گرابنر بیسیس می شود. پیچیدگی کاهش یک چندجمله ای روی گرابنر بیسیس، کاملا به اندازه گرابنر بیسیس (تعداد چندجمله ای های مدار) و الگوریتم کاهش وابسته می باشد. در این پایان نامه با ارائه دو روش درصدد افزایش کارایی این قسمت بر آمدیم: در روش اول، برای کاهش اندازه گرابنر بیسیس، اجزای پرتکرار مدار را با استفاده از یک آتوماتا استخراج نمودیم و آنها را با یک چندجمله ای نمایش دادیم. همچنین برای انجام موثرعملیات کاهش، چندجمله ای ها را با ساختار HED نمایش دادیم. در روش دوم، مناطق بدون فن اوت مدار را به طور خودکار استخراج نموده و آنها را به یک چندجمله ای تبدیل کردیم. برای انجام کاهش چندجمله ای مشخصه توسط گرابنر بیسیس، مفهوم حذف گوسی را روی ماتریس نشان دهنده ی مساله بکار بردیم. برای ارزیابی تکنیک های ارائه شده، آن ها را روی مدارهای حسابی بزرگ با ساختارهای متفاوت اعمال نمودیم. همچنین روشی رسمی مبتنی بر گرابنر بیسیس برای خطایابی مدارهای حسابی معرفی می کنیم. این روش، خطاهای تکی و چندتایی پیاده سازی مدار را بر اساس تحلیل باقی مانده کاهش چندجمله ای مشخصه ی مدار توسط گرابنر بیسیس مشخص و اصلاح می کند.
- Abstract
- Nowadays, Arithmetic circuits are critical components in many practical designs such as signal processing and multimedia applications. In these applications the size of the datapath can be very large so that contemporary verification methods are almost incapable of verifying such circuits in an efficient time and memory usage. This thesis addresses formal verification of large integer arithmetic circuits using symbolic computer algebra based approach. In order to efficiently verify gate level arithmetic circuits, we model the circuit and the specification in polynomial system and the verification problem is formulated as membership testing of the given specification polynomial in the circuit polynomials’ corresponding ideal. The membership testing needs Groebner basis reduction. In order to overcome the costly Groebner basis computation, we make use of a topological term order to represent polynomials. By using the topological term ordering, the circuit's polynomials will be the Groebner basis itself and Groebner basis computation will be eliminated. Thus the verification test reduces to Groebner basis reduction via polynomial division. The complexity of Groebner basis reduction completely depends on the Groebner basis size so it is related to the number of circuit polynomials. In order to improve this part, two different approaches have been taken into account. First, inordet to reduce the size of Grobner basis, we find repetitive components based on automata and represent them as a polynomial by using a canonical decision diagram named Horner Expansion Diagram (HED).Second, in order to overcome intensive polynomial reduction needed in Groebner basis computation so that we can deal with verifying large arithmetic circuits, the fanout-free regions of the circuit are extracted and represented as corresponding polynomials automatically. For further improvement, we make use of Gaussian elimination concept to perform specification polynomial reduction w.r.t Groebner basis on a matrix representation of the problem. the size of Groebner basis, the fanout-free regions of the circuit are extracted and represented as corresponding polynomials automatically. To evaluate the effectiveness of our verification technique, we have applied it to very large arithmetic circuits including multipliers with different architectures. Preliminary experimental results show that the proposed verification technique is scalable enough so that large arithmetic circuits can efficiently be verified in reasonable run time and memory usage. We also proposed a formal technique for debugging of arithmetic circuits based on Groebner basis method. We detect and correct single and multiple faults that occurred in arithmetic circuits based on analyzing the remainder of Groebner basis reduction.
