微架构设计和形式化证明

概述

• 在软件的形式化中，软件的设计建立在范畴之上。在这里，微架构的设计建立在直接证明的基础之上
• 我们使用模块化
  • （规范）确定模块的规范
  • （实现）计算模块的成本、时钟周期
  • （验证）证明模块的实现满足规范
  • （层次结构）小的模块组合为大的模块，从而整个微架构满足规范
    • 微架构可以实现ISA
    • 中断可以提供服务
    • 浮点单元满足IEEE 745标准
• 更多的说明
  • 我们使用手动证明、手动构建数字电路。不过，它们也可以自动化
    • 在软件的形式化中，证明可以使用自动定理证明（Automated Theorem Proving，ATP）
    • 在Verilog和数字电路中，构建数字电路可以使用电子设计自动化（Electronic Design Automation，EDA）
  • 我们主要考虑数字电路的功能。对于数字电路的时序，我们可以使用时序逻辑（Temporal Logic），它通常用于分布式计算