Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory

被引:0
|
作者
Ferres, B. [1 ]
Oulkaid, O. [1 ,2 ,3 ]
Henrio, L. [1 ]
Khosravian, M. G. [3 ]
Moy, M. [1 ]
Radanne, G. [1 ]
Raymond, P. [2 ]
机构
[1] Univ Lyon, CNRS, EnsL, UCBL,Inria,LIP, F-69342 Lyon 07, France
[2] Univ Grenoble Alpes, CNRS, Grenoble, France
[3] Aniah, F-38000 Grenoble, France
关键词
Electrical rule checking; Integrated Circuits; SMT solving;
D O I
10.23919/DATE56975.2023.10137147
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We consider the verification of electrical properties of circuits to identify potential violations of electrical design rules, also called Electrical Rule Checking (ERC). We present a general approach based on Satisfiability Modulo Theory (SMT) to verify that these errors cannot occur in a given circuit. We claim that our approach is scalable and more precise than existing analyses, like voltage propagation. We applied these techniques to a specific type of errors, the missing level shifters. On an industrial case-study, our technique is able to flag 31% of the warnings raised by the voltage propagation analysis as being false alarms.
引用
收藏
页数:2
相关论文
共 50 条
  • [21] Control design of discrete-time unicycle model using satisfiability modulo theory
    Adzkiya, Dieky
    Mufid, Muhammad Syifa'ul
    Saputri, Febrianti Silviana
    Abate, Alessandro
    SYSTEMS SCIENCE & CONTROL ENGINEERING, 2024, 12 (01)
  • [22] Using Symmetries to Lift Satisfiability Checking
    Carbonnelle, Pierre
    Schenner, Gottfried
    Bruynooghe, Maurice
    Bogaerts, Bart
    Denecker, Marc
    THIRTY-EIGHTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 38 NO 8, 2024, : 7961 - 7968
  • [23] QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
    Bonacina, Maria Paola
    Graham-Lengrand, Stephane
    Vauthier, Christophe
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 78 - 95
  • [24] Analysis of SEU Propagation in Combinational Circuits at RTL Based on Satisfiability Modulo Theories
    Kazma, Ghaith
    Hamad, Ghaith Bany
    Mohamed, Otmane Ait
    Savaria, Yvon
    PROCEEDINGS OF THE GREAT LAKES SYMPOSIUM ON VLSI 2017 (GLSVLSI' 17), 2017, : 239 - 244
  • [25] Railway Scheduling Using Boolean Satisfiability Modulo Simulations
    Kolarik, Tomas
    Ratschan, Stefan
    FORMAL METHODS, FM 2023, 2023, 14000 : 56 - 73
  • [26] Routability-Aware Placement for Advanced FinFET Mixed-Signal Circuits using Satisfiability Modulo Theories
    Chen, Hao
    Turner, Walker J.
    Pan, David Z.
    Ren, Haoxing
    PROCEEDINGS OF THE 2022 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE 2022), 2022, : 160 - 165
  • [27] Satisfiability checking using Boolean Expression Diagrams
    Poul F. Williams
    Henrik R. Andersen
    Henrik Hulgaard
    International Journal on Software Tools for Technology Transfer, 2003, 5 (1) : 4 - 14
  • [28] Bounded model checking using satisfiability solving
    Clarke, E
    Biere, A
    Raimi, R
    Zhu, Y
    FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) : 7 - 34
  • [29] Bounded Model Checking Using Satisfiability Solving
    Edmund Clarke
    Armin Biere
    Richard Raimi
    Yunshan Zhu
    Formal Methods in System Design, 2001, 19 : 7 - 34
  • [30] Satisfiability Modulo Graph Theory for Task Mapping and Scheduling on Multiprocessor Systems
    Liu, Weichen
    Gu, Zonghua
    Xu, Jiang
    Wu, Xiaowen
    Ye, Yaoyao
    IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 2011, 22 (08) : 1382 - 1389