VHDL Based Symbolic Model Checker with Improved CTL Property Language
محل انتشار: نهمین کنفرانس سالانه انجمن کامپیوتر ایران
سال انتشار: 1382
نوع سند: مقاله کنفرانسی
زبان: انگلیسی
مشاهده: 2,111
فایل این مقاله در 8 صفحه با فرمت PDF قابل دریافت می باشد
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
ACCSI09_007
تاریخ نمایه سازی: 4 بهمن 1386
چکیده مقاله:
Most existing verification tools suffer from having a standard language for design specification. Although most of these tools support standard hardware description languages, but the subset of the HDL they support is very limited. In this paper we introduce a verification tool, which does not have these limitations. We use symbolic model checking to verify a VHDL design. A Data Flow Graph (DFG) is extracted from the VHDL code, which has been fully implemented in object oriented format in C++ and covers about 90% of the synthesizable subset of VHDL. We use
Reduced Ordered Binary D ecision Diagrams to represent FSM description of a system in terms of transition relations. The conversion of DFG to BDDs is done inside the DFG classes. For the property language, we have used CTL with extensions to include event sequence structures and word-level properties. For these extensions, we have implemented a Multi-valued Decision Diagram (MDD) package over an existing BDD package. The complete package is put into a user-friendly environment for automatic verification of FSMs. We have compared our results with VIS and SMV tools.
کلیدواژه ها:
VHDL ، Verification ، Model Checking ، FSM ، BDD ، MDD ، CTL ، Image Computation ، Reachability Analysis ، Coverage
نویسندگان
Hamid Shojai
Electrical and Computer Engineering University of Tehran
Hadi Parandeh Afshar
Electrical and Computer Engineering University of Tehran
Zainalabedin Navabi
Electrical and Computer Engineering University of Tehran
مراجع و منابع این مقاله:
لیست زیر مراجع و منابع استفاده شده در این مقاله را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود مقاله لینک شده اند :