ফর্মাল এ মাইন্ড-স্ট্রেচারে ইন্টেল কীনোট

প্লেটো দ্বারা প্রকাশিত

অনুসরণকারী: 0

Synopsys SolvNet সাইটে ইন্টেল গ্রাফিক্সের ডাঃ থিও ড্রেন দ্বারা প্রদত্ত একটি আকর্ষণীয় বক্তৃতা পোস্ট করেছে। বিষয় হল ডেটাপথ সমতা যাচাই। অন্য একটি Synopsys VC ফর্মাল DPV অনুমোদনের মতো শোনাতে পারে তবে আপনার এটি যেভাবেই হোক দেখা উচিত। এটি আনুষ্ঠানিকভাবে এর ব্যবহার এবং বিবেচনার উপর একটি মন-প্রসারিত আলোচনা যা আপনাকে রুটিন ব্যবহারকারী-গাইড ধরণের পিচের বাইরে আরও আকর্ষণীয় অঞ্চলে নিয়ে যাবে।

ফর্মালের উপর ইন্টেল কীনোট

নমুনা পরীক্ষা বনাম বৌদ্ধিক বোঝাপড়া

একটি ডিজাইন স্পেসিফিকেশন বা বাস্তবায়নের সঠিকতা যাচাই করার ক্ষেত্রে তার সমস্ত ফর্মের পরীক্ষা-চালিত সিমুলেশন চমৎকার এবং প্রায়ই অপরিবর্তনীয়। এটি শুরু করাও সহজ। শুধু একটি পরীক্ষা প্রোগ্রাম লিখুন এবং অনুকরণ শুরু করুন. কিন্তু সেই সরলতার ফ্লিপ দিক হল যে আমাদের দরকার নেই সম্পূর্ণরূপে আমরা শুরু করার জন্য কি পরীক্ষা করছি তা বুঝুন। আমরা নিজেদেরকে সন্তুষ্ট করি যে আমরা বিশেষত্বটি মনোযোগ সহকারে পড়েছি এবং সমস্ত কোণার কেস বুঝতে পেরেছি, তবে আমাদের বোঝাপড়াকে ছাপিয়ে যেতে খুব বেশি জটিলতা লাগে না।

ফর্মাল আপনাকে গভীর স্তরে কার্যকারিতা বুঝতে উত্সাহিত করে (অন্তত যদি আপনি একটি মূল্যবান ফলাফল দিতে চান)। উপরের উদাহরণে, একটি সহজ প্রশ্ন - z কি কখনও সব 1 এর হতে পারে - একটি সিমুলেটরে এক বিলিয়ন চক্রের মধ্যে একটি উদাহরণ প্রদর্শন করতে ব্যর্থ হয়। অবাক হওয়ার কিছু নেই, যেহেতু এটি একটি চরম কোণার কেস। একটি আনুষ্ঠানিক পরীক্ষা 188 সেকেন্ডের মধ্যে একটি সুনির্দিষ্ট এবং খুব অ-স্পষ্ট উদাহরণ প্রদান করে এবং সামান্য কম সময়ের মধ্যে এটিই একমাত্র ঘটনা প্রমাণ করতে পারে।

ঠিক আছে ফর্মাল যা ডায়নামিক টেস্টিং করতে পারেনি, কিন্তু আরও গুরুত্বপূর্ণভাবে আপনি এমন কিছু শিখেছেন যা সিমুলেটর আপনাকে কখনও বলেনি। শুধুমাত্র একটি সম্ভাব্য কেস ছিল যেখানে সেই অবস্থা ঘটতে পারে। ফর্মাল আপনাকে বুদ্ধিবৃত্তিক স্তরে ডিজাইনটি আরও ভালভাবে বুঝতে সাহায্য করেছে, পরীক্ষার ক্ষেত্রে একটি সীমিত সেট জুড়ে সম্ভাব্য সারাংশের মতো নয়।

বিশেষ সমস্যা

থিওর পরবর্তী উদাহরণ একটি বাগ ভেন্ডিং মেশিনের উপর ভিত্তি করে (একে বলা হয় কারণ আপনি একটি বোতাম টিপলে আপনি একটি বাগ পাবেন)। এটি একটি সুন্দর সহজবোধ্য C থেকে RTL সমতা যাচাইয়ের সমস্যা, বাম দিকে C মডেল, ডানদিকে RTL মডেলের মতো দেখাচ্ছে৷ আনুষ্ঠানিকভাবে তার প্রথম দিনগুলিতে থিওর জন্য একটি আশ্চর্য ছিল যে সি-মডেলে ডান-শিফ্ট আচরণ সি স্ট্যান্ডার্ডে সম্পূর্ণরূপে সংজ্ঞায়িত করা হয়নি, যদিও জিসিসি যুক্তিসঙ্গত আচরণ করবে। যাইহোক, DPV RTL-এর সাথে তুলনা করে অমিলের অভিযোগ করবে, যেমনটি করা উচিত। অনির্ধারিত আচরণ নির্ভর করা একটি বিপজ্জনক জিনিস।

একটি বাগ ভেন্ডিং মেশিন হিসাবে আনুষ্ঠানিক

C এবং RTL এর মধ্যে বিশেষ তুলনা অন্যান্য বিপদের সাথে আসে, বিশেষ করে বিট প্রস্থের কাছাকাছি। একটি মধ্যবর্তী সংকেত (উপরে #3) একটি ক্যারি বিট ছেঁটে ফেলা বা হারানো ভাল উদাহরণ। এই বিশেষ সমস্যা? স্পেক এবং বাস্তবায়ন পছন্দ মধ্যে একটি ধূসর এলাকা হতে পারে.

সমতা যাচাইয়ের বাইরে

DPV-এর প্রাথমিক উদ্দেশ্য, মনে হচ্ছে, একটি C বা RTL রেফারেন্স এবং একটি RTL বাস্তবায়নের মধ্যে সমতা পরীক্ষা করা। তবে সেই প্রয়োজনটি তুলনামূলকভাবে বিরল এবং অন্যান্য কার্যকর উপায় রয়েছে যে এই ধরনের প্রযুক্তি প্রয়োগ করা যেতে পারে, যদি বাক্সের বাইরে একটু। বাস্তবায়নের জগতে প্রথমে একটি ক্লাসিক - আমি একটি পরিবর্তন করেছি, একটি বাগ সংশোধন করেছি - এর ফলে আমি কি কোনো নতুন বাগ প্রবর্তন করেছি? আপনি ঘড়ি গেটিং যোগ করার পরে কিছুটা SEQ চেক করার মতো। ব্লক আউটপুটগুলিতে পৌঁছানোর বিশ্লেষণ কিছু ক্ষেত্রে আরেকটি দরকারী অ্যাপ্লিকেশন হতে পারে।

শুধু সমতা যাচাই নয়

থিও আরও বেশি সৃজনশীল হয়ে ওঠে, প্রশিক্ষণার্থীদের নকশাটি আরও ভালভাবে বুঝতে পাল্টা উদাহরণ ব্যবহার করতে বলে, সুডোকাস সমাধান করুন or পূর্ণসংখ্যাকে ফ্যাক্টরাইজ করুন. তিনি স্বীকার করেন যে DPV-কে এই ধরনের সমস্যাগুলির সাথে যোগাযোগ করার একটি অদ্ভুত উপায় হিসাবে তৈরি করে কিন্তু নির্দেশ করে যে তার উদ্দেশ্য হল এই বিভ্রম ভাঙা যে DPV শুধুমাত্র সমতা যাচাইয়ের জন্য। আকর্ষণীয় ধারণা এবং এই ধরনের চ্যালেঞ্জের মধ্য দিয়ে চিন্তা করা অবশ্যই মস্তিষ্ক-প্রসারিত। (আমি স্বীকার করি যে তিনি এটি উল্লেখ করার সাথে সাথেই আমি সুডোকু সমস্যা সম্পর্কে ভাবতে শুরু করি।)

শেষ করি

থিও উৎপাদনের ব্যবহারে গুরুত্বপূর্ণ পদ্ধতির উপর আলোচনার মাধ্যমে শেষ করেছেন, সীমাবদ্ধতা, রিগ্রেশন এবং লিগ্যাসি RTL মডেলের সাথে তুলনা। এছাড়াও আপনি যা পরীক্ষা করছেন তা আসলে শীর্ষ-স্তরের প্রাকৃতিক ভাষার স্পেসিফিকেশনের সাথে মেলে কিনা তা জানার চ্যালেঞ্জগুলি৷

খুব শক্তিশালী আলোচনা, ভাল দেখার মত এখানে SolvNet এ!

এর মাধ্যমে এই পোস্টটি ভাগ করুন: