形式化验证漫谈:仿真之外,验证之内
“在未来五年内仿真将逐渐被淘汰,仅用于子系统和系统级验证。与此同时,形式化验证方法已经开始处理一些系统级任务。随着技术发展,更多Formal相关的商业标准化会推出。”Intel fellow M. V. Achutha Kiran Kumar
随着Formal技术的发展,业内已经有不少公司有专门的形式化验证团队,也培养了一批热爱Formal,愿意来钻研这门技术的EDA人。
仿真方法学是动态验证的一种,是一个“你想到哪里才能验到哪里”的验证方式,本质上在不断做加法。你需要先让自己尽可能多地想到各种场景、耗费大量时间搭建测试环境,再试图“碰出BUG”,但是这种方式更擅长发现设计“这里有BUG”,但却很难回答“那里没有BUG”的问题。
这方面形式化验证工具有很大的优势。
形式化验证则被称为静态验证,是一种基于严格的数学与算法的验证方法学。用户利用SVA断言描述清楚需要证明的设计规格,通过编译RTL和基于SVA的断言语言,建立Formal模型,然后不断做减法,发现不符合模型的“反例”。
显而易见的一个优势是,形式化验证工具能够通过建立数学模型,实现更敏捷的反向验证,以类似数学定理证明的方式,通过对所有可能的激励空间进行遍历,保证逻辑没有死角,实现验证的完备化、自动化。
传统的仿真工具,在进入具体发现bug阶段前,往往需要很长时间为UVM搭建一个完备的验证平台(testbench);而在调试(Debug)阶段,当出现UVM error,需要问题定位时,仿真工具一般需要从UVM繁杂的log到rtl再到waveform、信号级别,这也是一个很长的回溯曲线。形式化验证在这两个方面,则可以节省很多时间,尤其是通过直接提供反例波形,可以精准直指相关信号进行问题定位。
早期大家可能会担心,觉得Formal工具是不是有使用门槛,这种担心来源于形式化验证工具使用过程中,需要基于对设计的全面理解,才能正确构建验证模型的断言和约束。
一方面,形式化验证对验证工程师而言,确实能够大大的减轻焦虑,芯华章2021年推出GalaxFV,并且在项目的打磨中,持续不断地在丰富应用级断言库,并对其参数化、提高可配置性,让GalaxFV更加容易使用。
另外,随着设计规模增加,工具更加的自动化、智能化,理解设计会成为工程师的一大优势!用好Formal工具,项目将不再需要靠堆人、堆license、堆时间来提高验证质量。
*此内容为集微网原创,著作权归集微网所有,爱集微,爱原创
【集微发布】企业并购意愿降至历史低点,中国芯上市公司H1并购项目大幅下滑
热门评论