---
_id: '36994'
abstract:
- lang: eng
  text: This paper proposes a quality driven, simulation based approach to functional
    design verification, which applies mainly to IP-level HDL designs with well specified
    test instruction format and is evaluated on a soft microprocessor core MB-LITE
    [5]. The approach utilizes mutation analysis as the quality metric to steer an
    automated simulation data generation process. It leads to a simulation flow with
    two phases towards an enhanced mutation analysis result. First in a random simulation
    phase, an in-loop heuristics is deployed and adjusts dynamically the test probability
    distribution so as to improve the coverage efficiency. Next, for each remaining
    hard-to-kill mutant, a search heuristics on test input space is developed to iteratively
    locate a target test, using a specific objective cost function for the goal of
    killing HDL mutant. The effectiveness of this integrated two-phase simulation
    flow is demonstrated by the results with the MB-LITE microprocessor IP.
author:
- first_name: 'Tao '
  full_name: 'Xie, Tao '
  last_name: Xie
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
- first_name: Florian
  full_name: Letombe, Florian
  last_name: Letombe
citation:
  ama: 'Xie T, Müller W, Letombe F. Mutation-Analysis Driven Functional Verification
    of a Soft Microprocessor. In: <i>Proceedings of SOCC2012</i>. IEEE; 2012. doi:<a
    href="https://doi.org/10.1109/SOCC.2012.6398362">10.1109/SOCC.2012.6398362</a>'
  apa: Xie, T., Müller, W., &#38; Letombe, F. (2012). Mutation-Analysis Driven Functional
    Verification of a Soft Microprocessor. <i>Proceedings of SOCC2012</i>. <a href="https://doi.org/10.1109/SOCC.2012.6398362">https://doi.org/10.1109/SOCC.2012.6398362</a>
  bibtex: '@inproceedings{Xie_Müller_Letombe_2012, place={ Niagara Falls, NY, USA
    }, title={Mutation-Analysis Driven Functional Verification of a Soft Microprocessor},
    DOI={<a href="https://doi.org/10.1109/SOCC.2012.6398362">10.1109/SOCC.2012.6398362</a>},
    booktitle={Proceedings of SOCC2012}, publisher={IEEE}, author={Xie, Tao  and Müller,
    Wolfgang and Letombe, Florian}, year={2012} }'
  chicago: 'Xie, Tao , Wolfgang Müller, and Florian Letombe. “Mutation-Analysis Driven
    Functional Verification of a Soft Microprocessor.” In <i>Proceedings of SOCC2012</i>.  Niagara
    Falls, NY, USA : IEEE, 2012. <a href="https://doi.org/10.1109/SOCC.2012.6398362">https://doi.org/10.1109/SOCC.2012.6398362</a>.'
  ieee: 'T. Xie, W. Müller, and F. Letombe, “Mutation-Analysis Driven Functional Verification
    of a Soft Microprocessor,” 2012, doi: <a href="https://doi.org/10.1109/SOCC.2012.6398362">10.1109/SOCC.2012.6398362</a>.'
  mla: Xie, Tao, et al. “Mutation-Analysis Driven Functional Verification of a Soft
    Microprocessor.” <i>Proceedings of SOCC2012</i>, IEEE, 2012, doi:<a href="https://doi.org/10.1109/SOCC.2012.6398362">10.1109/SOCC.2012.6398362</a>.
  short: 'T. Xie, W. Müller, F. Letombe, in: Proceedings of SOCC2012, IEEE,  Niagara
    Falls, NY, USA , 2012.'
date_created: 2023-01-17T08:46:14Z
date_updated: 2023-01-17T08:46:29Z
department:
- _id: '672'
doi: 10.1109/SOCC.2012.6398362
keyword:
- Analytical models
- Hardware design languages
- Microprocessors
- Cost function
- Data models
- Search problems
- IP networks
language:
- iso: eng
place: ' Niagara Falls, NY, USA '
publication: Proceedings of SOCC2012
publication_identifier:
  eisbn:
  - 978-1-4673-1295-0
publisher: IEEE
status: public
title: Mutation-Analysis Driven Functional Verification of a Soft Microprocessor
type: conference
user_id: '5786'
year: '2012'
...
---
_id: '37002'
abstract:
- lang: eng
  text: HDL-mutation based fault injection and analysis is considered as an important
    coverage metric for measuring the quality of design simulation processes [20,
    3, 1, 2]. In this work, we try to solve the problem of automatic simulation data
    generation targeting HDL mutation faults. We follow a search based approach and
    eliminate the need for symbolic execution and mathematical constraint solving
    from existing work. An objective cost function is defined on the test input space
    and serves the guidance of search for fault-detecting test data. This is done
    by first mapping the simulation traces under a test onto a control and data flow
    graph structure which is extracted from the design. Then the progress of fault
    detection can be measured quantitatively on this graph to be the cost value. By
    minimizing this cost we approach the target test data. The effectiveness of the
    cost function is investigated under an example neighborhood search scheme. Case
    study with a floating point arithmetic IP design has shown that the cost function
    is able to guide effectively the search procedure towards a fault-detecting test.
    The cost calculation time as the search overhead was also observed to be minor
    compared to the actual design simulation time.
author:
- first_name: Tao
  full_name: Xie, Tao
  last_name: Xie
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
- first_name: Florian
  full_name: Letombe, Florian
  last_name: Letombe
citation:
  ama: 'Xie T, Müller W, Letombe F. HDL-Mutation Based Simulation Data Generation
    by Propagation Guided Search. In: <i>Proceedings of Euromicro DSD 2011</i>. IEEE;
    2011. doi:<a href="https://doi.org/10.1109/DSD.2011.83">10.1109/DSD.2011.83</a>'
  apa: Xie, T., Müller, W., &#38; Letombe, F. (2011). HDL-Mutation Based Simulation
    Data Generation by Propagation Guided Search. <i>Proceedings of Euromicro DSD
    2011</i>. <a href="https://doi.org/10.1109/DSD.2011.83">https://doi.org/10.1109/DSD.2011.83</a>
  bibtex: '@inproceedings{Xie_Müller_Letombe_2011, place={Oulu, Finnland}, title={HDL-Mutation
    Based Simulation Data Generation by Propagation Guided Search}, DOI={<a href="https://doi.org/10.1109/DSD.2011.83">10.1109/DSD.2011.83</a>},
    booktitle={Proceedings of Euromicro DSD 2011}, publisher={IEEE}, author={Xie,
    Tao and Müller, Wolfgang and Letombe, Florian}, year={2011} }'
  chicago: 'Xie, Tao, Wolfgang Müller, and Florian Letombe. “HDL-Mutation Based Simulation
    Data Generation by Propagation Guided Search.” In <i>Proceedings of Euromicro
    DSD 2011</i>. Oulu, Finnland: IEEE, 2011. <a href="https://doi.org/10.1109/DSD.2011.83">https://doi.org/10.1109/DSD.2011.83</a>.'
  ieee: 'T. Xie, W. Müller, and F. Letombe, “HDL-Mutation Based Simulation Data Generation
    by Propagation Guided Search,” 2011, doi: <a href="https://doi.org/10.1109/DSD.2011.83">10.1109/DSD.2011.83</a>.'
  mla: Xie, Tao, et al. “HDL-Mutation Based Simulation Data Generation by Propagation
    Guided Search.” <i>Proceedings of Euromicro DSD 2011</i>, IEEE, 2011, doi:<a href="https://doi.org/10.1109/DSD.2011.83">10.1109/DSD.2011.83</a>.
  short: 'T. Xie, W. Müller, F. Letombe, in: Proceedings of Euromicro DSD 2011, IEEE,
    Oulu, Finnland, 2011.'
date_created: 2023-01-17T09:02:48Z
date_updated: 2025-02-26T14:44:15Z
department:
- _id: '672'
doi: 10.1109/DSD.2011.83
keyword:
- Hardware design languages
- Cost function
- Computational modeling
- Fault detection
- Data models
- Analytical models
- Testing
language:
- iso: eng
place: Oulu, Finnland
publication: Proceedings of Euromicro DSD 2011
publication_identifier:
  isbn:
  - 978-1-4577-1048-3
publisher: IEEE
status: public
title: HDL-Mutation Based Simulation Data Generation by Propagation Guided Search
type: conference
user_id: '5786'
year: '2011'
...
---
_id: '37009'
abstract:
- lang: eng
  text: Today, mobile and embedded real time systems have to cope with the migration
    and allocation of multiple software tasks running on top of a real time operating
    system (RTOS) residing on one or several processors. For scaling of each task
    set and processor configuration, instruction set simulation and worst case timing
    analysis are typically applied. This paper presents a complementary approach for
    the verification of RTOS properties based on an abstract RTOS-Model in SystemC.
    We apply IEEE P1850 PSL for which we present an approach and first experiences
    for the assertion-based verification of RTOS properties.
author:
- first_name: Marcio F. S.
  full_name: Oliveira, Marcio F. S.
  last_name: Oliveira
- first_name: Henning
  full_name: Zabel, Henning
  last_name: Zabel
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
citation:
  ama: 'Oliveira MFS, Zabel H, Müller W. Assertion-Based Verification of RTOS Properties.
    In: <i>Proceedings of DATE’10</i>. IEEE; 2010. doi:<a href="https://doi.org/10.1109/DATE.2010.5457130">10.1109/DATE.2010.5457130</a>'
  apa: Oliveira, M. F. S., Zabel, H., &#38; Müller, W. (2010). Assertion-Based Verification
    of RTOS Properties. <i>Proceedings of DATE’10</i>. 2010 Design, Automation &#38;
    Test in Europe Conference &#38; Exhibition (DATE 2010), Dresden. <a href="https://doi.org/10.1109/DATE.2010.5457130">https://doi.org/10.1109/DATE.2010.5457130</a>
  bibtex: '@inproceedings{Oliveira_Zabel_Müller_2010, place={Dresden}, title={Assertion-Based
    Verification of RTOS Properties}, DOI={<a href="https://doi.org/10.1109/DATE.2010.5457130">10.1109/DATE.2010.5457130</a>},
    booktitle={Proceedings of DATE’10}, publisher={IEEE}, author={Oliveira, Marcio
    F. S. and Zabel, Henning and Müller, Wolfgang}, year={2010} }'
  chicago: 'Oliveira, Marcio F. S., Henning Zabel, and Wolfgang Müller. “Assertion-Based
    Verification of RTOS Properties.” In <i>Proceedings of DATE’10</i>. Dresden: IEEE,
    2010. <a href="https://doi.org/10.1109/DATE.2010.5457130">https://doi.org/10.1109/DATE.2010.5457130</a>.'
  ieee: 'M. F. S. Oliveira, H. Zabel, and W. Müller, “Assertion-Based Verification
    of RTOS Properties,” presented at the 2010 Design, Automation &#38; Test in Europe
    Conference &#38; Exhibition (DATE 2010), Dresden, 2010, doi: <a href="https://doi.org/10.1109/DATE.2010.5457130">10.1109/DATE.2010.5457130</a>.'
  mla: Oliveira, Marcio F. S., et al. “Assertion-Based Verification of RTOS Properties.”
    <i>Proceedings of DATE’10</i>, IEEE, 2010, doi:<a href="https://doi.org/10.1109/DATE.2010.5457130">10.1109/DATE.2010.5457130</a>.
  short: 'M.F.S. Oliveira, H. Zabel, W. Müller, in: Proceedings of DATE’10, IEEE,
    Dresden, 2010.'
conference:
  location: Dresden
  name: 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)
date_created: 2023-01-17T09:15:10Z
date_updated: 2023-01-17T09:15:18Z
department:
- _id: '672'
doi: 10.1109/DATE.2010.5457130
keyword:
- Operating systems
- Real time systems
- Timing
- Hardware
- Analytical models
- Embedded software
- Software systems
- Processor scheduling
- Software performance
- Performance analysis
language:
- iso: eng
place: Dresden
publication: Proceedings of DATE’10
publisher: IEEE
status: public
title: Assertion-Based Verification of RTOS Properties
type: conference
user_id: '5786'
year: '2010'
...
---
_id: '37066'
abstract:
- lang: eng
  text: Today, mobile and embedded real-time systems have to cope with the migration
    and allocation of multiple software tasks running on top of a real-time operating
    system (RTOS) residing on one or multiple system processors. Abstract RTOS simulations
    and timing analysis applies for fast and early estimation to configure it towards
    the individual needs of the application and environment. In this context, a high
    accuracy of the simulation compared to an instruction set simulation (ISS) is
    of key importance. In this paper, we investigate the accuracy of abstract RTOS
    simulation and compare it to ISS and the behavior of the physical system. We show
    that we can reach an increased accuracy of the simulation when we inject noise
    into the time model. Our results indicate that it is sufficient to inject uniformly
    distributed random time values to the RTOS real-time clock.
author:
- first_name: Henning
  full_name: Zabel, Henning
  last_name: Zabel
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
citation:
  ama: 'Zabel H, Müller W. Increased Accuracy through Noise Injection in Abstract
    RTOS Simulation. In: <i>Proceedings of DATE’09</i>. ; 2009. doi:<a href="https://doi.org/10.1109/DATE.2009.5090925">10.1109/DATE.2009.5090925</a>'
  apa: Zabel, H., &#38; Müller, W. (2009). Increased Accuracy through Noise Injection
    in Abstract RTOS Simulation. <i>Proceedings of DATE’09</i>. Design, Automation
    &#38; Test in Europe Conference &#38; Exhibition. <a href="https://doi.org/10.1109/DATE.2009.5090925">https://doi.org/10.1109/DATE.2009.5090925</a>
  bibtex: '@inproceedings{Zabel_Müller_2009, place={Nice, France}, title={Increased
    Accuracy through Noise Injection in Abstract RTOS Simulation}, DOI={<a href="https://doi.org/10.1109/DATE.2009.5090925">10.1109/DATE.2009.5090925</a>},
    booktitle={Proceedings of DATE’09}, author={Zabel, Henning and Müller, Wolfgang},
    year={2009} }'
  chicago: Zabel, Henning, and Wolfgang Müller. “Increased Accuracy through Noise
    Injection in Abstract RTOS Simulation.” In <i>Proceedings of DATE’09</i>. Nice,
    France, 2009. <a href="https://doi.org/10.1109/DATE.2009.5090925">https://doi.org/10.1109/DATE.2009.5090925</a>.
  ieee: 'H. Zabel and W. Müller, “Increased Accuracy through Noise Injection in Abstract
    RTOS Simulation,” presented at the Design, Automation &#38; Test in Europe Conference
    &#38; Exhibition, 2009, doi: <a href="https://doi.org/10.1109/DATE.2009.5090925">10.1109/DATE.2009.5090925</a>.'
  mla: Zabel, Henning, and Wolfgang Müller. “Increased Accuracy through Noise Injection
    in Abstract RTOS Simulation.” <i>Proceedings of DATE’09</i>, 2009, doi:<a href="https://doi.org/10.1109/DATE.2009.5090925">10.1109/DATE.2009.5090925</a>.
  short: 'H. Zabel, W. Müller, in: Proceedings of DATE’09, Nice, France, 2009.'
conference:
  name: Design, Automation & Test in Europe Conference & Exhibition
date_created: 2023-01-17T11:51:44Z
date_updated: 2023-01-17T11:51:48Z
department:
- _id: '672'
doi: 10.1109/DATE.2009.5090925
keyword:
- Timing
- Analytical models
- Clocks
- Performance analysis
- Scheduling
- Operating systems
- Delay
- Real time systems
- Application software
- Context modeling
language:
- iso: eng
place: Nice, France
publication: Proceedings of DATE'09
publication_identifier:
  isbn:
  - 978-1-4244-3781-8
status: public
title: Increased Accuracy through Noise Injection in Abstract RTOS Simulation
type: conference
user_id: '5786'
year: '2009'
...