سال انتشار: ۱۳۸۲
محل انتشار: نهمین کنفرانس سالانه انجمن کامپیوتر ایران
تعداد صفحات: ۸
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
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.