AveMC

应用于芯片设计的功能特性验证，正在越来越多的应用场景取代仿真验证。其使用方法是用户根据设计要求提供验证所需的属性和约束，用数学归纳和推理的方法回答这些属性是否正确。如果不正确会自动生成可用于仿真的激励链，以便于查错。形式验证的数学严密性使它成为对安全可靠性要求极高的芯片设计的必备选择。