تیم های طراحی می دانند که تأیید صحت عبور دامنه ساعت (CDC) یک کار مهم برای تأیید است، اما بسیاری از تیم های طراحی فقط ساختارهای هماهنگ سازی CDC را بطور آماری تأیید می کنند. ساختارهای هماهنگ سازی پروتکل CDC به تنهایی از بروز خطاهای CDC جلوگیری نمی کند ، زیرا استفاده نادرست همگام ساز منجر به از بین رفتن داده ها ، خرابی داده ها یا در بدترین حالت قابل تغییرپذیری آنها خواهد شد.

تأیید پروتکل CDC با استفاده از اعلامیه ، از استفاده نادرست همگام ساز جلوگیری می کند ، اما تأیید پروتکل سنتی دشوار و وقت گیر است. برای جلوگیری از چالش های تأیید پروتکل سنتی که یک کار بسیار پیچیده را برای مهندسان طراحی و تأیید ایجاد می کند ، یک روش خودکار لازم است.

در اینجا چالش هایی با روش های سنتی تأیید پروتکل CDC وجود دارد:

برای تنظیم طرح و ادعاهای رسمی و شبیه سازی ، تلاش و زمان زیادی لازم است
تلاش پیچیده و درگیر برای ادغام بین تجزیه و تحلیل ساختاری ، تأیید رسمی و ابزار شبیه سازی
تلاش قابل توجه مورد نیاز برای بررسی و اشکال زدایی به صورت رسمی و شبیه سازی

در این مقاله ، یک متدولوژی را توصیف می کنیم که تنظیم خودکار تنظیمات ، محدودیت ها و نتایج را به صورت خودکار انجام می دهد زیرا طرح، از آنالیز CDC استاتیک به سمت تأیید رسمی به شبیه سازی حرکت می کند. اتوماسیون ارائه شده توسط این روش از تلاشهای اسکریپت دستی جلوگیری می کند و در نتیجه تلاشهای تنظیم شده و خطاهای تنظیم را کاهش می دهد. این روش همچنین با پرداختن به مسئله مهم در ارتباط تجزیه و تحلیل ساختاری ، تأیید رسمی و نتایج شبیه سازی ، بهره وری از اشکال زدایی طراح را بهبود می بخشد.

پروتکل های CDC چیست و چرا مورد نیاز هستند؟

طرح های پیچیده امروزی شامل چندین ساعت ناهمزمان است. عبور سیگنالها بین حوزه های ساعت ناهمزمان ممکن است منجر به خطاهای عملکردی شود. هنگامی که یک سیگنال از یک دامنه ساعت ناهمزمان توسط یک رجیستر در یک دامنه ساعت ناهمزمان مختلف نمونه برداری می شود ، نیاز زمان تنظیم / نگه داشتن به ناچار در مقصد نقض می شود و این رجیستر قابل تغییر خواهد بود. هنگامی که طراحان برای جلوگیری از انتشار این رویدادهای بزرگ ، منطق هماهنگ سازی را اضافه می کنند ، طراحان باید پروتکل صحیح CDC مرتبط با ساختار منطق را پیاده سازی و تأیید کنند. بدون پروتکل به درستی اجرا شده ، یک ساختار CDC به درستی کار نخواهد کرد و بدین ترتیب داده ها را از دست داده یا خراب می شود.

اگرچه ساختارهای هماهنگ سازی CDC برای جلوگیری از استعمال در مسیرهای CDC لازم است ، اما طراحان غالباً از این واقعیت غافلند که یک ساختار منطقی خوب به تنهایی برای جلوگیری از خطاهای CDC کافی نیست. اگر هماهنگ کننده CDC به درستی مورد استفاده قرار نگیرد ، ممکن است مسیر CDC باعث از دست رفتن داده یا خراب شدن داده یا در بدترین حالت قابل استرداد شود. قوانینی که استفاده صحیح از هماهنگ کننده CDC را تعریف می کنند ، پروتکل های CDC نامیده می شوند.

در ساده ترین پرونده پروتکل ، یک هماهنگ کننده 2DFF به یک پروتکل ثبات نیاز دارد که در آن داده های انتقال باید حداقل برای دو چرخه ساعت دریافت پایدار، نگه داشته شوند، تا ثبات RX بتواند با اطمینان از داده های TX همگام سازی کند و از خرابی داده یا از دست دادن داده جلوگیری کند. در یک پرونده پروتکل پیچیده تر ، یک هماهنگ کننده data-mux (DMUX) نیاز دارد که هنگام فعال بودن mux ، داده های TX پایدار باشند و به رجیستر RX اجازه می دهد تا داده های TX را نمونه برداری کند. اگر پروتکل هماهنگ کننده DMUX نقض شود، رجیستری RX قابل تبدیل خواهد شد.

شکل 1. قوانین پروتکل DMUX

خطاهای پروتکل CDC باید در اوایل چرخه طراحی شناسایی شوند، در غیر این صورت در مراحل بعدی می توانند منجر به خرابی عملکرد شوند. این خرابی های عملکردی می تواند منجر به افزایش تکرارها و حتی چرخش مجدد سیلیکون شود. برای اطمینان از، از دست رفتن چنین مواردی ، مهندسین طراحی و تأیید پروتکل های هماهنگ کننده با ایجاد ادعای مربوط به پروتکل های هماهنگ کننده و تأیید آنها با استفاده از تکنیک های بررسی و مدل سازی رسمی ، تأیید می کنند.

چالش های تأیید پروتکل CDC

تأیید پروتکل برای جلوگیری از خطاهای CDC بسیار مهم است ، اما اغلب تیم های پروژه به دلیل تعداد چالش های استقرار، از تأیید پروتکل استفاده نمی کنند. چالش های مشترک برای استقرار شامل تأیید پروتکل ، تنظیم محدودیت ها و دشواری در بررسی و اشکال زدایی نتایج پروتکل است.

ایجاد ادعای پروتکل و تأیید چالش های تنظیم شده

تجزیه و تحلیل ساختاری CDC ساختارهای هماهنگ سازی CDC را مشخص می کند ، سپس ابزارهای CDC بطور خودکار ادعای پروتکل را برای سازه های همگام سازی CDC ایجاد می کنند. برنامه های CDC ، لحظه های ادعایی را ایجاد می کنند که رجیستر TX ، ثبات RX ، ساعت TX ، ساعت RX ، تنظیم مجدد TX و تنظیم مجدد RX را به ادعای پروتکل مناسب وصل می کنند.

پس از اظهارات پروتکل CDC ، می تواند برای طراحان دشوار باشد که این ادعاها را در محیط های تأیید رسمی و شبیه سازی قرار دهند. برای طراحان نا آشنا و مبتدی با تجزیه و تحلیل رسمی ، تولید اسکریپت های اجرا شده و تجزیه و تحلیل رسمی دشوار است. برای محیط های شبیه سازی پیچیده ، ترکیب ادعاهای پروتکل در رگرسیون های شبیه سازی چالش برانگیز است.

محدودیت های رسمی تولید چالش ها

محیط رسمی، جهت محدودیت های رسمی تنظیمات به طراحان نیاز دارد ،که شامل اطلاعات پیکربندی طراحی ، اطلاعات ساعت و اطلاعات درگاه ورودی است. اطلاعات پیکربندی طراحی رسمی شامل ثابت هایی است که برای درگاه ها و ثبات های تنظیمات مشخص شده است. اطلاعات رسمی ساعت شامل مشخصات ساعت طراحی و فرکانس های ساعت است. اطلاعات درگاه رسمی شامل مشخصات درگاه های ورودی اصلی و اطلاعات دامنه ساعت مربوط به آنها می باشد. برای مهندسان ناآشنا با تجزیه و تحلیل رسمی ، این مشخصات می تواند یک کار دلهره آور باشد.

چالش های اشکال زدایی ادعای پروتکل CDC

در روشهای سنتی پروتکل CDC ، بررسی تأیید پروتکل و اشکال زدایی از تجزیه و تحلیل ساختاری CDC جدا شده است. این ارتباط طراحان پروتکل را در شبیه سازی یا محیط رسمی با ساختار هماهنگ سازی CDC مرتبط را برای طراحان دشوارتر می کند. این عدم همبستگی بین تأیید ساختاری و پروتکل باعث می شود که طراحان برای بررسی و اشکال زدایی نتایج تأیید پروتکل ، وقت و تلاش بیشتری را صرف کنند.

متدولوژی پروتکل CDC خودکار

در پاسخ به این چالش ها و نیازها ، ما یک متدولوژی خودکار ایجاد کردیم که نه تنها به غلبه بر چالش های متداول روش های تأیید پروتکل سنتی کمک می کند ، بلکه همچنین بهتر می تواند مدل های رسمی بررسی و فن آوری های شبیه سازی رسمی را به منظور بهبود نتایج تأیید پروتکل ادغام کند.

شکل 2. جریان تأیید خودکار پروتکل

اصول گردش کار خودکار

این روش خودکار دارای یک گردش کار است که از چهار مرحله تشکیل شده است.

تجزیه و تحلیل استاتیک CDC

تجزیه و تحلیل استاتیک CDC تجزیه و تحلیل استاتیک CDC را بر روی طرح انجام می دهد تا اطمینان حاصل شود که تمام مسیرهای مربوط به CDC با استفاده از هماهنگ کننده های مناسب همگام شده اند. علاوه بر این ، به طور خودکار ادعاهای پروتکل ، محدودیت های تأیید رسمی را ایجاد می کند و تأیید رسمی و تنظیمات شبیه سازی تولید می کند.

تولید ادعای پروتکل خودکار: بر اساس تجزیه و تحلیل استاتیک CDC ، ابزار تولید پروتکل CDC اظهارات پروتکل ویژه برای هر نوع هماهنگ کننده CDC را ایجاد می کند (شکل 3)

شکل 3. ادعای پروتکل CDC

تولید محدودیت های تأیید خودکار رسمی: ابزار تولید پروتکل CDC اطلاعات محدودیت CDC برای سیگنال های ثابت ، پایدار و خاکستری را به تأیید SVA برای تأیید رسمی تبدیل می کند. بعلاوه ، اطلاعات دامنه ساعت پورت ورودی و خروجی به محدودیت های رسمی تبدیل می شوند تا دقت نمونه های رسمی متضاد را بهبود بخشند.
تأیید خودکار رسمی و تنظیم شبیه سازی: ابزار تولید پروتکل CDC تولید اسکریپت های اجرا شده را با بررسی مدل رسمی تولید می کند. این ابزار همچنین یک فایل استدلالی شبیه سازی ایجاد می کند تا به محیط شبیه سازی موجود طراح اضافه شود ، بنابراین طراحان می توانند به راحتی ادعای پروتکل را اضافه کنند و از اضافه کردن دستی چندین ادعا جلوگیری کنند و پرونده های ماژول را به شبیه سازی خود متصل کنند.

آنالیز رسمی

تجزیه و تحلیل رسمی با اجرای مدل رسمی ، اسکریپت ها را بررسی می کند و اسکریپت ها را اجرا می کند تا ادعای پروتکل همگام ساز خودکار را با استفاده از تنظیم تأیید رسمی تولید شده بررسی کند. تنظیم رسمی خودکار به طور قابل توجهی تلاش مورد نیاز برای تنظیم طرح را برای تجزیه و تحلیل رسمی کاهش می دهد و همچنین از تلاش اشکال زدایی برای حل مسائل ناقص یا نادرست تنظیم جلوگیری می کند.

یک اثبات رسمی برای هرگونه ادعای پروتکل نشان می دهد، که پروتکل هرگز نمی تواند برای ساختار هماهنگ سازی CDC همراه نقض شود ، بنابراین ساختار از بین رفتن داده ها ، فساد داده ها و انتشار استعمال مصون است. برای طراحان فاقد تخصص رسمی بررسی مدل ، اشکال زدایی و یا رفع ادعاهای اخراج و غیرقابل حل دشوار است ، بنابراین به جای اشکال زدایی در این موارد دشوار ، طراحان این ادعاها را به سمت شبیه سازی ارتقا می دهند.

شبیه سازی

شبیه سازی با اضافه کردن پرونده های تنظیم خودکار تولید شده به محیط شبیه سازی موجود ، ادعاهای پروتکل اثبات نشده را تأیید می کند. ابزار تولید پروتکل CDC فایلهای آرگومان شبیه سازی را برای جمع آوری و شبیه سازی تولید می کند.

در طول تحلیل رسمی ، اسکریپت آنالیز رسمی به طور خودکار پرونده های شبیه سازی را به روز می کند تا ادعاهای اثبات شده را از لیست ادعاهای شبیه سازی حذف کند. حذف ادعاهای اثبات شده از شبیه سازی، باعث کاهش زمان اجرای شبیه سازی و تلاش برای بررسی نتایج شبیه سازی برای ادعاهای اثبات شده می شود که در شبیه سازی نقض نمی شوند.

هرگونه ادعا شبیه سازی نشان دهنده ی نقض پروتکل هماهنگ کننده CDC است که منجر به از دست دادن داده ها ، خرابی داده ها یا انتشار پذیری فوق العاده در مسیر CDC مرتبط می شود. برای رعایت قوانین پروتکل همگام ساز ، طراحان باید شلیک های شبیه سازی را اشکال زده و منطق CDC را اصلاح کنند.

نتایج پروتکل CDC را مرور و اشکال زدایی کنید

نتایج اولیه پروتکل CDC را با اولین بار بررسی تجزیه و تحلیل ساختاری کل CDC ، تأیید رسمی و نتایج شبیه سازی بررسی و اشکال زدایی کنید. همبستگی بین چندین فناوری (تجزیه و تحلیل استاتیک CDC ، بررسی مدل رسمی و شبیه سازی) به طراحان این امکان را می دهد تا سریعتر و راحت تر خطاها را حل کنند. این همبستگی طراحان را قادر می سازد ساختار CDC مرتبط با خرابی پروتکل را پیدا کنند ، سپس به سرعت علت خطای پروتکل را تشخیص دهند. این بررسی و اشکال زدایی بهبود یافته تضمین می کند که اشکالات به طور صحیح مورد تجزیه و تحلیل قرار گرفته و خطاهای پروتکل برای هماهنگ کننده CDC از دست رفته یا نادرست مورد تجزیه و تحلیل قرار نگیرند.

نتایج دنیای واقعی

استقرار روش خودکار تأیید پروتکل در طرح های واقعی شواهدی از کاهش طراحی و تلاش برای تأیید و بسته شدن سریعتر طراحی را فراهم کرده است. هنگامی که متدولوژی خودکار روی مجموعه ای از طرح ها انجام شد ، از 1 تا 30 میلیون دروازه ، پیشرفت های زیر محقق شد (به جداول 1 و 2 مراجعه کنید):

کاهش قابل توجه در زمان تنظیم رسمی. با توجه به اتوماسیون تولید راه اندازی و کاهش تکرار اشکال زدایی افزایشی برای تنظیمات ناقص و نادرست ، زمان کلی تنظیم رسمی 3-5 برابر کاهش می یابد.
کاهش در زمان تنظیم برای شبیه سازی. با توجه به اتوماسیون تنظیم نسل و کاهش تکرار اشکال زدایی افزایشی برای تنظیمات ناقص و نادرست ، زمان تنظیم شبیه سازی کلی 6-17 برابر کاهش یافته است.
کاهش در شلیک های دروغین در تجزیه و تحلیل رسمی. تولید خودکار راه اندازی و وارد کردن محدودیت های طراحی CDC به آنالیز رسمی ، خطاهای تنظیم رسمی را کاهش داده و باعث کاهش شلیک های دروغین می شود. شلیک ادعای رسمی 59٪ -68٪ کاهش یافت.
افزایش پوشش رسمی. تنظیم رسمی و محدودیت ها منجر به ادعاهای کم نتیجه ای، اثبات و شلیک های بیشتر شد.
افزایش پوشش شبیه سازی. از آنجا که ادعاهای اثبات شده در روش پیشنهادی شبیه سازی نشده اند ، ادعاهای اثبات شده برای حفظ قوام پوشش شبیه سازی بین روش های سنتی و پیشنهادی تحت پوشش قرار گرفته اند.
کاهش زمان و تلاش برای تأیید شبیه سازی. به دلیل محرومیت از ادعاهای رسمی اثبات شده ، کاهش تعداد ادعاهای منتقل شده به شبیه سازی وجود دارد و در نتیجه تلاش تأیید لازم برای بررسی ادعاهای اثبات شده در شبیه سازی کاهش می یابد. همبستگی تجزیه و تحلیل ساختاری CDC ، تأیید رسمی و نتایج شبیه سازی باعث بهبود بهره وری از اشکال زدایی شده و به همبستگی آسان تر خطاهای پروتکل با مسیرهای CDC مرتبط آنها منجر شده است. زمان و تلاش برای بررسی نتایج شبیه سازی و اشکال زدایی برای این مطالعات موردی اندازه گیری نشده است.

در طول تأیید ، موارد زیر بی تأثیر نبودند:

حداقل تغییر در زمان اجرا شبیه سازی. کاهش تعداد ادعاهای اجرا شده در شبیه سازی به دلیل محرومیت از ادعاهای رسمی اثبات شده ، مدت زمان شبیه سازی را به طور قابل توجهی تغییر نمی دهد.

نتیجه گیری در مورد تأیید پروتکل CDC خودکار

این روش تأیید پروتکل CDC خودکار یک راه حل منظم و تکرار شونده برای دستیابی به بسته شدن در تأیید پروتکل CDC است. فرایند راه اندازی خودکار خطاهای تنظیم شده و تکرار اشکال زدایی لازم، برای حل مشکلات تنظیم را کاهش می دهد. تبدیل خودکار محدودیت های CDC به محدودیت های بررسی مدل رسمی ، دقت تحلیل رسمی را بهبود می بخشد و شلیک های رسمی کاذب را کاهش می دهد. سرانجام ، تجزیه و تحلیل ساختاری یکپارچه CDC ، تأیید رسمی و نتایج شبیه سازی ، امکان استفاده آسانتر از محیط اشکال زدایی را فراهم می کند که به طراحان اجازه می دهد خطاهای پروتکل را سریعتر و با تلاش کمتری مرتفع سازی و رفع کنند.