New Methodology for Complete Properties Extraction from Simulation Traces Guided with Static Analysis
Pages 705 - 719
Abstract
This paper introduces a new methodology for digital design properties extraction from simulation traces. A new Breadth-First Decision Tree (BF-DT) mining algorithm is proposed for complete properties extraction from simulation traces. The new mining engine supports both bit-level and word-level values of different design variables. Static analysis technique is implemented to extract all data dependencies between the digital design variables. New traces regeneration algorithm is proposed to obtain reduced traces for more efficient and easier mining. The mining engine is guided with these data dependencies to extract complete design properties relating target variables desired to extract properties for and their cone of interest feature variables. The contributed mining technique has been tested for different designs with different sizes. The design properties generated from the mining engine completely match with all design properties covered in the input simulation traces. Moreover, the generated properties are at the highest possible level of abstraction leading to the best coverage for the input data space. The simulation results show that the proposed methodology has superior efficiency in extracting both bit-level and word-level complete assertions of digital design in both superior quality and feasible time.
References
[1]
Boulé M, Zilic Z (2008) Automata-based assertion-checker synthesis of PSL properties. ACM Trans Des Autom Electron Syst 13(1):1---21
[2]
Chen KC (2003) Assertion-based verification for SoC designs, IEEE 5th International Conference on ASIC, Beijing, China, pp.12---15, 21---24
[3]
El Mandouh E, Wassal AG (2012) Automatic Generation of Hardware Design Properties from Simulation Traces, IEEE International Symposium on Circuits and Systems (ISCAS), pp. 2317---2320, 20---23
[4]
Foster H (2009) Applied assertion-based verification: an industry perspective. Found Trends Elec Design Auto 3(I):1---95
[5]
Foster H, Lacey D, Krolnik A (2003) Assertion-based design. Kluwer Academic Publishers, Norwell
[6]
Hanafy M, Said H, Wahba AM (2015) Complete Properties Extraction from Simulation Traces for Assertions Auto-Generation, IEEE 24th North Atlantic Test Workshop (NATW 2015), pp. 1---6, 11---13
[7]
Hangal S, Chandra N, Narayanan S, Chakravorty S (2005) Iodine: a tool to automatically infer dynamic invariants for hardware designs, 42nd annual Design Automation Conference (DAC '05), New York, USA, pp. 775---778
[8]
Hertz S, Sheridan D, Vasudevan S (2013) Mining hardware assertions with guidance from static analysis. IEEE Trans Comput-Aided Design Integr Circuits Syst 32:952---965
[9]
IEEE Std (1800---2009) IEEE Standard for SystemVerilog --- Unified Hardware Design, Specification, and Verification Language. Institute of Electrical and Electronic Engineers, New York
[10]
IEEE Std (1850---2010) IEEE Standard for Property Specification Language (PSL). Institute of Electrical and Electronic Engineers, New York
[11]
IEEE Std. 1800.2 (2015) IEEE Standard for Universal Verification Methodology Language Reference Manual. Institute of Electrical and Electronic Engineers, New York
[12]
ITRS (2013) International techoology roadmap for semiconductors report
[13]
Kayed M, Abdelsalam M, Guindi R (2014) A Novel Approach for SVA Generation of DDR Memory Protocols Based on TDML, 15th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions, December 15---16
[14]
Liu L, Sheridan D, Athavale V, Vasudevan S (2011) Automatic Generation of Assertions from System Level Design Using Data Mining, 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 191---200
[15]
Liu L, Lin C, Vasudevan S (2012) Word Level Feature Discovery to Enhance Quality of Assertion Mining, IEEE/ACM International Conference on Computer-Aided Design (ICCAD), pp. 210---217
[16]
Morris Mano M Digital Design, Third Edition, 2002, Prentice-Hall
[17]
Mostafa M, Safar M, El-Kharashi MW, Dessouky M (2014) SystemVerilog Assertion Debugging based on Visualization, Simulation Results and Mutation, 15th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions, December 15---16
[18]
Opencores benchmarks http://opencores.org
[19]
Questa® Advanced Simulator http://www.mentor.com/products/fv/ questa/
[20]
Sheridan D, Liu L, Kim H, Vasudevan S (2014) A Coverage Guided Mining Approach for Automatic Generation of Succinct Assertions, 27th International Conference on VLSI Design and 13th International Conference on Embedded Systems, pp. 68---73
[21]
Tong JG, Sarraf D, Boulé M, Zilic Z (2011) Generating Compact Assertions for Control-Based Logic Signals, IEEE 54th International Midwest Symposium on Circuits and Systems (MWSCAS), 2011, pp. 1---4
[22]
Vasudevan S, Sheridan D, Patel S, Tcheng D, Tuohy B, Johnson D (2010) GoldMine: Automatic Assertion Generation Using Data Mining and Static Analysis, Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 626---629
[23]
Zaki M, Tahar S (2003) Syntax code analysis and generation for Verilog. IEEE CCECE 2003, Can Conf Electr Comput Eng 1:235---240 4---7
- New Methodology for Complete Properties Extraction from Simulation Traces Guided with Static Analysis
Recommendations
Complete Properties Extraction from Simulation Traces for Assertions Auto-generation
NATW '15: Proceedings of the 2015 IEEE 24rd North Atlantic Test WorkshopMachine learning techniques based on Data Miningare employed for automatic assertion generation in hardwaredigital design verification. This paper presents a new miningtechnique to extract all design properties from simulation traces.The extracted ...
Inline Assertions - Embedding Formal Properties in a Test Bench
VLSID '09: Proceedings of the 2009 22nd International Conference on VLSI DesignThe scope of immediate assertions in SystemVerilog is restricted to Boolean properties, where as temporal properties are specified as concurrent assertions. Concurrent assertion statements can also be embedded in a procedural block - known as procedural ...
Back-annotation of Simulation Traces with Change-Driven Model Transformations
SEFM '10: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal MethodsModel-driven analysis aims at detecting design flaws early in high-level design models by automatically deriving mathematical models. These analysis models are subsequently investigated by formal verification and validation (V&V) tools, which may ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2016 Springer Science+Business Media New York.
Publisher
Kluwer Academic Publishers
United States
Publication History
Published: 01 December 2016
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 09 Jan 2025