Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

माइक्रोचिप्स की अदृश्य दुनिया में, जहाँ अरबों ट्रांजिस्टर स्मार्टफोन से लेकर अंतरिक्ष यान तक सब कुछ चलाने के लिए चालू और बंद होते हैं, एक एकल छिपी हुई त्रुटि पूरे सिस्टम को विनाशकारी रूप से विफल कर सकती है। इंजीनियर इन चिप्स को 'रजिस्टर ट्रांसफर लेवल' (RTL) नामक एक भाषा का उपयोग करके डिजाइन करते हैं, जो यह वर्णन करती है कि समय के साथ डेटा स्टोरेज तत्वों के बीच कैसे घूमता है। यह सुनिश्चित करने के लिए कि ये डिजाइन निर्माण से पहले सही ढंग से काम करें, सत्यापन विशेषज्ञ "असर्शन" (assertion) लिखते हैं। एक 'असर्शन' को डिजाइन के भीतर लिखी गई एक सख्त नियम के रूप में समझें, जो एक कथन है कि, "यदि यह होता है, तो वह अवश्य होना चाहिए।" यदि चिप कभी इस नियम का उल्लंघन करती है, तो सिस्टम अलार्म बजा देता है, जिससे एक ऐसा बग सामने आता है जो अन्यथा अनसुना रह सकता था। दशकों से, इन नियमों को लिखना एक धीमा, मैनुअल और त्रुटिपूर्ण कार्य रहा है, जिसमें इंजीनियरों को यह अनुमान लगाने और उनके लिए विशिष्ट जाँच लिखने की आवश्यकता होती है कि कौन से व्यवहार गलत हो सकते हैं। हालाँकि कंप्यूटर मौजूदा डिजाइन सिमुलेशन से पैटर्न खोजने के लिए खनन (mining) करके मदद करते रहे हैं, लेकिन ये स्वचालित विधियाँ अक्सर सबसे खतरनाक परिदृश्यों को भी चूक जाती हैं क्योंकि वे जिन रैंडम टेस्ट पर निर्भर करती हैं, वे कभी उन तक पहुँच ही नहीं पाते।

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

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

इस दृष्टिकोण के परिणामों का परीक्षण सात अलग-अलग चिप डिजाइनों पर किया गया, जिनमें छोटे आर्बिट्रेशन सर्किट से लेकर जटिल प्रोसेसर कोर तक शामिल थे। नया फ्रेमवर्क पिछले अत्याधुनिक तरीके (state-of-the-art method), जिसे 'SMART' कहा जाता है, की तुलना में लगातार बेहतर प्रदर्शन करता है, जो बिना इस सक्रिय शोधन के सिंगल पास माइनिंग पर निर्भर करता है। इन प्रयोगों में, न्यूरोअसर्शन ने पुराने तरीके की तुलना में लगभग दोगुने असार्टशन्स उत्पन्न किए। अधिक महत्वपूर्ण बात यह है कि इन नियमों की गुणवत्ता काफी अधिक थी। इंजेक्ट की गई त्रुटियों का पता लगाने की उनकी क्षमता के आधार पर मापे जाने पर, नए सिस्टम ने पारंपरिक दृष्टिकोण की तुलना में लगभग दोगुना कवरेज प्राप्त किया। कुछ विशिष्ट बेंचमार्क पर, सुधार और भी नाटकीय था; उदाहरण के लिए, एक प्रोसेसर घटक पर, म्यूटेशन कवरेज लगभग छह प्रतिशत से बढ़कर तीस-दो प्रतिशत से अधिक हो गया। शोधकर्ताओं ने अपने सिस्टम की तुलना एक सीधे दृष्टिकोण से भी की जहाँ एक बड़े लैंग्वेज मॉडल को बिना किसी औपचारिक जाँच या रिफाइनमेंट स्टेप के नियम लिखने के लिए कहा गया था। उस सीधे तरीके ने बहुत कम नियम बनाए और अधिकांश संभावित त्रुटियों को पकड़ने में विफल रहा, जो यह दर्शाता है कि इस उच्च-दांव वाले कार्य के लिए केवल कच्चा भाषा उत्पादन अपर्याप्त है।

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