سخت‌افزارها و مدارهای منطقی راه درازی را پیموده‌اند. ترانزیستورهای استفاده شده در یك مدار سادة CPU چندین میلیون بار كوچكتر از ترانزیستور اصلی ساخته شده درسال 1947 است. اگر یك ترانزیستور حال حاضر با تكنولوژی 1947 ساخته شود نیازمند یك كیلومتر مربع سطح می‌باشد (قانون مور)، در حالی كه در 10 الی 20 سال آینده تكنولوژی موفق به گشودن راهی جهت تولید مدارهای منطقی 3 بعدی خواهد شد.

در این میان، چندین پرسش سخت و پژوهشی كه در آكادمی‌ها وصنعت به آن پرداخته می‌شود وجود دارد:

1)گرفتن پیچیدگی‌ها در تحلیل روش‌های تولید SWITCH ،در روش‌های متولد شده به منظور مدل‌سازی چگونگی كارآئی آنها، در مدارهای منطقی مورد نیاز مهندسان، و امتیازات روش‌های نوین فناورانه بر روش های كلاسیك.

2) لحاظ كردن ملاحظاتی مبنی بر تعداد سوئیچ‌ها در واحد سطح و حجم در درون ابزار (گنجایش)، تعداد نهائی سوئیچ‌ها در درون ابزار (حجم)، شرایط حدی عملگرها، سرعت عملگرها، توان مورد نیاز، هزینة تولید و قابلیت اعتماد به تولید و دورة زمانی چرخة عمر آن.

پاسخ این تحلیل ها جهت پژوهش‌ها را به سمت روش‌های بهتر تولید سوییچ، هدایت خواهد كرد. ودر نهایت یافتن این كه چگونه یك روش ویژه در بهترین شكلش مورد استفاده قرار خواهد گرفت و نیز تحلیل و تباین روش‌های مختلف تولید.

3) حركت به سمت طراحی ظرفیت ابزار، جهت استفادة مؤثر از 10¹⁷ ترانزیستور یا سوئیچ است. چنین طراحی‌هائی در مقیاس‌های مطلوب ، حتی بی‌شباهت در مقایسه با افزایش ظرفیت ابزارها خواهد بود.

4) طراحی‌های قویتر و ابزارهای بررسی قوی‌تر به منظور طراحی "مدارهای منطقی" با چندین مرتبة مغناطیسی بزرگتر و پیچیده‌تر.

5) طراحی پروسه‌های انعطاف‌پذیرتر جهت مسیر تولید از مرحلة طراحی منطقی،‌ آزمایش و بررسی، تا بكارگیری در سخت‌افزار.

 پروسه‌ها می‌بایستی به قدری انعطاف‌پذیر باشند كه:

   الف) توسعة اشتراكی درطراحی، آزمایش و ساخت ،به گونه‌ای كه هیچ یك از این گام‌ها تثبیت شده نباشد.

   ب) توسعه طراحی، و بررسی به منظور كاوش یك روش نوین ساخت با هدف تقویت نقاط قوت و كم كردن نقاط ضعف .هر نوع از سیستم نانویی كه توسط طراحان ساخته می‌شود می‌بایستی صحت عملكرد آن تضمین شود.

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

1) بررسی مقیاسی سیستم‌های نانوئی:

مانع بزرگی به نام« بررسی چند میلیون ابزار نانومقیاس»، نیاز به روش‌های انقلابی به منظور بررسی سیستم‌هائی كه ذاتاً بزرگتر، پیچیده‌تر و دارای درجات نامعینی پیچیده‌تری هستند، را روشن می‌كند. در ابتدا مروری كوتاه خواهیم داشت بر ضرورت "آزمایش مدل.

آزمایش مدل از روش‌های پذیرفته شده و رسمی در حوزة بررسی روش‌های ساخت است. این حوزه شامل كاوش فضای طراحی است به منظور دیدن این نكته كه خواص مطلوب در مدل طراحی شده حفظ شده باشد، به گونه ای كه اگر یكی ازاین خواص، مختل شده باشد،‌ یك""Counter Example تولید شود.

 Model Checking Symbolic   بر مبنای ROBDDها یك نمونه از این روش‌ها است.

بهرحال، BDDها به منظور حل مسائل ناشی از خطای حافظه بكار گرفته می‌شوند و برای مدارات بزرگتر با تعداد حالات بزرگتر و متغیرتر مقیاس پذیر نمی‌باشند.

دو روش عمده برای حل این مسأله وجود دارد:

 یك روش حل مبتنی بر محدود كردن آزمایش كنندة مدل به یك مدار unbounded، است كه به نام "unbounded model checking" یا UMC نامیده می‌شود،‌ به گونه‌ای كه خواص آزمایش شده به تعداد دلخواه از Time-Frame" "ها وابستگی ندارد.

روش دیگر مبتنی بر مدل "مدار محدوداستوار است كه به نام BMC نامیده می‌شود در این روش بررسی مدل با تعداد ویژه و محدودی از Time-Frame" "ها صورت می‌گیرد.

ابتدا در مورد فرمولاسیون UMC كه مبتنی بر "رسیدن به سرعت در مراتب مغناطیسی" است و به وسیلة تكنیك‌های مقیاس پذیر"BMC" پیروی می‌شود،‌ بحث می‌كنیم و بالاخره این كه چهارچوبی را برای بررسی و لحاظ كردن درجات نامعینی به سیستم، معرفی می‌كنیم.

2- "UMC" مقیاس‌پذیر:

مزیت"UMC" بر "BMC" در كامل بودن آن است. روش "UMC" می‌تواند خواص مدل را همانگونه كه هست لحاظ كند زیرا این روش مبتنی بر قابلیت آزمایش به كمك نقاط ثابت است. عیب این روش در این است كه""ROBDD كاملاً به مرتبة متغیرها حساس است. ابعاد BDD می‌تواند غیرمنطقی باشد اگر مرتبة متغیرها بد انتخاب شود. در پاره‌ای از موارد (نظیر یك واحد" ضرب") هیچ مرتبة متغیری به منظور رسیدن به یك ROBDD كامل كه نمایشگر عملكرد مدار باشد،‌ وجود ندارد. به علاوه، برای خیلی از شواهد مسأله،‌ حتی اگر ROBDD برای روابط انتقال ساخته شود،‌ حافظه می‌تواند هنوز در خلال عمل كمیت‌گذاری، بتركد. پژوهش‌های اخیر بر بهبود الگوریتم‌های BDD جهت كاهش انفجار حافظه استوار و استفاده از خلاصه نگاری و تكنیك‌های كاهش، جهت كاهش اندازه مدل، تمركز یافته‌اند.

"SAT Solver"ها ضمیمة BDD ها می‌شوند. روابط انتقال یك سیستم در قالب K، Time-Frame"" باز می‌شود. "SAT" هابه ابعاد مسأله كمتر حساسند. اما به هر حال، SATها دارای یك محدودیت هستند و آن این كه خواص یك مدار را با تعداد محدودی (K)، می‌سنجند.

اگر هیچ Countervecample در K، Time-Frame یافت نشد، هیچ تضمینی برای همگرائی حل مسأله وجود ندارد.

BMC"" در مقایسه با UMC"" مبتنی بر"BDD" ،كامل نمی‌باشد. این روش می‌تواند فقط  "Counter Example"ها را بیابد و قادر به محاسبة خواص نمی‌باشد مگر آن كه یك حد بر روی حداكثر اندازة Counter Example"" تعیین شود.

روشی برای تركیب SAT-Solver و BDD به صورت فرمول CNF به كار گرفته شده است.

منبع:http://www.nano.ir