More Web Proxy on the site http://driver.im/

research-article

Properties first? A new design methodology for hardware, and its perspectives in safety analysis

Authors:

Shrinidhi Udupi,

Dominik Stoffel,

Wolfgang KunzAuthors Info & Claims

2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Pages 1 - 8

https://doi.org/10.1145/2966986.2980086

Published: 07 November 2016 Publication History

Abstract

This paper discusses the possible role of formal verification techniques in system-level design flows. It is argued that the role of formal verification techniques should not be limited to “bug hunting” alone. Instead, formal technology should be applied in such a way that a formal relationship is provided between an abstract system model and its concrete implementation at the Register Transfer Level (RTL). In order to avoid the high efforts associated with verification by property checking this paper advocates for a top-down methodology where abstract properties are automatically generated from a system-level description and are later refined along the design process. One advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional property checking. Moreover, the proposed approach can be beneficial also when analyzing non-functional design targets. The paper demonstrates this for safety. We present experimental results that show how the effects of Single Event Upsets (SEUs) at the gate level of an SoC module can be related to safety requirements at the system's transaction level with formal precision.

6. References

[1]

M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science 82 (2):253–284, 1991.

Digital Library

[2]

K. Beck. Test Driven Development: By Example. Addison-Wesley 2002.

Digital Library

[3]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. International Design Automation Conference (DAC), pages 317–320, June 1999.

[4]

J. Bormann and H. Busch. Verfahren zur Bestimmung der Güte einer Menge von Eigenschaften (Method for determining the quality of a set of properties). European Patent Application, Publication Number EP1764715, 09 2005.

[5]

M. Boul and Z. Zilic. Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring. Springer Publishing Company Incorporated, 1 edition, 2008.

[6]

K. Claessen. A coverage analysis for safety property lists. In Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 139–145. IEEE Computer Society 2007.

[7]

E. Cohen, W. Paul, and S. Schmaltz Theory of multi-core hypervisor verification. In P. Van Emde Boas, F. C. A. Groen, G. F. Italiano, J. Nawrocki, and H. Sack, editors, SOFSEM 2013: Theory and Practice of Computer Science, volume 7741 of Lecture Notes in Computer Science pages 1–27. Springer, 2013.

[8]

R. Gentilini, C. Piazza, and A. Policriti. From bisimulation to simulation: Coarsest partition problems. J. Autom. Reasoning, 31 (1):73–103, 2003.

Digital Library

[9]

K. Hao, S. Ray, and F. Xie. Equivalence checking for behaviorally synthesized pipelines. In Proceedings of the 49th Annual Design Automation Conference, DAC ‘ 12, pages 344–349, New York, NY, USA, 2012. ACM.

[10]

P. Manolios and S. K. Srinivasan. A complete compositional reasoning framework for the efficient verification of pipelined machines. In Proc. International Conference on Computer-Aided Design (ICCAD), pages 863–870, 2005.

[11]

P. Manolios and S. K. Srinivasan. A refinement-based compositional reasoning framework for pipelined machine verification. IEEE Transactions on VLSI Systems, 16: 353–364, 2008.

Digital Library

[12]

A. Miele. A fault-injection methodology for the system-level dependability analysis of multiprocessor embedded systems. Microprocessors and Microsystems, 38 (6):567–580, 2014.

Digital Library

[13]

R. Milner. Operational and algebraic semantics of concurrent processes. In J. Van Leeuwen, Handbook of theoretical computer science (vol. B), pages 1201–1242. Cambridge, MA, USA: MIT Press, 1990.

[14]

M. D. Nguyen, M. Thalmaier, M. Wedler, J. Bormann, D. Stoffel, and W. Kunz. Unbounded protocol compliance verification using interval property checking with invariants. IEEE Transactions on Computer-Aided Design, 27 (11):2068–2082, November 2008.

Digital Library

[15]

S. Ray and W. A. Hunt, Jr. Deductive verification of pipelined machines using first-order quantification. In Proc. Intl. Conf. on Computer-Aided Verification (CAV), pages 31–43, Boston, MA, 2004. Springer.

[16]

C.-J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6 (2):147–189, 1995.

Digital Library

[17]

B.-A. Tabacaru, M. Chaari, W. Ecker, and T. Kruse. A meta-modeling-based approach for automatic generation of fault-injection processes. DVCon Europe, pages 1–7, 2014.

[18]

J. Urdahl, D. Stoffel, and W. Kunz. Path predicate abstraction for sound system-level models of RT-level circuit designs. IEEE Transactions On Computer-Aided Design of Integrated Circuits and Systems (TCAD), 33 (2):291–304, Feb. 2014.

Digital Library

[19]

J. Urdahl, D. Stoffel, and W. Kunz. Architectural system modeling for correct-by-construction RTL design. In Forum on Specification and Design Languages (FDL), Barcelona, Spain, September 2015.

Cited By

Hu WChang CSengupta ABhunia SKastner RLi H(2021)An Overview of Hardware Security and Trust: Threats, Countermeasures, and Design ToolsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.304797640:6(1010-1038)Online publication date: Jun-2021
https://doi.org/10.1109/TCAD.2020.3047976
Hu WWu LTai YTan JZhang J(2020)A Unified Formal Model for Proving Security and Reliability Properties2020 IEEE 29th Asian Test Symposium (ATS)10.1109/ATS49688.2020.9301533(1-6)Online publication date: 23-Nov-2020
https://doi.org/10.1109/ATS49688.2020.9301533
Devarajegowda KEcker W(2018)Meta-model Based Automation of Properties for Pre-Silicon Verification2018 IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC)10.1109/VLSI-SoC.2018.8644957(231-236)Online publication date: Oct-2018
https://doi.org/10.1109/VLSI-SoC.2018.8644957
Show More Cited By

Index Terms

Properties first? A new design methodology for hardware, and its perspectives in safety analysis
1. Hardware

Index terms have been assigned to the content through auto-classification.

Recommendations

Unbounded safety verification for hardware using software analyzers
DATE '16: Proceedings of the 2016 Conference on Design, Automation & Test in Europe

Demand for scalable hardware verification is ever-increasing. We propose an unbounded safety verification framework for hardware, at the heart of which is a software verifier. To this end, we synthesize Verilog at register transfer level into a software-...
Beyond safety: customized SAT-based model checking
DAC '05: Proceedings of the 42nd annual Design Automation Conference

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) ...
Efficient Model Checking of PSL Safety Properties
ACSD '10: Proceedings of the 2010 10th International Conference on Application of Concurrency to System Design

Safety properties are an important class of properties as in the industrial use of model checking a large majority of the properties to be checked are safety properties. This work presents an efficient approach to model check safety properties expressed ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Nov 2016

946 pages

Copyright © 2016.

Publisher

IEEE Press

Publication History

Published: 07 November 2016

Permissions

Request permissions for this article.

Request Permissions

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
89
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Hu WChang CSengupta ABhunia SKastner RLi H(2021)An Overview of Hardware Security and Trust: Threats, Countermeasures, and Design ToolsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.304797640:6(1010-1038)Online publication date: Jun-2021
https://doi.org/10.1109/TCAD.2020.3047976
Hu WWu LTai YTan JZhang J(2020)A Unified Formal Model for Proving Security and Reliability Properties2020 IEEE 29th Asian Test Symposium (ATS)10.1109/ATS49688.2020.9301533(1-6)Online publication date: 23-Nov-2020
https://doi.org/10.1109/ATS49688.2020.9301533
Devarajegowda KEcker W(2018)Meta-model Based Automation of Properties for Pre-Silicon Verification2018 IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC)10.1109/VLSI-SoC.2018.8644957(231-236)Online publication date: Oct-2018
https://doi.org/10.1109/VLSI-SoC.2018.8644957
Devarajegowda KSchreiner JFindenig REcker WParameswaran S(2017)Python based framework for HDSLs with an underlying formal semanticsProceedings of the 36th International Conference on Computer-Aided Design10.5555/3199700.3199841(1019-1025)Online publication date: 13-Nov-2017
https://dl.acm.org/doi/10.5555/3199700.3199841
Devarajegowda KSchreiner JFindenig REcker W(2017)Python based framework for HDSLs with an underlying formal semantics: (Invited paper)2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)10.1109/ICCAD.2017.8203893(1019-1025)Online publication date: Nov-2017
https://doi.org/10.1109/ICCAD.2017.8203893
Devarajegowda KEcker W(2017)On generation of properties from specification2017 IEEE International High Level Design Validation and Test Workshop (HLDVT)10.1109/HLDVT.2017.8167470(95-98)Online publication date: Oct-2017
https://doi.org/10.1109/HLDVT.2017.8167470

View Options

View options

Media

Figures

Other

Tables

View Table of Contents