基于模型检查的VHDL到FSM的转换  

Modeling from VHDL design to FSM based on model checking

作　　者：苏继强[1] 沈云付[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机工程与设计》2008年第22期5840-5842,5846,共4页Computer Engineering and Design

摘　　要：随着计算机软硬件系统规模的日益复杂,如何保证系统的正确和可靠,逐渐成为当前理论界和产业界共同关心的重要问题。为此提出的诸多理论和方法中,模型检查以其简洁明了和自动化程度高而引人注目。提出了一个针对时序电路VHDL设计的模型检查的解决方案。讨论了该方案的系统结构,将VHDL设计转化为有限状态机模型的算法,以及针对同步时序电路设计的模型化简,可有效减少FSM的状态空间,继而可以采用符号模型检查算法对需要检查的性质进行验证。As our computer software and hardware systems have become increasingly complex, how to ensure the correctness and reliability of such systems has become a vital problem in both theoretical and industrial circles. Among the related theories and methods, model checking has come to front because of its conciseness and high degree of automation. A solution to model checking based on VHDL design is given. The system architecture of the solution is described including modeling algorithm which translates VHDL design into FSM and simplifying FSM of synchronous VHDL design. Thus it is used by symbolic model checking algorithm to model checking VHDL design.

关 键 词：模型检查 形式验证 有限状态机 硬件描述语言 同步时序电路 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]