گراف AND-NOT

https://

این مقاله در حال ترجمه از ویکی انگلیسی است لطفا حذف نشود.

en.wikipedia.org/wiki/And-inverter graph

 گراف AND-NOT 
گراف AND-NOT (And-inverter graph - AIG) , یک گراف جهت‌دار و غیرمدور است که پیاده‌سازی ساختاری عملکرد منطقی یک مدار یا شبکه را نمایش می‌دهد. یک AIG از گره‌های دو ورودی که نشان‌دهندهٔ عطف منطقی (Logical Conjunction) هستند، گره‌های پایانی با برچسب نام متغیرها و یال‌هایی که به صورت اختیاری شامل نشانگرهایی برای نفی منطقی (Logical Negation) می‌باشند، تشکیل شده است. این نمایش از یک تابع منطقی به ندرت برای مدارهای بزرگ از نظر ساختاری کارآمد است، اما یک نمایش کارآمد برای دستکاری توابع بولی (Boolean functions) محسوب می‌شود. به طور معمول، این گراف انتزاعی به عنوان یک ساختار داده در نرم‌افزار نمایش داده می‌شود.

تبدیل از شبکه‌ای از گیت‌های منطقی به AIGها سریع و مقیاس‌پذیر است. این تبدیل تنها نیاز دارد که هر گیت بر حسب گیت‌های AND و اینورترها بیان شود. این تبدیل منجر به افزایش غیرقابل پیش‌بینی در مصرف حافظه و زمان اجرا نمی‌شود. این ویژگی AIG را به یک نمایش کارآمد در مقایسه با نمودار تصمیم دودویی (BDD) یا فرم «مجموع حاصل‌ضرب‌ها» (ΣoΠ) تبدیل می‌کند، که همان فرم متعارف در جبر بولی است و با نام فرم نرمال فصلی (DNF) شناخته می‌شود . BDD و DNF را نیز می‌توان به عنوان مدار مشاهده کرد، اما آن‌ها شامل محدودیت‌های رسمی هستند که مقیاس‌پذیری آن‌ها را کاهش می‌دهند. برای مثال، ΣoΠها مدارهایی با حداکثر دو سطح هستند، در حالی که BDDها متعارف هستند، به این معنی که لازم است متغیرهای ورودی در تمام مسیرها به ترتیب یکسانی ارزیابی شوند.

 تاریخچه 
مدارهایی که از گیت‌های ساده تشکیل شده‌اند، از جمله AIGها، موضوعی «قدیمی» در تحقیقات هستند. علاقه به AIGها با مقاله پیشگامانه آلن تورینگ در سال ۱۹۴۸ [۱] در مورد شبکه‌های عصبی آغاز شد، که در آن او یک شبکه آموزش‌پذیر تصادفی از گیت‌های NAND را توصیف کرد. این علاقه در اواخر دهه ۱۹۵۰ [۲] و سپس در دهه ۱۹۷۰ که تبدیل‌های محلی مختلفی توسعه یافتند، ادامه پیدا کرد. این تبدیل‌ها در چندین سیستم سنتز و تأیید منطقی، مانند Darringer و همکاران [۳] و Smith و همکاران [۴]، پیاده‌سازی شدند. این سیستم‌ها مدارها را برای بهبود سطح و تأخیر در طول سنتز، یا برای تسریع در بررسی هم‌ارزی صوری، کاهش می‌دهند. چندین تکنیک مهم در اوایل در IBM کشف شد، مانند ترکیب و استفاده مجدد از عبارات و زیرعبارات منطقی چند ورودی، که اکنون به عنوان درهم‌سازی ساختاری (structural hashing) شناخته می‌شود.

اخيراً علاقه مجددی به AIGها به عنوان یک نمایشگر تابعی برای کارهای مختلف در سنتز و تأیید به وجود آمده است. دلیل این امر این است که نمایش‌های محبوبی که در دهه ۱۹۹۰ رایج بودند (مانند BDDها)، در بسیاری از کاربردهای خود به محدودیت‌های مقیاس‌پذیری رسیده‌اند . یک پیشرفت مهم دیگر، ظهور اخیر حل‌کننده‌های کارآمدتر ارضاپذیری بولی (SAT) است. هنگامی که این حل‌کننده‌ها با AIGها به عنوان نمایش مدار ترکیب می‌شوند، منجر به سرعت‌های قابل توجهی در حل طیف گسترده‌ای از مسائل بولی می‌شوند .

 کاربردها 
AIGها کاربرد موفقی در کاربردهای متنوع اتوماسیون طراحی الکترونیک (EDA) پیدا کرده‌اند. ترکیب مناسبی از AIGها و ارضاپذیری بولی، تأثیری بر تأیید صوری گذاشته است، که شامل بررسی مدل (model checking) و بررسی هم‌ارزی (equivalence checking) [۵] می‌شود. یک کار اخیر دیگر نشان می‌دهد که می‌توان از AIGها برای توسعه تکنیک‌های فشرده‌سازی کارآمد مدار استفاده کرد [۶]. در حال حاضر این درک رو به رشد وجود دارد که مسائل سنتز منطقی و فیزیکی را می‌توان با استفاده از شبیه‌سازی و ارضاپذیری بولی برای محاسبه خواص تابعی (مانند تقارن‌ها) [۷] و انعطاف‌پذیری گره (مانند عبارات بی‌اهمیت، جایگزینی‌های مجدد و SPFDها) [۸] [۹] [۱۰] حل کرد. Mishchenko و همکاران نشان می‌دهند که AIGها یک نمایش یکپارچه امیدوارکننده هستند که می‌تواند سنتز منطقی، نگاشت فناوری، سنتز فیزیکی و تأیید صوری را به هم مرتبط سازد. این امر تا حد زیادی به دلیل ساختار ساده و یکنواخت AIGها است که به بازنویسی، شبیه‌سازی، نگاشت، جایابی و تأیید اجازه می‌دهد تا از یک ساختار داده مشترک استفاده کنند.

 منطق ترتیبی 
علاوه بر منطق ترکیبی، AIGها در مورد منطق ترتیبی و تبدیل‌های ترتیبی نیز به کار گرفته شده‌اند. به طور خاص، روش درهم‌سازی ساختاری توسعه یافت تا برای AIGهایی با عناصر حافظه (مانند فلیپ‌فلاپ‌های نوع D با یک حالت اولیه، که به طور کلی می‌تواند نامشخص باشد) کار کند، که در نتیجه یک ساختار داده‌ای ایجاد شده که به طور خاص برای کاربردهای مرتبط با زمان‌بندی مجدد (retiming) [۱۱] تنظیم شده است.

 تحقیقات جاری 
تحقیقات جاری شامل پیاده‌سازی یک سیستم سنتز منطقی مدرن است که به طور کامل بر پایه AIGها بنا شده باشد. نمونه اولیه این سیستم که **ABC** نامیده می‌شود، شامل یک بسته AIG، چندین تکنیک سنتز و بررسی هم‌ارزی مبتنی بر AIG، و همچنین یک پیاده‌سازی آزمایشی از سنتز ترتیبی است. یکی از این تکنیک‌ها، نگاشت فناوری و زمان‌بندی مجدد را در یک مرحله بهینه‌سازی واحد ترکیب می‌کند. این بهینه‌سازی‌ها را می‌توان با استفاده از شبکه‌های متشکل از گیت‌های دلخواه نیز پیاده‌سازی کرد، اما استفاده از AIGها آن‌ها را مقیاس‌پذیرتر و پیاده‌سازی‌شان را آسان‌تر می‌سازد.

 پیاده‌سازی‌ها 

 سیستم تأیید و سنتز منطقی http://www.eecs.berkeley.edu/~alanmi/abc/
 مجموعه‌ای از ابزارها برای AIGها http://fmv.jku.at/aiger/index.html
 https://web.archive.org/web/20150924101539/http://www.si2.org/openeda.si2.org/help/group_ld.php?group=73
 کتابخانه منطق http://godoc.org/github.com/go-air/gini/logic

 همچنین ببینید 

 نمودار تصمیم دودویی https://en.wikipedia.org/wiki/Binary_decision_diagram 
 عطف منطقی https://en.wikipedia.org/wiki/Logical_conjunction

 منابع 

 https://en.wikipedia.org/wiki/And-inverter_graph#cite_ref-1
 https://en.wikipedia.org/wiki/And-inverter_graph#cite_ref-2