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 条
  • [31] Analog Layout Placement Retargeting using Satisfiability Modulo Theories
    Mohamed, Aya
    Dessouky, Mohamed
    Saif, Sherif M.
    2017 14TH INTERNATIONAL CONFERENCE ON SYNTHESIS, MODELING, ANALYSIS AND SIMULATION METHODS AND APPLICATIONS TO CIRCUIT DESIGN (SMACD), 2017,
  • [32] Solving quantified verification conditions using satisfiability modulo theories
    Ge, Yeting
    Barrett, Clark
    Tinelli, Cesare
    ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2009, 55 (1-2) : 101 - 122
  • [33] Solving quantified verification conditions using satisfiability modulo theories
    Yeting Ge
    Clark Barrett
    Cesare Tinelli
    Annals of Mathematics and Artificial Intelligence, 2009, 55 : 101 - 122
  • [34] Bounded Model Checking of Dense-Timed Deontic Interpreted Systems: A Satisfiability Modulo Theories Approach
    Wozna-Szczesniak, Bozena
    Szczesniak, Ireneusz
    Olszewski, Ireneusz
    APPLIED SCIENCES-BASEL, 2025, 15 (05):
  • [35] Using Satisfiability Modulo Theories for Inductive Verification of Lustre Programs
    Franzen, Anders
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (01) : 19 - 33
  • [36] Using Incomplete Satisfiability Modulo Theories to Determine Robotic Tasks
    Witsch, Andreas
    Skubch, Hendrik
    Niemczyk, Stefan
    Geihs, Kurt
    2013 IEEE/RSJ INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS), 2013, : 4784 - 4789
  • [37] Using Satisfiability Modulo Theories to Analyze Abstract State Machines
    Veanes, Margus
    Saabas, Ando
    ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, 2008, 5238 : 355 - 355
  • [38] Automated Verification of Query Equivalence Using Satisfiability Modulo Theories
    Zhou, Qi
    Arulraj, Joy
    Navathe, Shamkant
    Harris, William
    Xu, Dong
    PROCEEDINGS OF THE VLDB ENDOWMENT, 2019, 12 (11): : 1276 - 1288
  • [39] Solving quantified verification conditions using satisfiability modulo theories
    Ge, Yeting
    Barrett, Clark
    Tinelli, Cesare
    AUTOMATED DEDUCTION - CADE-21, PROCEEDINGS, 2007, 4603 : 167 - +
  • [40] METHOD FOR CHECKING ELECTRICAL CONTINUITY IN REDUNDANT CIRCUITS
    RACHAL, L
    STOFEL, E
    REVIEW OF SCIENTIFIC INSTRUMENTS, 1967, 38 (07): : 986 - &