औपचारिक तुल्यता परीक्षण
औपचारिक तुल्यता जाँच प्रक्रिया इलेक्ट्रॉनिक डिजाइन स्वचालन (EDA) का भाग है, जिसका उपयोग सामान्यतः डिजिटल सर्किट एकीकृत सर्किट के विकास के समय किया जाता है, औपचारिक रूप से यह साबित करने के लिए कि सर्किट डिज़ाइन के दो प्रतिनिधित्व पूर्ण रूप से समान व्यवहार प्रदर्शित करते हैं।
तुल्यता जाँच और अमूर्तता के स्तर
सामान्यतः, कार्यात्मक तुल्यता की संभावित परिभाषाओं की विस्तृत श्रृंखला होती है, जिसमें अमूर्तता के विभिन्न स्तरों और समय के विवरण की भिन्न-भिन्न ग्रैन्युलैरिटी के बीच तुलना सम्मलित होती है।
- सबसे सामान्य दृष्टिकोण मशीन तुल्यता की समस्या पर विचार करना है जो दो तुल्यकालिक सर्किट विनिर्देशों को कार्यात्मक रूप से समतुल्य परिभाषित करता है, अगर घड़ी दर घड़ी, वे इनपुट सिग्नल के किसी भी वैध अनुक्रम के लिए आउटपुट सिग्नल के समान अनुक्रम का उत्पादन करते हैं।
- माइक्रोप्रोसेसर डिज़ाइनर एक स्थानांतरण स्तर दर्ज करें (RTL) कार्यान्वयन के साथ निर्देश समुच्चय आर्किटेक्चर (ISA) के लिए निर्दिष्ट कार्यों की तुलना करने के लिए तुल्यता जाँच का उपयोग करते हैं, यह सुनिश्चित करते हुए कि दोनों मॉडलों पर निष्पादित कोई भी प्रोग्राम मुख्य मेमोरी सामग्री के समान अद्यतन का कारण बनेगा। यह अधिक सामान्य समस्या है।
- एक सिस्टम सी डिजाइन प्रवाह के लिए लेनदेन स्तर के मॉडल (टीएलएम) के बीच तुलना की आवश्यकता होती है, उदाहरण के लिए, सिस्टमसी और इसके संबंधित आरटीएल विनिर्देश में लिखा गया है। सिस्टम-ऑन-ए-चिप (एसओसी) डिजाइन वातावरण में इस तरह की जांच बढ़ती दिलचस्पी बन रही है।
तुल्यकालिक मशीन तुल्यता
डिजिटल चिप के रजिस्टर ट्रांसफर लेवल (आरटीएल) व्यवहार को सामान्यतः हार्डवेयर विवरण भाषा, जैसे Verilog या वीएचडीएल के साथ वर्णित किया जाता है। यह विवरण गोल्डन रेफरेंस मॉडल है जो विस्तार से वर्णन करता है कि कौन से ऑपरेशन किस घड़ी चक्र के दौरान और किस हार्डवेयर के टुकड़े द्वारा निष्पादित किए जाएंगे। एक बार जब लॉजिक डिज़ाइनर, सिमुलेशन और अन्य सत्यापन विधियों द्वारा, रजिस्टर ट्रांसफर विवरण को सत्यापित कर लेते हैं, तो डिज़ाइन को सामान्यतः लॉजिक सिंथेसिस टूल द्वारा 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.
