● 摘要
芯片设计的日趋复杂化和高速化，对设计自动化的理论和方法提出了新的要求。半导体工艺水平的发展使得集成电路集成度进一步提高，业界也由超大规模集成电路时代迈入了深亚微米时代，工艺技术日臻成熟，但系统级芯片（System on Chip，SoC）设计面临着严峻的问题：随着芯片功能和性能的需求发展，芯片规模越来越大，工作速度越来越高，开发周期越来越长，设计质量越来越难以控制，设计成本越来越高。如果芯片成本太高，设计周期过长，即使做出产品来也没有市场。本论文研究的是基带芯片SoC设计中的端口控制逻辑部分的IP化自动设计及其形式验证技术。目的是使端口控制设计IP化，缩短设计周期，具有可重用性，同时采用形式化的验证确保了验证功能的完备。 论文首先对端口控制逻辑在基带单芯片系统中的设计意义及设计需求进行了分析，端口控制是任何芯片都要有的控制逻辑，它的实现可以有效减少片外管脚的数量，从而达到缩小芯片面积的功能，这是我们集成电路设计评价的重要指标之一。基于脚本语言自动实现硬件设计是我们提高设计效率的关键。通过对端口控制逻辑的基本功能设计，根据端口控制逻辑的功能特点，提出了采用属性检查的形式验证方法。论文基于OneSpin公司的360MV系统检验平台，对属性检查的形式化验证方法进行了分析和阐述。包括了以下几个方面：①一致性检测，含有了动态软连接和意图检查，研究如何有效地完成数据流图之间的一致性测试。将原始设计表示成有限状态机，将要验证的性质用时态逻辑描述。然后，遍历有限状态机以检验性质是否存在。②属性检查，检查设计说明是否正确实现；检查功能是否正确，如不正确给出反例；③完备性。实现100%功能覆盖。