VHDL Based Symbolic Model Checker with Improved CTL Property Language
- سال انتشار: 1382
- محل انتشار: نهمین کنفرانس سالانه انجمن کامپیوتر ایران
- کد COI اختصاصی: ACCSI09_007
- زبان مقاله: انگلیسی
- تعداد مشاهده: 2112
نویسندگان
Electrical and Computer Engineering University of Tehran
Electrical and Computer Engineering University of Tehran
Electrical and Computer Engineering University of Tehran
چکیده
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مقالات مرتبط جدید
- تاثیر نوروفیدبک بر آموزش کودکان مبتلا به ADHD و اختلالات خواندن: یک بررسی سیستماتیک
- بررسی نقش سیستم های پیشرانش جت و بهبود کارایی انتقال حرارت در انجین های فضاپیما
- مروری بر کاربرد داده کاوی در کشف دانش پنهان
- تجزیه و تحلیل ترمودینامیکی استفاده از یک چرخه دی اکسید کربن فوق بحرانی با اینترکولر، گرم کردن مجدد و احیاکننده برای بازیابی گرمای اتلافی یک توربین گازی
- کاربرد IOT در مهندس پزشکی
اطلاعات بیشتر در مورد COI
COI مخفف عبارت CIVILICA Object Identifier به معنی شناسه سیویلیکا برای اسناد است. COI کدی است که مطابق محل انتشار، به مقالات کنفرانسها و ژورنالهای داخل کشور به هنگام نمایه سازی بر روی پایگاه استنادی سیویلیکا اختصاص می یابد.
کد COI به مفهوم کد ملی اسناد نمایه شده در سیویلیکا است و کدی یکتا و ثابت است و به همین دلیل همواره قابلیت استناد و پیگیری دارد.