[發明專利]組合電路瞬態脈沖重匯聚現象可滿足性分析方法及系統

有效

• 申請號: 201810432652.0
• 申請日: 2018-05-08
• 公開（公告）號: CN108763660B
• 公開（公告）日: 2022-05-03
• 發明（設計）人: 郭陽;劉暢;梁斌;張龍;賀旭;張璐捷;陳建軍;劉必慰
• 申請（專利權）人: 中國人民解放軍國防科技大學
• 主分類號: G06F30/398
• 分類號: G06F30/398
• 代理公司: 湖南兆弘專利事務所(普通合伙) 43008
• 代理人: 譚武藝

1.一種組合電路瞬態脈沖重匯聚現象可滿足性分析方法，其特征在于實施步驟包括：

1）讀入被分析組合電路的與非圖格式文件；

2）針對被分析組合電路中隨機選取某一起始節點V，使用深度優先的方法搜索所有可能到達的輸出節點，并任意選擇一個輸出節點P；

3）從輸出節點P出發，使用深度優先的方法逆著電路傳播方向反向搜索到達起始節點V的所有路徑，并將路徑上任意節點到起始節點V間隔的最大節點數量以及最少節點數量分別記錄為該任意節點到輸出節點P的最大距離和最小距離；

4）初始化建立待檢查列表C，所述待檢查列表C中任意元素(V_1,V₂)的元素結構包含從起始節點V出發同時到達的節點V₁和V₂、起始節點V分別到節點V₁和V₂的路徑P₁和P₂、以及路徑P₁和P₂的分別敏化判斷結果和同時敏化判斷結果，敏化判斷結果為滿足SAT或不滿足UNSAT；將元素(V_,V)加入待檢查列表C，其中V為起始節點；

5）對待檢查列表C中每個元素添加敏化約束條件，并將元素中從起始節點V出發同時到達的兩個節點的敏化約束條件利用SAT求解器求解其對應的兩條路徑的分別敏化判斷結果和同時敏化判斷結果；

6）針對待檢查列表C中的任意元素(V_1,V₂)，如果節點V₁和V₂均為輸出節點P、路徑P₁和P₂不相同、且同時敏化判斷結果為滿足SAT，則判定存在滿足要求的輸入向量可以使起始節點V和輸出節點P之間直接有兩條可以同時敏化的路徑，過程結束并退出；否則，跳轉執行下一步；

7）更新待檢查列表C，對待檢查列表C中的元素進行排序；

8）判斷待檢查列表C是否為空，若待檢查列表C不為空，則跳轉執行步驟5），否則，判定不存在滿足要求的輸入向量可以使起始節點V和輸出節點P之間直接有兩條可以同時敏化的路徑，過程結束并退出。