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

The VHDL Development Strategy Based On The Formal Method

高安全高可靠的相似冗容错架构善于容忍各通道独立产生的错误,因此设计正确的拜占庭容错计算机出现的主要故障为共模故障。减少共模故障最经济最有效的阶段是整个设计和开发阶段。基于形式化方法的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.