औपचारिक तुल्यता परीक्षण

औपचारिक तुल्यता अन्वेषण प्रक्रिया इलेक्ट्रॉनिक डिजाइन स्वचालन का भाग है, जिसका उपयोग सामान्यतः डिजिटल परिपथ एकीकृत परिपथ के विकास के समय किया जाता है, औपचारिक रूप से यह प्रमाणित करने के लिए कि परिपथ डिज़ाइन के दो प्रतिनिधित्व पूर्ण रूप से समान व्यवहार प्रदर्शित करते हैं।

तुल्यता अन्वेषण और अस्पष्ट के स्तर

सामान्यतः, कार्यात्मक तुल्यता की संभावित परिभाषाओं की विस्तृत श्रृंखला होती है, जिसमें अस्पष्ट के विभिन्न स्तरों और समय के विवरण की भिन्न-भिन्न विवरण के स्तर के मध्य तुलना सम्मलित होती है।

• सबसे सामान्य दृष्टिकोण तंत्र तुल्यता की समस्या पर विचार करना है जो दो तुल्यकालिक परिपथ विनिर्देशों को कार्यात्मक रूप से समतुल्य परिभाषित करता है, यदि घड़ी की दर, वे इनपुट सिग्नल के किसी भी वैध अनुक्रम के लिए आउटपुट सिग्नल के समान अनुक्रम का उत्पादन करती हैं।
• माइक्रोप्रोसेसर डिज़ाइनर स्थानांतरण स्तर अंकित करने के लिए (आरटीएल) कार्यान्वयन के साथ निर्देश समुच्चय आर्किटेक्चर (आईएसए) के लिए निर्दिष्ट कार्यों की तुलना करने के लिए तुल्यता अन्वेषण का उपयोग करते हैं, यह सुनिश्चित करते हुए कि दोनों प्रतिरूपों पर निष्पादित कोई भी प्रोग्राम मुख्य मेमोरी सामग्री के समान अद्यतन का कारण बनेगा। यह अधिक सामान्य समस्या है।
• प्रणाली सी डिजाइन प्रवाह के लिए लेनदेन स्तर के प्रतिरूप (टीएलएम) के मध्य तुलना की आवश्यकता होती है, उदाहरण के लिए, प्रणाली सी और इसके संबंधित आरटीएल विनिर्देश में लिखा गया है। प्रणाली-ऑन-ए-चिप (एसओसी) डिजाइन वातावरण में इस प्रकार की अन्वेषण के मुख्य रूप से लोकप्रियता बन रही है।

तुल्यकालिक तंत्र तुल्यता

डिजिटल चिप के रजिस्टर ट्रांसफर लेवल (आरटीएल) व्यवहार को सामान्यतः हार्डवेयर विवरण भाषा, जैसे वेरीलॉग या वीएचडीएल के साथ वर्णित किया जाता है। यह विवरण गोल्डन संदर्भ प्रतिरूप है जो विस्तार से वर्णन करता है कि कौन से ऑपरेशन किस घड़ी चक्र के समय और किस हार्डवेयर के भाग द्वारा निष्पादित किए जाएंगे। जब लॉजिक डिज़ाइनर, सिमुलेशन और अन्य सत्यापन विधियों द्वारा, रजिस्टर ट्रांसफर विवरण को सत्यापित कर लेते हैं, तो डिज़ाइन को सामान्यतः तार्किक सिंथेसिस उपकरण द्वारा नेटलिस्ट में परवर्तित किया जाता है। समतुल्यता को कार्यात्मक शुद्धता के साथ भ्रमित नहीं होना चाहिए, जिसे कार्यात्मक सत्यापन द्वारा निर्धारित किया जाना चाहिए।

भौतिक लेआउट में तर्क तत्वों की नियुक्ति के लिए आधार के रूप में उपयोग किए जाने से पूर्व प्रारंभिक नेटलिस्ट सामान्यतः अनुकूलन, परीक्षण के लिए डिजाइन (डीएफटी) संरचनाओं के अतिरिक्त, आदि जैसे कई परिवर्तनों से निकलती है। समसामयिक भौतिक डिज़ाइन सॉफ़्टवेयर कभी-कभी नेटलिस्ट में महत्वपूर्ण संशोधन भी करता है (जैसे तार्किक तत्वों को समतुल्य समान तत्वों के साथ परवर्तित करना जिनके निकट उच्च या निम्न ड्राइव शक्ति एवं क्षेत्र है)। अधिक जटिल, बहु-चरण प्रक्रिया के प्रत्येक चरण के समय, मुख्य कार्यक्षमता और मुख्य कोड द्वारा वर्णित व्यवहार को बनाए रखा जाना चाहिए। जब अंतिम अंटेप-आउट डिजिटल चिप से बना होता है, तो कई भिन्न-भिन्न ईडीए प्रोग्राम और संभवतः कुछ नियमावली संपादन नेटलिस्ट को परवर्तित कर देते हैं।

सिद्धांत रूप में, तर्क संश्लेषण उपकरण आश्वासन देता है कि प्रथम नेटलिस्ट आरटीएल स्रोत कोड के लिए तार्किक तुल्यता है। प्रक्रिया में पश्चात में सभी कार्यक्रम जो नेटलिस्ट में परिवर्तन करते हैं, सैद्धांतिक रूप से यह भी सुनिश्चित करते हैं कि ये परिवर्तन तार्किक रूप से पूर्व संस्करण के समतुल्य हैं।

व्यवहार में, प्रोग्राम में बग होते हैं और यह स्वीकार करना बड़ा अनिष्ट होगा कि अंतिम टेप-आउट नेटलिस्ट के माध्यम से आरटीएल के सभी चरणों को बिना किसी त्रुटि के निष्पादित किया गया है। इसके पश्चात, वास्तविक जीवन में, डिजाइनरों के लिए नेटलिस्ट में नियमावली परिवर्तन करना सामान्य है, जिसे सामान्यतः अभियांत्रिकी परिवर्तन आदेश या ईसीओ के रूप में जाना जाता है, जिससे प्रमुख अतिरिक्त त्रुटि कारक प्रस्तुत होता है। इसलिए, आंख बंदकर यह स्वीकार करने के अतिरिक्त कि कोई त्रुटि नहीं हुई है, डिजाइन के मूल विवरण के नेटलिस्ट के अंतिम संस्करण की तार्किक समानता की अन्वेषण के लिए सत्यापन कार्य की आवश्यकता होती है।

ऐतिहासिक रूप से, तुल्यता की अन्वेषण करने का उपाय अंतिम नेटलिस्ट का उपयोग करके पुन: अनुकरण करना था, परीक्षण की स्थिति में आरटीएल की शुद्धता को सत्यापित करने के लिए विकसित किए गए थे। इस प्रक्रिया को गेट लेवल तर्क अनुकरण कहा जाता है। चूँकि, इसके साथ समस्या यह है कि अन्वेषण की गुणवत्ता केवल परीक्षण विषयो की गुणवत्ता जितनी ही उचित होती है। इसके अतिरिक्त, गेट-लेवल सिमुलेशन निष्पादित करने के लिए प्रसिध्य हैं, बड़ी समस्या यह है कि डिजिटल डिजाइनों का आकार तीव्रता से विस्तारित हो रहा है।

इसका समाधान करने का वैकल्पिक उपाय औपचारिक रूप से यह प्रमाणित करना है कि आरटीएल कोड और संश्लेषित नेटलिस्ट सभी (प्रासंगिक) विषयो में सम्पूर्ण रूप से समान व्यवहार करते हैं। इस प्रक्रिया को औपचारिक तुल्यता अन्वेषण कहा जाता है और यह समस्या है जिसका औपचारिक सत्यापन के व्यापक क्षेत्र के अन्तर्गत अध्ययन किया जाता है।

डिजाइन के किसी भी दो प्रतिनिधित्वों के मध्य औपचारिक तुल्यता अन्वेषण की जा सकती है: आरटीएल <> नेटलिस्ट, नेटलिस्ट <> नेटलिस्ट या आरटीएल <> आरटीएल, चूँकि इसके पश्चात वाला पूर्व दो की तुलना में दुर्लभ है। सामान्यतः, औपचारिक तुल्यता अन्वेषण उपकरण भी त्रुटिहीनता के साथ प्रदर्शित करेगा कि किस बिंदु पर दो अभ्यावेदन के मध्य अंतर है।

विधि

तुल्यता अन्वेषण कार्यक्रमों में बूलियन रीजनिंग के लिए दो बुनियादी प्रौद्यौगिकों का उपयोग किया जाता है:

• द्विआधारी निर्णय आरेख, या बीडीडी बूलियन कार्यों के विषय में तर्क का समर्थन करने के लिए डिज़ाइन की गई विशेष डेटा संरचना है। बीडीडी अपनी दक्षता और बहुमुखी प्रतिभा के कारण अत्यधिक लोकप्रिय हो गए हैं।
• संयोजी सामान्य प्रपत्र संतुष्टि बूलियन संतुष्टि समस्या का समाधान करने वाले प्रस्ताव सूत्र के चर के लिए असाइनमेंट वापस करते हैं जो इसे संतुष्ट करता है यदि ऐसा असाइनमेंट जो लगभग किसी भी बूलियन रीजनिंग समस्या को एसएटी समस्या के रूप में व्यक्त किया जा सकता है।

तुल्यता अन्वेषण के लिए व्यावसायिक अनुप्रयोग

ईडीए के तर्क समतुल्य अन्वेषण (एलईसी) क्षेत्र में प्रमुख उत्पाद हैं:

• मेंटर ग्राफिक्स द्वारा फॉर्मलप्रो
• मेंटर ग्राफिक्स द्वारा क्वेस्टा एसएलईसी
• कैडेंस डिजाइन प्रणाली द्वारा अनुरूप
• कैडेंस डिजाइन प्रणाली द्वारा जैस्परगोल्ड
• सिनोप्सिस द्वारा औपचारिकता
• सिनोप्सिस द्वारा कुलपति औपचारिक
• 360 ईसी वनस्पिन सॉल्यूशंस द्वारा
• एटीईसी प्राद्यौगिकी, इंक द्वारा एटीईसी।

सामान्यीकरण

• रिटिम्ड परिपथ की समतुल्यता अन्वेषण कभी-कभी तर्क को रजिस्टर को स्थान्तरित करने में सहायता करता है, और यह अन्वेषण की समस्या को जटिल बनाता है।
• अनुक्रमिक तुल्यता अन्वेषण : कभी-कभी, संयोजन स्तर पर दो तंत्रें पूर्ण रूप से भिन्न होती हैं, परन्तु समान इनपुट दिए जाने पर समान आउटपुट देना चाहिए। क्लासिक उदाहरण राज्यों के लिए भिन्न-भिन्न एन्कोडिंग वाली दो समान राज्य तंत्रें हैं। चूंकि इसे संयोजन समस्या में कम नहीं किया जा सकता है, अधिक सामान्य तकनीकों की आवश्यकता होती है।
• सॉफ़्टवेयर प्रोग्राम की समतुल्यता, अर्थात अन्वेषण करना कि क्या दो उचित रूप से परिभाषित प्रोग्राम जो N इनपुट लेते हैं और M आउटपुट उत्पन्न करते हैं, समतुल्य हैं: वैचारिक रूप से, आप सॉफ़्टवेयर को स्टेट तंत्र में पर्वर्तित कर सकते हैं (कंपाइलर का संयोजन यही करता है, क्योंकि कंप्यूटर प्लस इसके मेमोरी अधिक बड़ी राज्य तंत्र बनाती है।) फिर, सिद्धांत रूप में, संपत्ति का अन्वेषण के विभिन्न रूप यह सुनिश्चित कर सकते हैं कि वे आउटपुट का उत्पादन करें। यह समस्या अनुक्रमिक तुल्यता अन्वेषण से भी जटिल है, क्योंकि दो कार्यक्रमों के आउटपुट भिन्न-भिन्न समय पर प्रकट हो सकते हैं; परन्तु यह संभव है और शोधकर्ता इस पर कार्य कर रहे हैं।

यह भी देखें

• औपचारिक उपाय

संदर्भ

• Electronic Design Automation For Integrated Circuits Handbook, by Lavagno, Martin, and Scheffer, ISBN 0-8493-3096-3 A survey of the field. This article was derived, with permission, from Volume 2, Chapter 4, Equivalence Checking, by Fabio Somenzi and Andreas Kuehlmann.
• R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers., C-35, pp. 677–691, 1986. The original reference on BDDs.
• Sequential equivalence checking for आरटीएल models. Nikhil Sharma, Gagan Hasteer and Venkat Krishnaswamy. EE Times.

बाहरी संबंध

• CADP – provides equivalence checking tools for asynchronous designs
• OneSpin 360 EC-FPGA – Functional correctness of FPGA synthesis from आरटीएल code to final netlist