四川省市场经济诚信建设促进会-

成都奥卡思微电科科技有限公司

成都奥卡思微电科技有限公司于2018年4月成立于成都高新区，注册资本1200万元，是目前国内唯一推出商业化验证EDA软件的公司。目前拥有2项发明专利，12项软件著作权，另8项专利正在申请中，于2020年申请成为四川省高新技术企业。
其核心研发人员均有Cadence，Synopsys，Xilinx等国际知名EDA公司和芯片设计公司的从业经历，具有平均超过15年的全球EDA行业经验，是多项业内知名软件工具的主要研发者。
成都奥卡思微电科技有限公司致力于开发国际领先、自主可控的具有完全自主知识产权的电子设计自动化产品平台产品（EDA），具有独特产品优势。该公司现已研发并投入使用的产品有AVEMC芯片形式化验证产品AVECEC芯片逻辑等价性验证产品，其中AVEMC软件在覆盖率、空泛性等技术方面全球独一无二。并于2020年4月20日正式发布国内首款基于亚马逊AWS云平台的形式化验证工具AveMC Cloud，标志着该公司EDA工具正式迈入云计算时代，用户可以远程完成复杂芯片RTL设计的验证及调试工作，也为该公司EDA软件走向国际市场打下了坚实的基础。
在与其他同类业内产品对比的情况下，该公司具有明显的优势。项目产品的功能和性能竞争性远超于目前业内最先进的产品，该公司产品可用图形化的方式，帮助用户快速建立属性和约束模型，数据表明这一块占了形式验证时间的三分之一，其更为精确的模型和计算速度，能发现其他工具忽略的属性完备性检查漏洞，因其开放的构架，用户可以根据具体的设计和验证场景构建自己的工具。
关于形式化验证：
形式化方法的定义
Specification（规范）：具有形式语义的符号(symbol)和逻辑明确地表述所要设计的系统要求
Verification（验证）：利用符号和逻辑运算从数学上证明一个逻辑系统（比如芯片）满足设计规范
形式化方法的起源
60年代末出现 “软件危机”（软件可靠性没有保障，无法控制软件开发）使得形式化方法利用数学方法证明程序的正确性
软件和硬件领域的广泛应用
软硬件系统的formal市场估计在100亿元以上
传统上软件方面的形式化方法应用在软件规范的形式化描述，即严格地表达用户需求，形成明确的、一致的、可运行的系统规范
硬件的形式化方法集中在硬件设计验证方面，硬件语法相对软件简单
软件形式化验证正在兴起
形式化方法在安全方面的应用，芯片/软件信息安全，汽车功能安全，智能合约等。
公司使命：
该公司专注于研发芯片数字前端验证EDA，志在打破国外在芯片EDA领域的垄断地位，为中国自主创”芯”事业添砖加瓦。