Verilog HDL的ITL形式语义及其应用

摘要

硬件描述语言为硬件设计师提供一个非常好的分析和设计数字硬件的工具,也为沟通软件和硬件提供了一种方法。然而它缺乏对于电路逻辑关系描述和分析的形式化方法,尤其是基于时序的逻辑描述。这对于化简和检验正确性都带来麻烦。ITL语言描述则提供另一套基于时序的形式化解决方法。用ITL能够方便准确地描述基于时序的数字电路,却缺乏可执行能力,运算公式不能直接进行计算机仿真和验证。Tempura则是ITL强有力的可编程可执行的工具集,大大增强ITL的实用性。通过对RS触发器的描述与验证说明这三者之间的联系,展现ITL等形式方法的发展前景。