درستي سنجي صوري معماري مديريت توان در سطح سيستم براي پردازنده هاي مدرن

Formal Verification of System-Level Power Management Architecture in Modern Processors

همچنانكه كه بر پيچيدگي طراحي هاي توان پايين افزوده مي شود، ابزار هاي خودكار كارآمدتري به منظور درستي سنجي عملكرد آن ها مورد نياز است. درستي سنجي همزمان عملكرد طراحي ها و سازگاري بخش كنترلي مديريت توان با هدف توان پايين آن ها يكي از چالش هاي بزرگ است. اين مقاله روشي ارايه مي دهد كه اين مشكل را در پردازنده هاي مدرن توان پايين پيچيده كه داراي ده ها حوزه تواني هستند، حل نمايد. براي اطمينان از اين كه عملكرد پردازنده پس از قرار گرفتن بخش كنترل مديريت توان تغيير نمي كند، بررسي برابري كارآمدي بين مدل پياده سازي توان پايين و مدل مشخصه آن انجام مي شود. با اين حال، اين نوع درستي سنجي به دليل رفتار غيرعملكردي استراتژي هاي مديريت توان در سطح سيستم كافي نيست. بنابراين، روش پيشنهادي سازگاري بين PMU و UPF را به وسيله قوانين تواني سطح بالاي استخراج شده از UPF بررسي مي كند. نتايج تجربي نشان مي دهد كه روش پيشنهادي نه تنها به طراحان كمك مي كند تا يك كنترل كننده مديريت توان سطح بالاي صحيح بسازند بلكه همچنين بتوانند ايرادهاي عملكردي توان پايين در طراحي شان را شناسايي كنند.

As the complexity of low-power designs grows, more efficient and automated tools are needed to functionally verify them. Simultaneous verification of both the design functionality and the consistency of power management controllers with the low-level power intent is a big challenge. This paper presents a method which attempts to resolve such a problem for complicated processors with tens of power domains. 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. 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.