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

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

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

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

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

तुल्यकालिक मशीन तुल्यता

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

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

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

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

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

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

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

तरीके

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

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

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

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

• मेंटर ग्राफिक्स द्वारा फॉर्मलप्रो
• मेंटर ग्राफिक्स द्वारा क्वेस्टा एसएलईसी
• ताल डिजाइन सिस्टम द्वारा अनुरूप
• कैडेंस डिजाइन सिस्टम्स द्वारा जैस्परगोल्ड
• सिनोप्सिस द्वारा औपचारिकता
• सिनोप्सिस द्वारा कुलपति औपचारिक
• 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