基于时态逻辑的形式化综合

实现了硬件描述语言VHDL到XYZ/E的翻译，通过实例研究得到了用XYZ系统描述和验证硬件的途径的方法。提出了一条新的从时态逻辑规范开始自动综合途径和将时态逻辑公式自动地转换为非确的自动机的算法和实时自动机状态分析的等法。开发了“基于时态逻 辑的形式化综合系统的原型“。对伯克莱大学的理论和综合系统VIS进行了全面的分析、实验和功能扩展的实际应用。进行了实时模型检验和BDD的研究。利用该系统进行了微处理器PIC的设计验证。利用斯坦福大学的STep系统验证了SDHI2Mb/s异步映射和光同专用芯片部分关键电路，该芯片一次投片成功。