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