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

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

तुल्यता जाँच और अमूर्तता के स्तर

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

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

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

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

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

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

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

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

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

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

तरीके

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

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

तुल्यता जाँच के लिए व्यावसायिक अनुप्रयोग

EDA के तर्क समतुल्य जाँच (LEC) क्षेत्र में प्रमुख उत्पाद हैं:

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