Formal Equivalecne Checking
Formal equivalence checking process is a part of electronic design automation (EDA), commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior. [Wiki]
Research
- Equivalence Chekcing
- 1. What is the Equivalence Checkig? [ppt]
- 2. Combination Equivalenc Checking [ppt]
- 3. Sequential Equivalence Checking [ppt]
- BDD
- 1. What is the BDD (Binary Decision Diagram?) [ppt]
- 2. What is the ROBDD (Reduced Ordered Binary Decision Diagram?) [ppt]
- 3. What is the SBDD (Shared Ordered Binary Decision Diagram?) [ppt]
- Thecniques
- 1. Finite State Transition Traversal [ppt]
- 2. Flip-Flop Matching [ppt]
- 3. Basic BDD Manuplation Techniques [ppt]
- Problem
- 1. Variable Ordering Problem [ppt]
- 2. Memory Explosion [ppt]
- 3. Arithmatic Expression [ppt]
- 4. Indentifying a Logic Cone [ppt]
Tools
- FECT 0.9 - Formal Equivalence Checking Tool 0.9
- A BDD-based equivalence checking technique for FBD programs.
- It reads two FBD programs written in 'PLCopen' format directly, and can prove their behavioral equivalence mathematically.
- Latest Release: FECT 0.9 [...] (2016.07.24)
- Prerequisites: To Execute FBDtoVerilog 1.00, Java Version 7 or above is Required.
- CVEC 0.9 - A Customized VIS-based Equivalence Checker
- A Customized VIS-based Equivalence Checker for FPGA Logic Synthesis
- It can contribute to the correctness demonstration of the combination - the 'Synopsys Synplify Pro' synthesizer in the 'Actel Libero IDE' EDA.
- Latest Release: CEVC 0.9[...] (2016.07.24)
Reference papers
- Eui-Sub Kim and Junbeom Yoo, "A New Equivalence Checker for Demonstrating Correctness of Synthesis and Generation of Safety-Critical Software," The 11th IEMEK Symposium on Embedded Technology (ISET 2016), May 26-27, Deajeon, Korea, 2016. (paper, ppt)
- 김의섭, 정세진, 김재엽, 유준범, 장천현, "Verilog4VIS-EC: VIS의 동치성 검사를 위한 Verilog의 정제된 포맷", 한국정보과학회 2015 한국컴퓨터종합학술대회, pp.573-575, 제주대, 06.24-06.26, 2015. (paper, ppt)
- Eui-Sub Kim, Junbeom Yoo, Jong-Gyun Choi, Jang-Yeol Kim, Jang-Soo Lee, "A Correctness Verification Technique for Commercial FPGA Synthesis Tools", Transactions of the Korean Nuclear Society Autumn Meeting, pp 1986-1988, Pyeongchang, Korea, 10.30-10.31, 2014. (paper, ppt)
