一、简介

      Scavel HDL工具(简称)，是系统可信性自动验证国家地方联合工程实验室在系统可信性验证相关理论与技术方面积累大量原创性研究成果的基础上，开发的以形式化和自动推理为核心技术的自主可控工具。

二、功能

      (1)形式化验证VerilogHDL、VHDL等FPGA语言程序;

      (2)验证数组越界、数据溢出、除数为零、非数字等问题;

三、特点

      在不修改、不运行源程序的情况下，以静态方式验证程序运行时错误(Run-Time Errors)，不需要搭建测试环境、运行源码和构建测试例，保证遍历所有可能执行路径以证明源代码的正确性。