Reza Hajisheykhi
ABSTRACT
In this paper, we evaluate the effectiveness of model slicing to provide assurance about correctness of SystemC TLM programs. The need for such assurance is important since SystemC has become a de-facto standard for building systems with hardware/software co-design. Existing approaches that enable one to transform the given SystemC TLM program into an UPPAAL model that can be verified suffer from models that result in state space explosion. This problem becomes even more complex when verifying fault-tolerance. Model slicing has the potential to provide a solution to this problem. Therefore, we focus on developing a model slicer that extends existing work on model slicing and combines it with tools to generate UPPAAL models from SystemC TLM programs and tools to add the impact of faults to those UPPAAL models. The experimental results show that with the proposed framework, the designer is capable of verifying even very complex SystemC TLM models, which would have been impossible without the proposed approach.
- Getting Started with TLM-2.0. http://www.doulos.com/knowhow/systemc/tlm2/.Google Scholar
- Karlsruhe SystemC Parser Suite (KaSCPar). http://forge.greensocs.com/en/Projects/KaSCPar/.Google Scholar
- Open SystemC Initiative (OSCI): Defining and advancing SystemC standard IEEE 1666-2005. http://www.systemc.org/.Google Scholar
- Transaction-Level Modeling (TLM) 2.0 Reference Manual. http://www.systemc.org/downloads/standards/.Google Scholar
- Gerd Behrmann, Alexandre David, and Kim Guldstrand Larsen. A tutorial on uppaal. In SFM, pages 200--236, 2004.Google ScholarCross Ref
- R. Hajisheykhi, A. Ebnenasir, and S. Kulkarni. UFIT: A tool for modeling faults in UPPAAL timed automata. In NFM, pages 429--435, 2015.Google ScholarCross Ref
- P. Herber, M. Pockrandt, and S.e Glesner. Transforming SystemC Transaction Level Models into UPPAAL timed automata. In MEMOCODE, pages 161--170, 2011.Google ScholarDigital Library
- A. Janowska and P. Janowski. Slicing of timed automata with discrete data. Fundam. Inform., 72(1-3):181--195, 2006. Google ScholarDigital Library
- K. Tanabe, S. Sasaki, and M. Fujita. Program slicing for system level designs in SpecC. In IASTED, pages 252--258, 2004.Google Scholar
- D. Thomas., E. Lagnese, J. Nestor, J. Rajan, R. Blackburn, and R. Walker. Algorithmic and Register-Transfer Level Synthesis: The System Architect's Workbench. Kluwer Academic Publishers, Norwell, MA, USA, 1989. Google ScholarDigital Library
- M. Weiser. Program slicing. IEEE Trans. Software Eng., 10(4):352--357, 1984. Google ScholarDigital Library
Recommendations
Induction-Based Formal Verification of SystemC TLM Designs
MTV '09: Proceedings of the 2009 10th International Workshop on Microprocessor Test and VerificationIn this paper we present a formal verification approach for SystemC TLM designs. The approaches allows to check expressive properties and uses induction to cope with the large state space of abstract SystemC programs. The technique is tightly integrated ...
Testbench Qualification of SystemC TLM Protocols through Mutation Analysis
Transaction-level modeling (TLM) has become the de-facto reference modeling style for system-level design and verification of embedded systems. It allows designers to implement high-level communication protocols for simulations up to $1000 \times $ ...
Reusing RTL Assertion Checkers for Verification of SystemC TLM Models
The recent trend towards system-level design gives rise to new challenges for reusing existing (RTL) intellectual properties (IPs) and their verification environment in (TLM). While techniques and tools to abstract (RTL) IPs into TLM models have begun ...
Comments