随着硬件描述性语言(Hardware Description Language,HDL)的高速发展,Verilog作为一种标准化的硬件描述性语言,被广泛地应用在数字电路和系统的设计上。同时,硬件描述性语言的正确性需求也越来越高,用形式化的验证方法是其主要的验证方式之一。然而,由于现有的定理证明技术不能对硬件描述性语言中一些特殊性质进行验证,比如事件驱动性质和实时性质等。所以对该类型语言进行行形式化验证的工作很少。本文通过对经典Hoare Logic的改进,提出一种实时性的Hoare Logic,并基于这个实时性的Hoare Logic,提出适用于硬件描述性语言的证明推理系统。多线程离散事件模拟语言(Multithreaded Discrete Event Simulation Lan-guage,MDESL)是一种类Verilog的形式化语言。其中包含许多硬件描述性语言的特性,比如事件驱动计算、实时性和基于共享变量的并发性。本文在研究多线程离散事件模拟语言的语义模型的基础上,结合实时性Hoare Logic,首先提出了程序状态行为和顺序程序的规则。然后根据程序的并发模型提出了并行环境中守卫语句规则以及并行程序规则。接着给出了结构性语句规则和辅助规则形成了一个完整的多线程离散事件模拟语言的证明推理系统。利用该证明推理系统可以对多线程离散事件模拟语言中事件驱动计算和实时的性质以及基于离散时间控制的并发行为进行分析与验证。该推理证明系统不仅丰富了多线程离散事件模拟语言的语义模型,还为后续研究多线程离散事件模拟语言的语义连接理论打下了理论基础。此外,为了证明系统的可靠性,本文还对证明推理系统中的推理规则进行逐条验证。最后,通过一个实例来说明如何用本文提出的证明推理系统对并行程序进行正确性验证。