论文部分内容阅读
为保证硬件设计的正确性，提出了对硬件设计组合验证的新方法．该方法在命题投影时序逻辑的统一框架下，实现对硬件系统行为的建模，对所期望性质的形式化描述，并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证，从而证明硬件系统满足期望的性质，保证设计的正确性．进位保留加法器的验证实例说明了该方法的可行性．