NDLI: An effective model extraction method with state space compression for model checking SystemC TLM designs

Content Provider	IEEE Xplore Digital Library
Author	Yanyan Gao Xi Li
Copyright Year	2013
Description	Author affiliation: Sch. of Comput. Sci., Univ. of Sci. & Technol. of China, Hefei, China (Xi Li) \|\| Sch. of Comput. & Inf., Hefei Univ. of Technol., Hefei, China (Yanyan Gao)
Abstract	SystemC has become a de-facto standard language for SoC and ASIP designs. The verification of implementation with SystemC is the key to guarantee the correctness of designs and prevent the errors from propagating to the lower levels. The gap between SystemC TLM model and its corresponding formal model makes it hard to perform automated translation between them. SystemC describes process behavior in sequential statements and usually employs intermediate variables, while most model checking languages for hardware only describe parallel behaviors, in which the usage of intermediate variables not only increases state space and may prolong execution time, but also introduce potential errors. For a model checking language which supports parallel description, the elimination of redundant intermediate variables is requisite and also an efficient way to reduce the state space. This paper intends to solve these issues: (1) proposing an extraction method that can implement the translation from a description which supports sequential execution to a description supports parallel execution; (2) identifying and removing redundant intermediate variables. In this paper, a novel mechanism is presented to automatically extract behavior description from SystemC to a widespreadly used model checking language SMV. We have implemented a tool SC2SMV and performed actual extraction process on it to demonstrate the effectiveness of the method presented in this paper.
Starting Page	64
Ending Page	71
File Size	780661
Page Count	8
File Format	PDF
ISBN	9781479901036
DOI	10.1109/SAMOS.2013.6621107
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2013-07-15
Publisher Place	Greece
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	model checking TLM Model checking Educational institutions Hardware Time-domain analysis SMV Equations Time-varying systems Standards SystemC
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Mutation analysis for SystemC designs at TLM

Scalable fault localization for SystemC TLM designs

An assertion-based verification method for SystemC TLM

Automatic Fault Localization for SystemC TLM Designs

CULT: A unified framework for tracing and logging C-based designs

Model checking a SystemC/TLM design of the AMBA AHB protocol

A Semantics-based Translation Method for Automated Verification of SystemC TLM Designs

Combining Behavioural Real-time Software Modelling with the OSCI TLM-2.0 Communication Standard

A SystemC AMS/TLM platform for CMOS video sensors

An effective model extraction method with state space compression for model checking SystemC TLM designs

Similar Documents

Mutation analysis for SystemC designs at TLM

Scalable fault localization for SystemC TLM designs

An assertion-based verification method for SystemC TLM

Automatic Fault Localization for SystemC TLM Designs

CULT: A unified framework for tracing and logging C-based designs

Model checking a SystemC/TLM design of the AMBA AHB protocol

A Semantics-based Translation Method for Automated Verification of SystemC TLM Designs

Combining Behavioural Real-time Software Modelling with the OSCI TLM-2.0 Communication Standard

A SystemC AMS/TLM platform for CMOS video sensors

An effective model extraction method with state space compression for model checking SystemC TLM designs