Article

Simulation-guided property checking based on a multi-valued AR-automata

Authors:

J. Ruf,

D. Hoffmann,

T. Kropf,

W. RosenstielAuthors Info & Claims

DATE '01: Proceedings of the conference on Design, automation and test in Europe

Pages 742 - 748

Published: 13 March 2001 Publication History

Get Access

References

[1]

L. Augustin, B. Gennart, Y. Huh, D. Luckham, and A. Stanculescu. Verification of VHDL designs using VAL. In Design Automation Conference (DAC), pages 48-53. ACM/IEEE, 1988.

Digital Library

Google Scholar

[2]

D. Brand. Verification of Large Synthesized Designs. In IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 534-537, Santa Clara, California, November 1993. ACM/IEEE, IEEE Computer Society Press.

Digital Library

Google Scholar

[3]

J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic Model Checking: 10 20 States and Beyond. In IEEE Symposium on Logic in Computer Science (LICS), pages 1-33, Washington, D.C., June 1990. IEEE Computer Society Press.

Google Scholar

[4]

W. Canfield, E. Emerson, and A. Saha. Checking formal specifications under simulation. In International Conference on Computer Design (ICCD '97). IEEE Computer Society Press, 1997.

Digital Library

Google Scholar

[5]

E. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 996-1072, Amsterdam, 1990. Elsevier Science Publishers.

Digital Library

Google Scholar

[6]

T. Kropf. Formal Hardware Verification - Methods and Systems in Comparison, volume 1287 of Lecture Notes in Computer Science. Springer Verlag, state of the art report edition, August 1997.

Digital Library

Google Scholar

[7]

K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.

Digital Library

Google Scholar

[8]

R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer- Verlag, New York, 1980.

Digital Library

Google Scholar

[9]

B. Nelson and R. Jones. Simulation event pattern checking with proto. In SHDL 1994, 1994.

Google Scholar

[10]

M. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959.

Digital Library

Google Scholar

[11]

J. Ruf, D. W. Hoffmann, T. Kropf, and W. Rosenstiel. Simulation based validation of fltl formulas in executable system descriptions. In R. Seepold, editor, Forum on Design Languages (FDL 2000), pages 311-319, T~bingen, Germany, September 2000. Sig.-VHDL and ECSI.

Google Scholar

[12]

Synopsys Inc., CoWare Inc., and Frontier Design Inc., www.systemc.org. SystemC Version 1.0 User's Guide.

Google Scholar

Cited By

View all

Reiter SBurger AViehl ABringmann ORosenstiel WBarros FPerumalla KEwald R(2014)Virtual prototyping evaluation framework for automotive embedded systems engineeringProceedings of the 7th International ICST Conference on Simulation Tools and Techniques10.4108/icst.simutools.2014.254625(1-10)Online publication date: 17-Mar-2014
https://dl.acm.org/doi/10.4108/icst.simutools.2014.254625
Morgenstern AGesell MSchneider K(2012)An asymptotically correct finite path semantics for LTLProceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning10.1007/978-3-642-28717-6_24(304-319)Online publication date: 11-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28717-6_24
Lämmermann SRuf JKropf TRosenstiel WViehl AJesser AHedrich LDe Micheli GAl-Hashimi BMueller WMacii E(2010)Towards assertion-based verification of heterogeneous system designsProceedings of the Conference on Design, Automation and Test in Europe10.5555/1870926.1871210(1171-1176)Online publication date: 8-Mar-2010
https://dl.acm.org/doi/10.5555/1870926.1871210
Show More Cited By

Index Terms

Recommendations

Active property checking
EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

Runtime property checking (as implemented in tools like Purify or Valgrind) checks whether a program execution satisfies a property. Active property checking extends runtime checking by checking whether the property is satisfied by all program ...
Three-valued logic in bounded model checking
MEMOCODE '05: Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

In principle, bounded model checking (BMC) leads to semi-decision procedures that can be used to verify liveness properties and to falsify safety properties. If the procedures fail, there is usually no information about the validity of the considered ...
Property-Specific Testbench Generation for Guided Simulation
ASP-DAC '02: Proceedings of the 2002 Asia and South Pacific Design Automation Conference

Simulation continues to be the primary technique for functional validation of designs. It is important that simulation vectors be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The overall ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '01: Proceedings of the conference on Design, automation and test in Europe

March 2001

756 pages

ISBN:0769509932

Editors:
Wolfgang Nebel
Oldenburg Univ. and OFFIS, Germany
,
Ahmed Jerraya
TIMA, Grenoble, France

Publisher

IEEE Press

Publication History

Published: 13 March 2001

Check for updates

Qualifiers

Article

Conference

DATE01

Sponsor:

EDAA
IFIP WG 10.5
EDAC
SIGDA
IEEE-CS\TTTC
IEEE-CS\DATC
The Russian Academy of Sciences

DATE01: Design, Automation and Test in Europe

Munich, Germany

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
223
Total Downloads

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

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Reiter SBurger AViehl ABringmann ORosenstiel WBarros FPerumalla KEwald R(2014)Virtual prototyping evaluation framework for automotive embedded systems engineeringProceedings of the 7th International ICST Conference on Simulation Tools and Techniques10.4108/icst.simutools.2014.254625(1-10)Online publication date: 17-Mar-2014
https://dl.acm.org/doi/10.4108/icst.simutools.2014.254625
Morgenstern AGesell MSchneider K(2012)An asymptotically correct finite path semantics for LTLProceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning10.1007/978-3-642-28717-6_24(304-319)Online publication date: 11-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28717-6_24
Lämmermann SRuf JKropf TRosenstiel WViehl AJesser AHedrich LDe Micheli GAl-Hashimi BMueller WMacii E(2010)Towards assertion-based verification of heterogeneous system designsProceedings of the Conference on Design, Automation and Test in Europe10.5555/1870926.1871210(1171-1176)Online publication date: 8-Mar-2010
https://dl.acm.org/doi/10.5555/1870926.1871210
Braun ABringmann OLettnin DRosenstiel WDe Micheli GAl-Hashimi BMueller WMacii E(2010)Simulation-based verification of the MOST NetInterface specification revision 3.0Proceedings of the Conference on Design, Automation and Test in Europe10.5555/1870926.1871053(538-543)Online publication date: 8-Mar-2010
https://dl.acm.org/doi/10.5555/1870926.1871053
Cansell DMéry DProch C(2009)System-on-chip design by proof-based refinementInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220918.322122311:3(217-238)Online publication date: 1-Jul-2009
https://dl.acm.org/doi/10.5555/3220918.3221223
Lettnin DNalla PRuf JKropf TRosenstiel WKirsten TSchönknecht VReitemeyer SSciuto D(2008)Verification of temporal properties in automotive embedded softwareProceedings of the conference on Design, automation and test in Europe10.1145/1403375.1403417(164-169)Online publication date: 10-Mar-2008
https://dl.acm.org/doi/10.1145/1403375.1403417
Verma SHarris IRamineni KLauwereins RMadsen J(2007)Interactive presentation: Automatic generation of functional coverage models from behavioral verilog descriptionsProceedings of the conference on Design, automation and test in Europe10.5555/1266366.1266560(900-905)Online publication date: 16-Apr-2007
https://dl.acm.org/doi/10.5555/1266366.1266560
Karlsson DEles PPeng ZGielen G(2006)Formal verification of systemc designs using a petri-net based representationProceedings of the conference on Design, automation and test in Europe: Proceedings10.5555/1131481.1131824(1228-1233)Online publication date: 6-Mar-2006
https://dl.acm.org/doi/10.5555/1131481.1131824
Peranandam PNalla PRuf JWeiss RKropf TRosenstiel WSentovich E(2006)Fast falsification based on symbolic bounded property checkingProceedings of the 43rd annual Design Automation Conference10.1145/1146909.1147181(1077-1082)Online publication date: 24-Jul-2006
https://dl.acm.org/doi/10.1145/1146909.1147181
Nalla PWeiss RPeranandam PRuf JKropf TRosenstiel W(2006)Distributed Symbolic Bounded Property CheckingElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.10.018135:2(47-63)Online publication date: 1-Feb-2006
https://dl.acm.org/doi/10.1016/j.entcs.2005.10.018
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Active property checking

Three-valued logic in bounded model checking

Property-Specific Testbench Generation for Guided Simulation