12月24日下午，由中國計(jì)算機(jī)學(xué)會（CCF）主辦，上海工業(yè)控制安全創(chuàng)新科技有限公司、華東師范大學(xué)共同承辦的“2021CCF中國軟件大會電子設(shè)計(jì)自動化軟件驗(yàn)證論壇”成功舉辦。本次論壇由于疫情影響以線上直播方式進(jìn)行，邀請來自學(xué)術(shù)界和的工業(yè)界的多位頂尖專家，聚焦國內(nèi)芯片驗(yàn)證軟件最新行業(yè)進(jìn)展和理論前沿，深度解析我國EDA軟件形式化驗(yàn)證領(lǐng)域現(xiàn)狀，共話我國EDA軟件未來發(fā)展前景。論壇受到學(xué)術(shù)界及業(yè)界師生和從業(yè)者的熱烈響應(yīng)，騰訊會議室實(shí)時在線人數(shù)超過120人，論壇視頻在線直播和B站在線直播累積觀看人數(shù)超過4200人。

論壇首先由上海工業(yè)控制安全創(chuàng)新科技有限公司總經(jīng)理、華東師范大學(xué)教授蒲戈光作開場致辭，簡要介紹了本次論壇的背景。他對我國EDA軟件的發(fā)展前景給予肯定，表示雖然當(dāng)前工業(yè)軟件面臨巨大技術(shù)挑戰(zhàn)，但隨著電子信息產(chǎn)業(yè)深度發(fā)展，以EDA軟件為主的國產(chǎn)工業(yè)軟件迎來了新的發(fā)展增長契機(jī)，企業(yè)愈發(fā)重視自主可控技術(shù)研發(fā)。

隨后，由5位來自學(xué)術(shù)界和業(yè)界的專家學(xué)者帶來報(bào)告分享。

• 奧卡思微電科技聯(lián)合創(chuàng)始人與首席執(zhí)行官 袁軍

報(bào)告主題：芯片形式驗(yàn)證技術(shù)及應(yīng)用

主要介紹芯片形式化驗(yàn)證方法，不同驗(yàn)證工具的技術(shù)特點(diǎn)及應(yīng)用場景

• 華為海思半導(dǎo)體項(xiàng)目群總監(jiān) 李選林

報(bào)告主題：硬件形式驗(yàn)證應(yīng)用

結(jié)合當(dāng)前集成電路形式化證明應(yīng)用現(xiàn)狀及面臨的挑戰(zhàn)，分享高階邏輯系統(tǒng)及其在硬件驗(yàn)證中的應(yīng)用實(shí)例

• 芯華章科技股份有限公司高級研發(fā)經(jīng)理 劉軍

報(bào)告主題：形式化工具在EDA領(lǐng)域最新發(fā)展方向研究

基于工具發(fā)展歷程、產(chǎn)業(yè)機(jī)遇與挑戰(zhàn)等方面，系統(tǒng)梳理形式化工具在EDA領(lǐng)域最新發(fā)展方向研究

• 中國科學(xué)院軟件研究所研究員、博導(dǎo) 蔡少偉

報(bào)告主題：約束求解的一些進(jìn)展

交流SAT問題、在EDA中的典型應(yīng)用及常見的SAT算法，提出當(dāng)前約束求解研究進(jìn)展

• 華東師范大學(xué)研究員、博導(dǎo) 李建文

報(bào)告主題：互補(bǔ)近似可達(dá)驗(yàn)證技術(shù)及其應(yīng)用

從應(yīng)用場景包括芯片、航天、軌道交通等安全攸關(guān)領(lǐng)域研究方向，分享用于保障計(jì)算機(jī)軟硬件系統(tǒng)的正確性和安全性的相關(guān)應(yīng)用

至此，2021CCF電子設(shè)計(jì)自動化軟件驗(yàn)證論壇落下帷幕。未來，上海控安也將繼續(xù)深化拓展學(xué)術(shù)研究成果與產(chǎn)業(yè)實(shí)踐需求交叉，加強(qiáng)學(xué)術(shù)界與工業(yè)界合作，促進(jìn)國產(chǎn)EDA驗(yàn)證軟件理論研究、工具成果和行業(yè)實(shí)踐應(yīng)用的融合發(fā)展。