Skip to main content
Top

Hint

Swipe to navigate through the chapters of this book

2020 | OriginalPaper | Chapter

AADD-Based Symbolic Simulation of SystemC AMS

Authors : Carna Zivkovic, Christoph Grimm

Published in: Languages, Design Methods, and Tools for Electronic System Design

Publisher: Springer International Publishing

share
SHARE

Abstract

Traditional modeling languages and simulators are still separated from formal verification languages and tools. The main reason for this is that formal verification algorithms require a formal model of a system to verify its behavior. However, the automatic generation of such model requires a separate, dedicated compiler. This paper shows an approach how to use the existing simulator to generate a formal model of a system without using yet another compiler, intermediate language or tool. The approach is based on generation of AADD and BDD for symbolic simulation and it is integrated in SystemC AMS modeling language and simulator.
Literature
6.
go back to reference Große, D., Le, H. M., & Drechsler, R. (2010). Proving transaction and system-level properties of untimed SystemC TLM designs. In Proceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE ’10 (pp. 113–122). Washington: IEEE Computer Society. https://​doi.​org/​10.​1109/​MEMCOD.​2010.​5558643. Große, D., Le, H. M., & Drechsler, R. (2010). Proving transaction and system-level properties of untimed SystemC TLM designs. In Proceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE ’10 (pp. 113–122). Washington: IEEE Computer Society. https://​doi.​org/​10.​1109/​MEMCOD.​2010.​5558643.
15.
go back to reference Sammane, G. A., Zaki, M. H., Tahar, S., & Bois, G. (2007). Constraint-Based verification of delta-sigma modulators using interval analysis. In 50th Midwest Symposium on Circuits and Systems (pp. 726–729). Sammane, G. A., Zaki, M. H., Tahar, S., & Bois, G. (2007). Constraint-Based verification of delta-sigma modulators using interval analysis. In 50th Midwest Symposium on Circuits and Systems (pp. 726–729).
16.
go back to reference Sen, K., Marinov, D., & Agha, G. (2005). Cute: A concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-13, pp. 263–272. New York: ACM. http://​doi.​acm.​org/​10.​1145/​1081706.​1081750. Sen, K., Marinov, D., & Agha, G. (2005). Cute: A concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-13, pp. 263–272. New York: ACM. http://​doi.​acm.​org/​10.​1145/​1081706.​1081750.
18.
go back to reference Zivkovic, C., & Grimm, C. (2018). Symbolic simulation of SystemC AMS without yet another compiler. In Forum on Specification and Design Languages 2018, pp. 5–16. Zivkovic, C., & Grimm, C. (2018). Symbolic simulation of SystemC AMS without yet another compiler. In Forum on Specification and Design Languages 2018, pp. 5–16.
19.
go back to reference Zivkovic, C., & Grimm, C. (2019). Nubolic simulation of AMS systems with data flow and discrete event models. In DATE 2019, Accepted for a Long Presentation; To be Presented in March 2019 Zivkovic, C., & Grimm, C. (2019). Nubolic simulation of AMS systems with data flow and discrete event models. In DATE 2019, Accepted for a Long Presentation; To be Presented in March 2019
Metadata
Title
AADD-Based Symbolic Simulation of SystemC AMS
Authors
Carna Zivkovic
Christoph Grimm
Copyright Year
2020
DOI
https://doi.org/10.1007/978-3-030-31585-6_8