基于形式化方法的VHDL开发策略  

The VHDL Development Strategy Based On The Formal Method

作　　者：白晨 安书董 李明[1] Bai Chen;An Shudong;Li Ming(Xi'an Aeronautics Computing Technique Research Institute,AVIC,Xi'an 710068,China)

机构地区：[1]航空工业西安航空计算技术研究所,陕西西安710068

出　　处：《长江信息通信》2021年第7期66-68,71,共4页Changjiang Information & Communications

摘　　要：高安全高可靠的相似冗容错架构善于容忍各通道独立产生的错误,因此设计正确的拜占庭容错计算机出现的主要故障为共模故障。减少共模故障最经济最有效的阶段是整个设计和开发阶段。基于形式化方法的VHDL开发策略将基于常规VHDL的自伤而下的数字设计和综合方法与形式规范和验证相结合。此策略是将形式化方法的强大技术过渡到通用数字工程领域的最佳方法。将验证体系结构关键元素和进行VHDL仿真相结合,可有效避免共模故障。The high-safety and high-reliability similar redundant fault-tolerant architecture is good at tolerating errors generated by each channel independently. Therefore, the main fault of a correctly designed Byzantine fault-tolerant computer is a common-mode fault(CMF). The most economical and effective stage to reduce CMF is the entire design and development stage. The VHDL development strategy based on the formal method combines the self-harming digital design and synthesis method based on the conventional VHDL with the formal specification and verification. This strategy is the best way to transition the powerful techniques of formal methods to the field of general digital engineering. Combining key elements of the verification architecture with VHDL simulation can effectively avoid CMF.

关 键 词：相似冗余容错 共模故障 形式化方法 VHDL 

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