소프트웨어모델링및분석 (Equivalence Checking 소개 ) 김의섭 Dependable Software Laboratory KONKUK University 2016.06.03
Equivalence Checking 이란? Equivalence Checking: 두프로그램이동일한기능을하는지정형적으로검증하는방법 왜 Equivalence Checking 이필요한가? Software 개발중에다양한 design 변경 / 변환이이루어진다. 변경 / 변환으로인해새로운 Error 나 Bug 가생성되지않았다는것을증명할필요가있음 Modern Software 규모와복잡도高 다양한산업에서사용 다양한 Error 또는 Bug 의생성을수반이를찾아내는것이점점어려워짐 가정용 SW 부터 Safety Critical System 의 SW 까지 Ex) 원자력발전소, 철도제어시스템, 항공운항시스템등 Error 및 Bug 의영향이재난수준의결과를초래 2
왜 Equivalence Checking 이필요한가? SW Development Lifecycle 에는다양한변환이존재 Requirement Modeling Design (Model) C/JAVA Code Transformation (Implementation) C/JAVA Complier 기존프로그램과기능이동일한프로그램으로변환을잘하였는가? 새로운 Bug 나 Error 를생성하지않았는가? Compiler : high technology 다양한 optimization 수행 ex) * 연산 << 연산 이를어떻게증명할것인가? Object Program (Software) 3
왜 Equivalence Checking 이필요한가? SW Design 은다양한이유로인해개발중에변경이생김 Computation Speed, Security, 제한적인 Memory Resource 우리가의도한대로동작할것인가? 빠른길찾기프로그램 Library 를믿고사용해도되는가? 우리가원하는기능대로동작할것인가? 너비우선알고리즘 A* 알고리즘구현 A* 알고리즘 Library 사용 A* 구현 A* Lib 4
Equivalence Checking 따라서 Equivalence Checking 이필요 두프로그램이동일한기능을하는지정형적으로검증 Design을 Boolean Reprobation으로표현후두프로그램의 Equivalence를검증 Formal Verification Technique 의일종 Simulation 이나 Testing은모든가능한경우를확인할수없음 Formal Verification은모든가능한경우를전수검사할수있음 Test Vector가필요하지않음 5
Informal Verification Simulation based Verification 가장많이사용되는방법 Simulation은느리다 모든경우의수를확인하는것은불가능 따라서충분한 Coverage 또는 Corner Case 를커버하는 Test bench 의작성이중요 회로의기능을정확하게검증할수있는의미있는시뮬레이션입력벡터의생성이중요 특정기능이나특성을목표로하는입력벡터들은설계자가알고있는입력공간의영역으로편향되기때문에설계자가알지못하는영역에서버그들이종종발생하게됨 모든경우의수를확인하는것은불가능 (2^input bits) Co-NPHard Test Vector 프로그램 1 Simulation output Equivalent 비교 프로그램 2 Re-Simulation output Counter example 6
Finding Bugs by Simulation 출처 : https://www.google.co.kr/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&ved=0ahukewi8hikmv4rnahxfkzqkhsrtddqqfgghmaa&url= https%3a%2f%2fceit.aut.ac.ir%2f~szamani%2findex_files%2fvhdl_slides%2f15_2_formal%2520verification.ppt&usg= AFQjCNEzzO-nfBtdy0lEhicCpUQR3HdFlw&sig2=PUbsfS1JP76X5O8QVKQCJw&cad=rja 7
Formal Verification Equivalence Checking Hardware Verification (IC 개발 ) 에서많이사용됨 효율적인검증 - 테스트벤치를생성할필요가없다. 효과적인검증 - 시뮬레이션에비해속도가빠르다. 정형검증 가능한모든입력에대해확인이가능하다. 시뮬레이션기반방법론을사용하는것은불가능하다. 특히, ECO (Engineering change orders) 경우에사용하면효율적 ECO 개발자게의해기능은동일하지만보다효율적인설계등의목적으로 HDL 또는 Netlist 를수동으로변경하는것 이럴경우원래의기능이변경되었는지확인해볼필요가있는데, ECO의경우내부적인 Structural 변경이크지않기때문에 EC 를사용하기적절. FBD 1 Intermediate format ROBDD Equivalent EC engine FBD 2 Intermediate format ROBDD Counter example 8
EC 개념 두프로그램이동일한 input 에대해동일한 output 을출력하면동일 Output 들을 XOR 하여 0 이면 Equivalent (miter) i M1 o i M1 o i M2 o M2 9
EC 분류 CEC (Combinational Equivalence Checking) BDD 이용 SEC (Sequential Equivalence Checking) FSM 이용 10
Problem Verification Time Input Size 에따라 Verification time 이 Exponential 하게증가 State Explosion Input Size 에따라 memory usage 가 Exponential 하게증가 time time Input size 출처 : https://socratic.org/questions/how-do-logistic-and-exponential-growth-differ-1 Input size 11
진행중인연구
연구개요 목표 : 1. New Equivalence Checker 개발 2. 개발한 EC 도구의성능개선 Contribution: Hardware Verification 변환기 ( 상용합성도구 ) 의 correctness 증명 Design flow 13
연구동기 Platform Change from PLC to FPGA Target: RPS (Reactor Protection System) Safety critical component of I&C in the Nuclear power plants Recently, FPGA has received much attention from nuclear industry Increasing maintenance cost CCF(Common Cause Fault) problem In-depth strategy for security 14
FPGA? FPGA (Field-Programmable Gate Array) 프로그래머블논리요소와프로그래밍가능내부선이포함된반도체소자 Filed( 사용자 ) 에서프로그래밍이가능한 gate array( 디지털회로반도체 ) 개발에 Synthesis 도구가사용됨 ALTERA 15
Synthesis? RTL 레벨의 HDL 로작성된 Code를 Gate-Level의 optimization 된 Netlist로변환 원래는사용자가직접 Netlist를작성해야하지만제품의사이즈와복잡도가증가로인해직접작성이불가능해짐 사용자는사용자친화적언어인 HDL로제품을설계하면 Synthesis 도구가이를지동으로 Netlist 형태로변환해줌 사용자가고려해야하는복잡한과정 (Optimization) 을대신해서수행 칩의 speed, cost, power 측면에서의최적화를자동으로수행 따라서, 사용자는위와같은복잡한고려없이디자인및설계에집중하여칩개발이가능해짐 사용자수준의언어 Verilog Design Constraints Synthesis Target Library Netlist Speed, Cost, Power 등을고려한셀배치 16
Synthesis? 실제, FPGA 분야는 Synthesis( 자동화도구에의한 ) 도구로인해굉장히발전하게되었음 문제는 Vendor마다최적화또는변환룰이각각다름 검증또한 Synthesis 도구를제공하는 Vendor에의해수행 Optimization 성능에따라가격이결정됨 Optimization 으로인해 design의정형성이깨지게됨 일반적으로좋은결과를제공하지만, 신뢰성 검증이필요 Verilog Synthesis Netlist 17
Formal Verification (Equivalence Checking) 상호다른두디자인간의 functional equivalence 를체크 Netlist 가원래의 RTL 코드를정확하게구현하였는가를검증하기위해사용 ( 또는, Layout 이 Gate-Level Netlist 를정확하게구현하였는가?) 만약 Synthesis Tool 을완전하게믿는다면 EC 는필요하지않다. 대부분의 Synthesis Tool 들이좋은성능을보여주지만, 이런소프트웨어도밝혀지지않은오류가존재할수있기때문에검증이필요하다. 현재 Nuclear domain 에사용된이력이없으며, 관련인증또한획득하지않았음. 검증이필요 18
Development of the EC tool from the scratch 기존 EC 도구 제한적인적용환경 현재, Synplify Pro + Actel Libero SoC 환경을지원하는 EC 도구가없다. Royalty 19
NuDE an integrated PLC/FPGA development framework 20
IN DETAIL
FBD_EC 두 FBD 를입력으로받아 Equivalent 를출력 입력 : FBD 결과 : Equivalent 여부 ROBDD (Reduced Ordered Binary Decision Diagram) 사용 Property: 동일한 logic & ordering 의경우 canonical BDD를가짐 (new?) BDD 생성알고리즘과 Node Replacement 알고리즘제시 FBD 1 Intermediate format ROBDD Equivalent EC engine FBD 2 Intermediate format ROBDD Counter example 22
Binary Decision Diagrams (BDD) Based on recursive Shannon expansion F = x Fx + x Fx a b c f 0 0 0 0 0 0 1 0 0 1 0 0 0 1 1 1 1 0 0 0 1 0 1 1 1 1 0 0 1 1 1 1 f = ac + bc c b f a 0 0 0 1 0 1 0 1 b c c c 23
BDD Manipulation f f f = (a+b)c a a a b b b b b c c c c c c c 0 1 0 1 0 1 1. Merge terminal nodes 2. Merge 3. Remove duplicate redundant nodes nodes 24
BDD Manipulation 25
Ordering Good variable ordering 26
BDD 생성알고리즘과 NODE REPLACE 알고리즘제시
BDD 생성알고리즘과 Node Replace 알고리즘제시 알고리즘 알고리즘1. 분기기반 Backward Tracking 알고리즘 compact 한 BDD 생성 알고리즘2. Node Replace technique 적용 연산수감소 Performance 향상에기여 (?) 28
알고리즘 1. 분기기반 Backward Tracking 알고리즘이란? 분기를기반으로 compact BDD 를생성후마지막단계에서합침 미리 BDD 를생성하면 BDD 의 Size 가커지고연산이복잡해지기때문 14 26 29
14 26 30
기존 BDD 생성 Forward & APPLY 31
APPLY 32
APPLY Algorithm 33
APPLY 34
BDD 생성알고리즘 ( 제시 ) - 분기기반 Backward 알고리즘 35
BDD 생성알고리즘 ( 제시 ) - 분기기반 Backward 알고리즘 0 0 1 36
01 01 0 01 00 00 0 1 0 1 37
분기확인 = 2 01 01 00 0 1 0 1 38
01 1 01 01 1 01 0 01 01 0 0 1 0 1 39
분기확인 = 2 01 1 01 1 01 0 0 1 0 1 40
01 11 01 1 01 10 01 0 01 11 01 10 01 0 1 0 1 41
01 11 01 11 01 10 C 0 1 0 1 42
01 11 D C C 0 1 0 1 43
D C 구현된도구 0 1 44
중간과정 45
Node Replacement 알고리즘 ( 제시 ) Node Replacement technique 알고리즘 1. division & reorder 2. reduction 3. combine & reduction 46
Node Replacement technique 알고리즘 1. division & reorder 2. reduction 3. combine & reduction D D D C C C 0 1 0 1 = 0 = 1 47
Node Replacement technique 알고리즘 1. division & reorder 2. reduction 3. combine & reduction D D D C C C 0 1 0 1 = 0 = 1 48
Node Replacement technique 알고리즘 1. division & reorder 2. reduction 3. combine & reduction D D D C C C 0 1 0 1 = 0 = 1 49
Node Replacement technique 알고리즘 1. division & reorder 2. reduction 3. combine & reduction D C 0 1 0 1 = 0 = 1 50
Summary EC 도구구현중 (new?) 알고리즘 2 개제시 survey, 증명, formalization 필요 BDD 생성방법 (Branch 기반 Backward trace) Node Replacement 방법 과연 performance 가향상되었을지비교분석필요 51
Future work Future work Function: Sequential Equivalence Checking of FBD program Various Input programs: Verilog, VHDL, Gate-level netlist (EDIF) Graphic: Visualization of counter example User friendly GUI Evaluation & Improvement!! Speed, Memory usage Model checking 52
Future Work We are now planning to extend the tool can be used in anywhere in NuDE. If all verifications succeed, we can say that the final software will operate exactly as we intended. 53