تأیید رسمی: جریان و اشکال زدایی Synopsys Formality

آنچه یاد خواهید گرفت:

• راه‌اندازی و اجرای Synopsys Formality را با اطمینان انجام دهید.
• مخروط‌های منطقی و نقاط مقایسه را درک و شناسایی کنید.
• طراحی‌های مرجع و پیاده‌سازی را به‌درستی بارگذاری کنید.
• فایل‌های راهنما (SVF) و فرمان های راه‌اندازی را اعمال کنید.
• گزارش‌های تطبیق، تأیید و شکست را تفسیر کنید.
• شکست‌های تأیید در دنیای واقعی را اشکال زدایی کنید.
• طراحی‌ها را با اثبات هم‌ارزی عملکردی تأیید نهایی کنید.

پیش‌نیازهای دوره

• درک اولیه از طراحی منطق دیجیتال (گیت‌ها، فلیپ‌فلاپ‌ها، منطق ترکیبی)
• آشنایی با مفاهیم RTL (Verilog/VHDL) مفید است اما الزامی نیست.
• هیچ تجربه‌ی قبلی با ابزارهای تأیید رسمی لازم نیست - دوره از مبانی شروع می‌شود.
• برای بخش‌های آزمایشگاهی، به رایانه‌ای نیاز دارید که بتواند Synopsys Formality را اجرا کند. (یا دسترسی به سروری که ابزار روی آن نصب است)

توضیحات دوره

قدرت تأیید رسمی را آزاد کنید و دیگر هفته‌ها را صرف شبیه‌سازی‌های غیرضروری نکنید.

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

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

چه چیزی این دوره را متفاوت می‌کند؟

مدرس تنها تئوری آموزش نمی‌دهد. کل جریان Formality را از ابتدا تا انتها مرور می‌کند و سپس آن را در سه آزمایشگاه عملی به کار می‌برد؛ جایی که طراحی‌های واقعی را بارگذاری می‌کنید، تطبیق و تأیید را اجرا می‌کنید و نتایج را تفسیر می‌کنید. اما چون در مهندسی واقعی همیشه همه‌چیز با تیک سبز تمام نمی‌شود، یک بخش کامل را به موارد اشکال زدایی اختصاص داده است - دقیقاً نشان می‌دهد چگونه نقاط مقایسه‌ی ناموفق را تحلیل کنید، مخروط‌های منطقی را دنبال کنید و ناهماهنگی‌ها را برطرف کنید.

سرفصل دوره:

• درس 1: مقدمه‌ای بر تأیید رسمی - چرا تأیید رسمی؟ چه زمانی از آن استفاده کنیم؟ گزینه‌های ابزار.
• درس 2: اجزای تأیید رسمی و بررسی هم‌ارزی طراحی - بررسی عمیق مخروط‌های منطقی، نقاط مقایسه و مفهوم تطبیق.
• درس 3: جریان Formality - مرور کامل از اجرای ابزار تا گزارش‌دهی، شامل فرمان های مهمی مانند set_svf، set_constant و set_dont_verify_points
• درس 4: آزمایشگاه 1 - تأیید رسمی اولیه - اولین طراحی‌ها را بارگذاری کنید و یک تأیید موفق اجرا کنید.
• درس 5: آزمایشگاه 2 - تأیید سطح متوسط - مدیریت حالت‌های اسکن و ثابت‌ها
• درس 6: آزمایشگاه 3 - تأیید پیچیده - کار با راهنمایی‌های SVF و تحلیل گزارش‌های تطبیق.
• درس 7: موارد اشکال زدایی - سناریوهای واقعی شکست - ردیابی، تحلیل و رفع آن‌ها را بیاموزید.

این دوره برای چه کسانی مناسب است؟

• مهندسان طراحی ASIC/FPGA که می‌خواهند نتایج سنتز خود را با RTL اصلی مطابقت دهند.
• دانشجویان طراحی دیجیتال که می‌خواهند جریان‌های تأیید نهایی استاندارد صنعت را درک کنند.
• توسعه‌دهندگان جریان CAD که نیاز به پیاده‌سازی تأیید رسمی در گردش‌کارهای طراحی دارند.
• هر فردی که در طراحی تراشه‌های دیجیتال نقش دارد و می‌خواهد فراتر از شبیه‌سازی برود و از متدهای تأیید اثبات‌شده‌ی ریاضی استفاده کند.