Transcription
ISET 20152015.06.04-06DeaguVerification Techniquesqfor COTSDedication of Commercial FPGA ToolsJunbeom Yoo , Eui-Sub Kim , Sejin JungDependable Software LaboratoryKONKUK University2015.06.04
ISET 20152015.06.04-06DeaguFormal Verification Techniques which can beused for COTS SW Dedication of CommercialFPGA Tools used to Develop Safety-CriticalControl Software in Nuclear Power PlantsJunbeom Yoo , Eui-Sub Kim , Sejin JungDependable Software LaboratoryKONKUK University2015.06.04
Platform Change from PLC to FPGADigital I&C(Instrumentation & Control) in nuclear power plantsPLC(Programmable Logic Controller) has been used to implement I&Cs for decades- SW development on industrial computers (CPU & OS)However, increasing maintenance cost and CCF(Common Cause Fault) problem in security- Request for alternative implementation platformsFPGA(Field Programmable Gate Array) is an alternative platform of PLC for I&Cs- Highergcomputationppperformance and strongerg securityy- HW developmentFBD program for PLCNetlist design for FPGA3
FPGA Development ProcessRequirement orDesign SpecificationRTL Design(Verilog or VHDL)Logic Synthesis(3rd Parties)Gate-Level Design(Netlist)PlPlace& RouteR t(Chip Supplier)LayoutIDE (Chip Supplier)FPGA4
FPGA Development Process VerificationRequirement orDesign SpecificationPropertyTest BenchModelCheckingRTL Design(Verilog or VHDL)RTL SimulationGate-Level gStatic TimingAnalysisFPGA5
COTS SW DedicationA process for demonstrating correctness and safety of commercial software (COTS)used directly or indirectly- Direct COTS SW : Directly used in an application to perform safety functions- Indirect COTS SW : Directly produces direct SW (not COTS SW)Two international standards to cope with for digital I&Cs in NPPStandardsTargetEPRI-NP5652(EPRI TR-106439)Commercial Grade Item (CGI)NUREG/CR-6421Direct / Indirect COTS softwareProcessNoteMethod 1 4Focusing onDirect CGIBase of Korean Std.Processes for eachsafetyy categoryg yContainingIndirect CGI Software-based equipments6
COTS SW Dedication for FPGA DevelopmentCOTS software such as logic synthesis and IDEs are always used to develop FPGA.- Indirect COTS SW & Category B- Should take the COTS SW dedication process according to the standardsHere is our interestFPGA Logic Synthesis (Compiler)i an IDEinP&R in IDEThe whole IDE7
COTS SW Dedication : EPRI NP-5652NP-5652 suggests 4 methodsMethod 1 : Special Test and Inspection- Verifying important functionalitiesMethod 2 : Commercial-Grade Survey- Confirming and evaluating QA program of suppliersMethod 3 : Source Verification- Verifying critical characteristics at the supplier’ssupplier sfacility (often impossible)Method 4 : Item/Supplier Performance Record- Verifying acceptability through documented items ors pplie ’s pesupplier’sperformancefo mance recordseco dsMethod 1 is important for logic synthesis- Functionality to verify : correct synthesis- Direct compiler verification techniques can’t be used- It is a commercial compiler (No source code opened)Indirect verification is required- Logic Equivalence Checking(LEC) for specific inputs8
Logic Equivalence CheckingFormally verify(prove) that- for a specific input, the output always shows the same behavior with the inputCommercial LEC tools- FormalPro- Formality(Mentor Graphics)(Synopsys)- Encounter Conformal EC- Jasper Gold(Cadence)- Quartz Formal- 360 ECSynthesisDesign A(Cadence)(Magma Design Automation)(OneSpin Solutions)Design BEquivalenceCheckerTrueCounter Example9
Applicability of LECsApplicability depends on the tool combinations- LEC x Logic Synthesis x IDEsNo applicable LEC for Synopsys Synplify Pro(in Actel Libero IDE)- In this case, we need to develop a customized LECMentor GraphicsLogicg SynthesisyIDEMentor GraphicsXilinx ISEOActel Libero SocOXilinx ISEOPrecision RTLSynopsysSynplify ProXilinxSynopsysXSTDC UltraFormalProCadenceEncounterConformal ECSynopsysFormalityONo LEC availableActel Libero SocAltera Quartus ⅡOXili ISEXilinxO-OO10
A New Customized LEC : CVECA VIS based solution(A Customized VIS based Equivalence Checking)(VIS : Verification Interacting with Synthesis)It can verify the combination of ‘Synopsys Synplify Pro’ with ‘Actel Libero SoC’- An open-sourced formal verification tool, VIS- Translators requiresq(step1,2)( p , ) to use the VIS- Verification performance is up to the VISEquivalence?[3①②③Steps]Verilog Verilog4VISEDIF BLIF-MVBLIF MVVIS Equivalence CheckingTarget Synthesis ToolThe combination of‘Actel Libero IDE’ ‘Synopsys Synplify Pro’11
SummaryFPGA is receiving international attention as an alternative platform of digital I&Cs inNPPs.NPPsWe should do the COTS SW dedication to demonstrate correctness and safetyy ofcommercial software(COTS) used indirectly, such as FPGA logic synthesis and IDEs,according to international standards.LEC(Logic(L i EquivalenceE i lChecking)Ch ki ) is strongly suggested as a means of the special test(M th d 1).(MethodOur target (Current working set) - the combination of Actel Libero Soc with SynopsysSynplify Pro has no LEC solution applicable.In this case, we may need to develop a new customized solution.COTS SW dedication of indirect SW involves an in-depth analysis on the target’sfunctionality and the techniques used to verify the functionality.12
THANK YOUSejin Jung & Eui-Sub Kimhttp://dslab.konkuk.ac.krjbyoo@konkuk ac [email protected]
14
15
16
17
Encounter Synopsys Formality In this case, we need to develop a customized LEC gy Conformal EC Mentor Graphics Precision RTL Xilinx ISE O Actel Libero Soc O Synopsys Synplify Pro Xilinx ISE O O Actel Libero Soc Altera Quartus Ⅱ O XST Xili ISE O O No LEC available Xi
