Blog
About

  • Record: found
  • Abstract: found
  • Article: found
Is Open Access

Building SystemC waiting state automata

, ,

Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011) (VECOS)

Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

15-16 September 2011

SystemC, automata, operational semantics, symbolic execution, compostional verification

Read this article at

Bookmark
      There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

      Abstract

      SystemC is becoming a de facto standard for the system-level description of system-on-chip. However most formal verification techniques used for verifying hardware components targets low level design, usually netlist or RTL, but time-to-market requirements have rushed the industry towards design paradigms that offer a very high level of abstraction. In previous works, we proposed a verification methodology based on SystemC waiting-state automata, an abstract formal model for verifying properties of SystemC at the transaction level within a delta-cycle. The main drawback of thismodel is that it should be providedmanually. In this paper, we propose a method to automatically build the SystemC waiting-state automata from the SystemC code. It is based on an extended symbolic execution of the SystemC design that takes care of synchronous as well as asynchronous communications and that preserves the semantics of SystemC up to a delta-cycle.

      Related collections

      Most cited references 5

      • Record: found
      • Abstract: not found
      • Book Chapter: not found

      Counterexample-Guided Abstraction Refinement

        Bookmark
        • Record: found
        • Abstract: not found
        • Book Chapter: not found

        Construction of abstract state graphs with PVS

          Bookmark
          • Record: found
          • Abstract: not found
          • Article: not found

          Formal Verification of SystemC Designs Using a Petri-Net Based Representation

            Bookmark

            Author and article information

            Affiliations
            UEI, ENSTA, 32 Bd Victor,

            75739 Paris cedex 15, Francewww.ensta-paristech.fr
            CEDRIC, CNAM, 292 rue Saint Martin,

            75141 Paris cedex 03, Francewww.cnam.fr
            Contributors
            Conference
            September 2011
            September 2011
            : 1-12
            10.14236/ewic/VECOS2011.11
            © Nesrine HARRATH et al. Published by BCS Learning and Development Ltd. Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011), Tunis, Tunisia

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
            VECOS
            5
            Tunis, Tunisia
            15-16 September 2011
            Electronic Workshops in Computing (eWiC)
            Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
            Product
            Product Information: 1477-9358 BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article