وارسی پردازنده ها را میتوان به دو روش انجام داد: روش شبیه سازی و روش رسمی. روش شبیه سازی یک اثبات کلی نیست چراکه فقط به ازای ورودیهای امتحان شده به ما ضمانت درستی طراحی را میدهد. استفاده از روشهای رسمی به دلیل کلیت و اثبات ریاضی صحت عملکرد، در چند سال اخیر بسیار متداول شده است. این روش به شیوه های مختلف اعمال میشود. یکی از متداولترین این شیوهها، روشmodel checking است که دارای حالت خودکاری بیشتری است. در این مقاله، ابتدا روشهای وارسی رسمی پردازنده های ابرعددی را بررسی کرده و سپس روش جدیدی مبتنی بر model checking معرفی نموده، پردازنده DLX با دو خط لوله را با این روش وارسی خواهیم کرد.
