第31届集成电路设计业展览会（ICCAD-Expo2025）于11月20日至21日在中国·成都西博城举办。作为国内最早商用的形式验证EDA软件供应商、国内EDA领军企业华大九天战略持股企业，上海阿卡思微电子技术有限公司（以下称“阿卡思微”）携多款高性能验证工具及主旨报告邀您共襄盛会。

从2018年成都初创到如今布局全国，从硅谷专家团队归国创业到斩获头部客户与资本青睐，阿卡思微正以稳扎稳打的步伐，成为国产EDA赛道的核心力量。

核心产品矩阵：打破垄断，定义验证新标准

本次参展，阿卡思微集中展示了三大核心产品及专属APP工具，以数学验证的严密性破解芯片设计验证痛点，其性能已实现与国际三大家同台竞技，部分场景更完成超越。

Formal MC：功能验证的“智能证明者”

作为传统RTL仿真验证的有效补充工具，Formal MC凭借数学证明与推理技术，无需用户生成测试激励，即可完成属性验证的严格证明，仿真验证之后采用形式化验证仍然发现问题，形式化验证之后采用仿真不会发现问题，解决了仿真验证在完备性方面的难题。

更具备三大差异化优势：图形化属性建模工具将验证准备时间大幅缩短；更精准的计算模型可捕捉同类工具遗漏的漏洞；搭配云计算模式实现弹性算力配置，适配从模块级到系统级的全阶段验证需求，尤其在设计早期即可发现错误，大幅减少迭代成本。

Formal EC：全流程等价性的“安全卫士”

针对芯片设计中高达半数的功能错误导致的re-spin问题，Formal EC采用穷尽式数学验证方法，无需测试向量即可确保设计实现与黄金设计完全一致。其处理速度远超模拟验证，支持复杂datapath优化、先进时钟门控设计及FPGA全流程验证，更具备强大的debug能力与可扩展性，可轻松应对大型SOC设计的等价性检查需求，成为芯片流片前的关键保障。

Formal HiLEC：AI时代的解题利器

采用模型检验与逻辑等价检查混合技术，利用C/C++黄金模型对数据流路径、浮点算术单元的RTL设计进行等价验证，验证RTL设计实现符合C/C++参考算法。该软件适用于AI/ML、数字信号处理、图像处理芯片设计。

专属验证APP：属性质量的“精准检测仪”

同步展出的属性空泛性检查APP与属性覆盖率精确检查APP，是阿卡思微独创的验证效率工具。前者可识别无效断言，避免验证资源浪费；后者实现属性覆盖率的精准核算，确保验证完备性，两款工具共同构筑起形式化验证的“双重保险”。

技术底气：先发优势与本土化创新双轮驱动

阿卡思微的核心竞争力，源于团队三十年深耕形式化验证的技术积淀与前瞻性布局。创始人作为硅谷归来的行业专家，带领团队在国内EDA产业尚处萌芽阶段时，便聚焦数字前端验证工具研发，成为该领域国内领先的商业化企业。如今，公司产品已服务于国内头部通讯、高性能计算及AI芯片企业，客户数量从最初的十几个增长至数十个，覆盖国内主流芯片设计公司。

阿卡思微技术总监冯煌

公司技术总监冯煌认为，相较于国际三大家，阿卡思微以“快速响应+生态兼容”构建差异化优势。针对客户痛点需求，最快可实现月度级功能迭代，而国际巨头往往需要半年周期；打破封闭工具链壁垒，无论客户采用何种综合工具，均可无缝对接阿卡思微的验证产品，成为行业内公平公正的第三方验证选择。这种聚焦客户需求+技术快速迭代的模式，让公司在部分点工具性能上实现对国际巨头的超越，更赢得了市场与客户的认可。

生态共建：从单点突破到产业协同

作为华大九天生态战略合作伙伴，阿卡思微借助生态赋能实现客户质量与业务规模的双重增长。本次独立参展，既是对成都本土市场的深情回馈，更是向行业展示国产EDA企业协同发展的决心——当前国产EDA工具虽呈“小而散”格局，但阿卡思微坚信，通过工具间的兼容互通与生态整合，终将形成合力。目前，公司已与国内多家厂商开启合作探索，以开放姿态推动国产EDA产业链的协同升级。

面对“AI大模型赋能EDA”的行业趋势，冯煌也表示，阿卡思微保持理性布局。既认可AI当前仍处于萌芽阶段，更多起到效率提升的“锦上添花”作用；也积极投入技术探索，聚焦形式化验证的核心痛点——将AI应用于求解器性能优化、验证意图转换、算法选择等场景，通过技术积累抢占未来先机。

未来展望：稳扎稳打，剑指国际一流

发展规划方面，阿卡思微始终坚守“成为国内领先的形式化技术开发与服务商”的目标，下一步将持续聚焦形式化验证赛道，补齐工具成熟度与易用性短板，同时基于国内客户需求打造国际巨头未覆盖的创新功能。公司将继续以头部客户为核心，通过复杂场景打磨产品，逐步拓展中小客户市场，最终实现对国际三大家的全面追赶与超越。

在成都这片创业初心之地，阿卡思微竭诚交流形式化验证技术应用、探讨EDA生态共建路径，公司将以技术为基、以生态为翼，愿成为这场征程中的坚定践行者与推动者！