对于集成电路设计工程师来说，把设计要点用命题注释可以提高程序的可读性，但是这会引出在综合过程中如何利用命题，并防止对命题综合从而影响逻辑输出的问题。本文比较了在verilog 或 vhdl语言程序中不同的命题方法进行硬件设计验证的优点和缺点，所提出的白盒验证工具能够降低命题的复杂性。
命题方法在软件设计中已经应用了很长时间，并已成为许多软件研发团队使用的主流方法，然而，在硬件描述语言verilog 或 vhdl中采用命题来进行硬件设计也不过最近才开始普及。虽然vhdl具备固有的命题结构，但是verilog却没有。因此采用verilog语言的设计及验证工程师要采用不同的命题方法。本文对几种不同的命题方法进行了研究，阐述了它们各自的优缺点。
命题的作用
一般来说，命题是描述一个特定的设计应该实现何种功能或不应该实现何种功能的语句。这样的一个描述可以在所有的时间或环境下为真，或者在设计中的特定行为下有条件地部分为真。命题也可称为“设计意图的表述”或“设计工程师的假设”，因为它们对设计的重要特性进行归档。最具有价值的命题不仅仅是文档，它们被动地观察设计并核查设计的行为是否与设计工程师的期望或假设一致。
作为命题的一个简单例程，我们可以观察采用one-hot编码的状态机。在verilog语言中没有任何特殊的编码方案来识别状态寄存器，若一个设计错误导致寄存器违反了one-hot规则，则没有内在的机制来核查及报告这种违规。在这种情况下，采用命题是最适宜的。命题可描述寄存器的行为：它可以是被设计成、打算设计成或者被假设具有one-hot编码的多种行为。这个命题既可是个注释并仅进行纯粹的信息描述，也可以是一个主动的命令,对one-hot规则进行连续地核查。
命题的例程包括：
1、一个verilog实例描述是并行的，两个项目永远不会同时为真；
2、一个状态机不会进行非法行为转换；
3、存储器要从经过初始化的地址读取信息；
4、接口上的两个信号要遵循请求-确认握手协议。
在所有的这些例程中，设计工程师企图匹配命题定义的行为来实现逻辑，但有时设计工程师会出错，而命题在这时则提供了一种交叉核查的方法；当设计工程师设计出来的行为与命题规定的行为不符时，命题就会发出报警。若在verilog仿真时出现违反命题的情况，人们就非常希望能核查并报告这种违反命题的情况。
除了仿真之外，命题也是形式或半形式验证工具要达到的验证目标。这些工具构造基于形式的数学模型，并采用推理技术来证明或反证设计工程师所期望达到的电路行为的特性。
若验证工具发现了一种可以违反电路特性的方法，那么也就发现了电路设计中的某种缺陷。如果验证工具能够证明无法违反电路属性，那么就得到了有价值的验证信息。
形式或半形式验证工具能够证明两个verilog例程项目不能同时评估，或没有办法让状态机进行非法行为转换。工程师非常希望形式验证工具的目标特性与仿真中使用的命题相匹配。这使命题具体化并在利用形式验证方法之前的仿真过程中排除故障。进一步来说，如果仿真测试套件中包含某种违反命题的测试，则表明存在设计缺陷，要在进行形式的分析前改正这种缺陷。
设计中的命题是“白盒”验证的一个极好的实例，因为它们能够将设计所期望的的内部行为具体化而不仅仅定义从设计输入到输出的端到端行为。在许多场合，包括上述几个实例，命题直接映射到内部设计结构，如状态机和存储器。
除了核查表示设计缺陷的问题之外，对电路内部结构的命题提高了整个设计的可观测性和设计行为的能见度。对于一个大型设计的输出，人们不容易核查到深藏在电路设计内部的设计缺陷的作用，并且诊断及改正这种缺陷也非常耗时。最好在缺陷源头或接近源头处核查到缺陷，这些地方往往就是内部设计结构命题所报告的设计违规之处。
