电子说
一:形式验证的基本概念
形式验证不仅仅是芯片领域中的一个概念。正如文章开头提到过,形式验证强调使用严格的数学推理和形式化技术,以确保系统的行为是否符合预期的性质和规格。所以说只要是可以通过量化方式构建数学模型的系统,都可以使用形式验证来check其功能性以及其他可量化特性。比如:
这里拿计数器举一个简单的形式验证示例。请注意,这只是一个简化的示例,实际的形式验证可能涉及更复杂的设计和性质。
假设有一个4位的计数器电路,可以从0计数到15。我们想要验证以下性质:当计数器的值达到最大值15时,下一个计数值应该是0。
设计:计数器电路有一个4位的计数器寄存器,可以递增。当计数器值达到15时,下一个时钟周期应该将计数器重置为0。
形式验证属性:我们使用SystemVerilog的属性规约 (SVA) 来表达这个性质。(一般形式验证的case都使用SVA来编写)以下是一个简化的属性规约示例:
property reset_at_max;
@(posedge clk) disable iff (!rst_n)
(count == 4'b1111) |= > (next_count == 4'b0000);
endproperty
assert property (reset_at_max);
在这个属性规约中,我们定义了一个属性 reset_at_max ,它表达了当计数器值为15时,下一个计数值应为0。这个属性在时钟上升沿触发时进行检查。如果属性不满足,将会产生一个验证错误。
在这个示例中,使用仿真进行验证可能需要执行多个时钟周期来验证所有可能的计数序列。但是,使用形式验证可以直接进行数学推理,验证属性在所有可能的情况下是否成立.
除此之外,与基于仿真的验证不同,基于仿真的验证会使用各种输入情景来测试设计以确保其正确行为,形式验证涉及数学分析以验证设计的属性。这些属性可以包括功能正确性、安全性、安全性以及某些类型错误的缺失(例如,竞态条件、死锁等)。
二:形式验证的优势
从上述的例子看来,那么形式验证要优于基于仿真的验证?看似高性能的形式验证,要将它发挥得淋漓尽致也是需要代价的。
其实不然,形式验证也面临着挑战。它可能计算成本高昂,需要专门的专业知识来制定属性并设置验证过程。通常与其他验证技术(如仿真和测试)结合使用,以提供全面的验证策略。形式验证和基于仿真的验证各有其优势和局限性,没有绝对的优劣之分。选择哪种验证方法取决于具体的设计需求、时间和资源限制以及设计的复杂性。
可见,trade-off的概念在芯片领域里面处处可见。鱼与熊掌不可得兼。
三:在芯片验证中实现形式验证
形式验证主要由以下几个部分组成:
在电子设计自动化 (EDA) 工具中,许多主要的形式验证工具已经集成到综合工具链中,以帮助硬件工程师验证他们的设计。这些工具通常基于硬件描述语言 (如Verilog或VHDL) 。
比如:
1. Cadence JasperGold :JasperGold是一个集成式形式验证平台,支持属性规约和模型检查,广泛应用于验证硬件设计。
2. Synopsys VC Formal :VC Formal是Synopsys的形式验证工具,用于验证功能、时序和系统级性质。
最近几年,学术界
全部0条评论
快来发表一下你的评论吧 !