Formal Methods for the Verification of Digital Circuits

دسته بندی: ریاضیات گسسته
ویرایش:  
نویسندگان: Van Eijk C.A.J.  
سری:  
 
ناشر:  
سال نشر:  
تعداد صفحات: 156 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 552 کیلوبایت 

قیمت کتاب (تومان) : 51,000

Диссертация, Technische Universiteit Eindhoven, 1997, -156 pp. با پیچیدگی روزافزون و برنامه های فشرده زمان عرضه به بازار سیستم های دیجیتال امروزی، این امر روز به روز دشوارتر می شود. برای طراحی مدارهای صحیح برای این سیستم ها. بنابراین، در طول فرآیند طراحی باید بررسی شود که هیچ خطایی وجود نداشته باشد. این کار تایید نامیده می شود. به طور سنتی، یک طرح با شبیه سازی گسترده آن تأیید می شود. این رویکرد دیگر کافی نیست، زیرا بیش از حد وقت گیر است و هیچ تضمین مطلقی در مورد صحت طراحی ارائه نمی دهد. یکی از رویکردهایی که برای حل این مشکلات مطرح شده است، تایید رسمی است. ویژگی کلیدی این رویکرد این است که روش‌های رسمی برای ساختن یک اثبات ریاضی برای درستی طرح به کار می‌روند.
در این پایان‌نامه، روش‌های رسمی برای تأیید مدارهای دیجیتال سنکرون را مورد بحث قرار می‌دهیم. به طور خاص تر، ما روش هایی را برای تأیید هم ارزی عملکردی مدارهای مشخص شده در سطح انتقال ثبت و گیت توصیف می کنیم. چنین روش‌هایی را می‌توان در عمل برای تأیید اینکه توصیفات مدار قبل و بعد از مرحله طراحی، عملکرد یکسانی را تعریف می‌کنند، استفاده کرد. ما بر توسعه روش های تأیید رسمی با درجه بالایی از اتوماسیون و با عملکرد کافی برای مدیریت مدارهای با پیچیدگی صنعتی تمرکز می کنیم. از نظر تئوری، اکثر مشکلات مربوط به تایید رسمی مدارهای دیجیتال متعلق به کلاس های پیچیدگی هستند که تصور می شود هیچ الگوریتم چند جمله ای برای آنها وجود نداشته باشد. بنابراین توسعه روش های تأیید برای حل هر نمونه مشکل در یک زمان معقول غیر قابل بحث است. در عوض، ما باید راه‌های دیگری برای توسعه روش‌هایی پیدا کنیم که در عمل به اندازه کافی عمل کنند. در این پایان نامه، ما یک رویکرد مبتنی بر این مشاهدات را اعمال می کنیم که تأیید به طور معمول برای مقایسه مدارهایی که شباهت های خاصی را نشان می دهند استفاده می شود. ما روش‌های راستی‌آزمایی را پیشنهاد می‌کنیم که الگوریتم‌های تأیید عمومی قدرتمند را با تکنیک‌هایی برای استفاده از این شباهت‌ها ترکیب می‌کنند. ما این رویکرد را برای سه مشکل راستی‌آزمایی زیر اعمال می‌کنیم.
اولین مشکلی که در نظر می‌گیریم، تأیید هم ارزی عملکردی مدارهای ترکیبی است. ما بر تأیید مدارهای ترکیبی بهینه‌سازی شده توسط ابزارهای سنتز منطق تمرکز می‌کنیم. این ابزارهای سنتز معمولاً تأثیر محدودی بر ساختار یک مدار دارند. بنابراین، اغلب امکان شناسایی سیگنال‌ها در مدارهای قبل و بعد از سنتز وجود دارد که عملکرد یکسانی را اجرا می‌کنند. ما نشان می‌دهیم که چگونه یک روش تأیید شناخته شده مبتنی بر نمودارهای تصمیم باینری (BDD) می‌تواند برای شناسایی و استفاده خودکار این سیگنال‌ها گسترش یابد. ما همچنین نشان می‌دهیم که روش به‌دست‌آمده کارایی کافی برای تأیید صحت مدارهای سنتز شده در یک محیط صنعتی دارد.
دومین مشکل راستی‌آزمایی که در این پایان‌نامه به آن می‌پردازیم، تأیید هم ارزی عملکردی مدارهای متوالی با رمزگذاری‌های حالت یکسان است. ما نشان می‌دهیم که اگر برای هر ثبات یک مقدار اولیه مشخص شود، ثبات‌های مربوطه را می‌توان به طور خودکار با حل یک سری مشکلات تأیید ترکیبی شناسایی کرد. بنابراین، روش های تأیید ترکیبی را می توان به راحتی برای استخراج خودکار مکاتبات ثبت گسترش داد. در عمل، این بدان معنی است که الزامی نیست که مطابقت رجیستر به طور صریح مشخص شود یا بتوان آن را از نام رجیسترها مشتق کرد.
بررسی هم ارزی عملکردی مدارهای ترتیبی سومین و کلی ترین تأیید است. مشکلی که در این پایان نامه در نظر می گیریم. ما یک روش تأیید مبتنی بر BDD را پیشنهاد می‌کنیم که از وابستگی‌های عملکردی برای استفاده از رابطه بین کدگذاری‌های حالت هر دو مدار استفاده می‌کند. این وابستگی‌های عملکردی را می‌توان در حین محاسبه فضای حالت قابل دستیابی به اصطلاح ماشین محصول شناسایی کرد. ما همچنین دو تکنیک را برای شناسایی انواع خاصی از وابستگی‌های عملکردی قبل از محاسبه فضای حالت قابل دسترسی پیشنهاد می‌کنیم. بهره‌برداری از وابستگی‌های عملکردی به وضوح منجر به افزایش قابل‌توجه در عملکرد می‌شود و در برخی موارد تأیید مدارهای بسیار بزرگ‌تر را نیز امکان‌پذیر می‌سازد.
برای مدیریت پیچیدگی تأیید متوالی، لازم است دستگاه محصول به تعدادی از دستگاه‌ها تجزیه شود. ماشین‌های فرعی کوچک‌تر که هر کدام را می‌توان جداگانه تحلیل کرد. برای بهره مندی واقعی از این رویکرد، به طور کلی لازم است که از تعاملات دقیق بین این ماشین های فرعی انتزاع کنیم. بنابراین، ما استفاده از تکنیک‌های انتزاعی با حفظ ضعیف را در زمینه تأیید متوالی بررسی می‌کنیم. ما یک مکانیسم انتزاع مناسب را پیشنهاد می‌کنیم و یک روش تأیید مبتنی بر تجزیه را بر اساس این مکانیسم ارائه می‌کنیم. علاوه بر این، ما همچنین تکنیک‌های انتزاعی را برای رد هم ارزی مدارهای متوالی توصیف می‌کنیم. />تأیید متوالی
تکنیک های انتزاعی
نکته های پایانی

Диссертация, Technische Universiteit Eindhoven, 1997, -156 pp. With the increasing complexity and tight time-to-market schedules of today’s digital systems, it is becoming more and more difficult to design correct circuits for these systems. Therefore, throughout the design process it is necessary to check that no errors are made. This task is called verification. Traditionally, a design is verified by simulating it extensively. This approach is no longer adequate, because it is too time-consuming and it gives no absolute guarantees about the correctness of the design. One of the approaches that have been put forward to solve these problems is formal verification. The key characteristic of this approach is that formal methods are applied to actually construct a mathematical proof for the correctness of the design.
In this thesis, we discuss formal methods for the verification of synchronous digital circuits. More specifically, we describe methods to verify the functional equivalence of circuits specified at the register transfer and gate level. Such methods can be used in practice to verify that the circuit descriptions preceding and following a design step define the same functionality. We focus on the development of formal verification methods with a high degree of automation and with sufficient performance to handle circuits of industrial complexity. Theoretically, most problems related to the formal verification of digital circuits belong to complexity classes for which no polynomial algorithms are believed to exist. Therefore the development of verification methods solving each problem instance in a reasonable time is out of the question. Instead, we have to find other ways to develop methods which perform adequately in practice. In this thesis, we apply an approach based on the observation that verification is typically used to compare circuits which show certain similarities. We propose verification methods which combine powerful general verification algorithms with techniques to utilize these similarities. We apply this approach to the following three verification problems.
The first problem we consider is that of verifying the functional equivalence of combinational circuits. We focus on the verification of combinational circuits optimized by logic synthesis tools. These synthesis tools typically have a limited effect on the structure of a circuit. Therefore, it is often possible to identify signals in the circuits preceding and following synthesis which implement the same function. We show how a well-known verification method based on binary decision diagrams (BDDs) can be extended to automatically detect and utilize these signals. We also demonstrate that the resulting method has sufficient performance to verify the correctness of circuits synthesized in an industrial environment.
The second verification problem we address in this thesis is that of verifying the functional equivalence of sequential circuits with identical state encodings. We show that if for each register an initial value is specified, the corresponding registers can be detected automatically by solving a sequence of combinational verification problems. Therefore, combinational verification methods can easily be extended to automatically extract the register correspondence. In practice, this means that it is not necessary to require that the register correspondence is specified explicitly or that it can be derived from the names of the registers.
Checking the functional equivalence of sequential circuits is the third and most general verification problem we consider in this thesis. We propose a BDD-based verification method which uses functional dependencies to utilize the relation between the state encodings of both circuits. These functional dependencies can be detected while calculating the reachable state space of the so-called product machine. We also propose two techniques to detect specific types of functional dependencies before the reachable state space is calculated. Exploiting functional dependencies clearly results in a significant increase in performance, and in some cases it also enables the verification of significantly larger circuits.
To manage the complexity of sequential verification, it is necessary to decompose the product machine into a number of smaller sub-machines which can each be analyzed separately. To really benefit from this approach, it is generally necessary to abstract from the detailed interactions between these sub-machines. Therefore, we investigate the use of weakly-preserving abstraction techniques in the context of sequential verification. We propose an appropriate abstraction mechanism and we present a decompositionbased verification method based on this mechanism. Furthermore, we also describe abstraction techniques for disproving the equivalence of sequential circuits. Formal Verification
Preliminaries
Combinational Verification
Register Correspondences
Sequential Verification
Abstraction Techniques
Concluding Remarks