مشخصات پژوهش

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