fa درستی‌سنجی صوری معماری مدیریت توان در سطح سیستم برای پردازنده های مدرن الکترونیک Electronic پژوهشي Research همچنانکه که بر پیچیدگی طراحی‌های توان پایین افزوده می‌شود، ابزار‌های خودکارِ کارآمدتری به منظور درستی‌سنجی عملکرد آن‌ها مورد نیاز است. درستی‌سنجی همزمان عملکرد طراحی‌ها و سازگاری بخش کنترلی مدیریت توان با هدف توان پایین‌ آن‌ها یکی از چالش‌های بزرگ است. این مقاله روشی ارائه می‌دهد که این مشکل را در پردازنده‌های مدرن توان پایین پیچیده که دارای ده‌ها حوزه توانی هستند، حل نماید. برای اطمینان از این که عملکرد پردازنده پس از قرار گرفتن بخش کنترل مدیریت توان تغییر نمی‌کند، بررسی برابری کارآمدی بین مدل پیاده&shy;سازی توان پایین و مدل مشخصه آن انجام می‌شود. با این حال، این نوع درستی‌سنجی به دلیل رفتار غیرعملکردی استراتژی‌های مدیریت توان در سطح سیستم کافی نیست. بنابراین، روش پیشنهادی سازگاری بین <span dir="LTR">PMU</span> و <span dir="LTR">UPF</span> را به وسیله قوانین توانی سطح بالای استخراج شده از <span dir="LTR">UPF</span> بررسی می‌کند. نتایج تجربی نشان می‌دهد که روش پیشنهادی نه تنها به طراحان کمک می‌کند تا یک کنترل&shy;کننده مدیریت توان سطح بالای صحیح بسازند بلکه همچنین بتوانند ایرادهای عملکردی توان پایین در طراحی‌شان را شناسایی کنند. As the complexity of low-power designs grows, more efficient and automated tools are needed to functionally verify them<a name="OLE_LINK5">. </a><a name="OLE_LINK74">Simultaneous verification of both the design functionality and the consistency of power management controllers with the low-level power intent</a> is a big challenge. This paper presents a method which attempts to resolve such a problem for complicated processors with tens of power domains. <a name="OLE_LINK21">In order to ensure that the functionality of the processor after inserting power management controllers does not change, an efficient equivalence checking is performed between the low-power implementation model and its specification model. However, this kind of verification is not sufficient due to non-functional behavior of system-level power management strategies. Therefore, the proposed method checks the consistency between PMU and UPF by high-level power rules which are extracted from UPF. </a>The experimental results show that the proposed method helps the designers not only to create a correct high-level power management controller but also to identify the low-power functional bugs in their designs. درستی‌سنجی صوری, معماری مدیریت توان, سطح سیستم, پردازنده توان پایین Formal verification, Power management architecture, System-level, low-power processor 185 196 http://jiaeee.com/browse.php?a_code=A-10-1236-1&slc_lang=fa&sid=1 Reza Sharafinejad سید رضا شرفی نژاد r.sharafi@ut.ac.ir 10031947532846008551 10031947532846008551 No College of Engineering, Universtiy of Tehran, Tehran, Iran پردیس دانشکده‌های فنی دانشگاه تهران - دانشکده مهندسی برق و کامپیوتر Bijan Alizadeh بیژن علیزاده b.alizadeh@ut.ac.ir 10031947532846008552 10031947532846008552 Yes College of Engineering, Universtiy of Tehran, Tehran, Iran پردیس دانشکده‌های فنی دانشگاه تهران - دانشکده مهندسی برق و کامپیوتر