过去几十年来，微电子技术的高速发展和人们对信息技术的强大需求使得现代集成电路系统的规模和复杂程度日趋提高。这必将导致对集成电路系统级的设计、制造提出更高的要求。从目前集成电路的制造技术看，深亚微米制造技术的突破使得在单一硅片上实现信号采集、转换、存储、处理和输入／输出功能的片上系统(Systems-on-Chip，SoC)成为可能。相形之下，系统级的设计就越来越成为重要的因素。提高数字系统的设计层次、减少高层设计对象是当前集成电路设计的一个方向。但是，现有的集成电路设计方法学和设计支撑工具并不支持抽象的高层次的设计。 另一方面，确保系统设计的正确性也是系统级设计的极大的挑战。在主要依靠设计师自身积累的经验的情况下，现有的设计验证技术也无法有效保证系统设计的正确性。1994年Intel公司的Pentium芯片中的浮点除法运算错误是在其大量进入商用后才被一位用户发现的，虽然这种错误发生的概率为几亿分之一。但这个设计错误还是为Intel公司造成4.75亿美圆的经济损失和无形的形象损失。 为了提高数字硬件的设计层次，保证数字系统设计的正确性，采用“形式化方法”(Formal Methods)设计数字硬件或者集成电路系统是一种比较好的途径。所谓形式化方法，就是利用严格的数学方法，从给出系统设计的规范(Specifications)开始并逐步地推导或者验证系统的方法。 本文将试图研究数字系统形式设计所涉及的主要理论、方法和技术；探讨在系统级的层次应用形式设计的可行性，并提出一种新的数字硬件形式化设计方法。 本论文的研究和创新工作主要包括以下内容： (1)对形式设计方法所取得的成果作了详细的回顾，并讨论了形式设计过程中所用到的理论和方法。详细论述了形式规范、程序的精化演算的作用、类型、适用范围。在此基础上，分析了几个用形式方法设计的硬件系统。 (2)提出了以Agent组成的硬件设计的形式计算模型FCMHD(Formal Computational Model for Hardware Design)。这是一个基于两层的形式设计模型。该模型将简化形式设计的过程并有效降低设计过程的复杂性。给出了FCMHD的区间时态逻辑(Interval Temporal Logic，ITL)语义。作者以时段演算(Duration Calculus，DC)为工具对VHDL的子集进行了形式语义分析；通过分析VHDL和Verilog HDL部分语句的形式语义，为硬件描述语言的分析、设计、编译提供了一个严格的理论基础和新的途径。同时也对本文后半部分提出新的硬件描述语言CHDL作好准备。中文摘要 (3)提出了一个新的硬件描述语言一“基本硬件描述语言‘’CHDL(C。re HardwareDescriPtion Language)。该语言的抽象程度要稍高于目前常见的硬件描述语言，但又很容易将其转换为常见的硬件描述语言。并给出了CHDL的形式语义及常用的硬件的语义;提出了把CHDL转换为vHDL或ve川。9 HDL的方法。 (’)论述了FCMHD的精化演算并给出了具体的精化规则;论述了I孔的复合验证。 (5)运用前面讨论的理论和方法，研究了一个比较大的实例。从给出高层设计规范，利用精化公式逐步导出设计问题的代码。