[{"_id":"36994","language":[{"iso":"eng"}],"publisher":"IEEE","user_id":"5786","doi":"10.1109/SOCC.2012.6398362","status":"public","year":"2012","title":"Mutation-Analysis Driven Functional Verification of a Soft Microprocessor","author":[{"first_name":"Tao ","last_name":"Xie","full_name":"Xie, Tao "},{"first_name":"Wolfgang","last_name":"Müller","full_name":"Müller, Wolfgang","id":"16243"},{"last_name":"Letombe","first_name":"Florian","full_name":"Letombe, Florian"}],"publication_identifier":{"eisbn":["978-1-4673-1295-0"]},"date_updated":"2023-01-17T08:46:29Z","date_created":"2023-01-17T08:46:14Z","place":" Niagara Falls, NY, USA ","type":"conference","keyword":["Analytical models","Hardware design languages","Microprocessors","Cost function","Data models","Search problems","IP networks"],"department":[{"_id":"672"}],"publication":"Proceedings of SOCC2012","citation":{"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>.","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} }","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>","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>.","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>","short":"T. Xie, W. Müller, F. Letombe, in: Proceedings of SOCC2012, IEEE,  Niagara Falls, NY, USA , 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>."},"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."}]},{"publication_identifier":{"isbn":["978-1-4577-1048-3"]},"author":[{"full_name":"Xie, Tao","last_name":"Xie","first_name":"Tao"},{"id":"16243","full_name":"Müller, Wolfgang","first_name":"Wolfgang","last_name":"Müller"},{"full_name":"Letombe, Florian","last_name":"Letombe","first_name":"Florian"}],"status":"public","year":"2011","title":"HDL-Mutation Based Simulation Data Generation by Propagation Guided Search","date_updated":"2025-02-26T14:44:15Z","publisher":"IEEE","_id":"37002","language":[{"iso":"eng"}],"user_id":"5786","doi":"10.1109/DSD.2011.83","citation":{"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>.","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} }","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>","short":"T. Xie, W. Müller, F. Letombe, in: Proceedings of Euromicro DSD 2011, IEEE, Oulu, Finnland, 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>."},"publication":"Proceedings of Euromicro DSD 2011","abstract":[{"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.","lang":"eng"}],"date_created":"2023-01-17T09:02:48Z","place":"Oulu, Finnland","department":[{"_id":"672"}],"keyword":["Hardware design languages","Cost function","Computational modeling","Fault detection","Data models","Analytical models","Testing"],"type":"conference"},{"user_id":"5786","doi":"10.1109/DATE.2010.5457130","publisher":"IEEE","_id":"37009","language":[{"iso":"eng"}],"date_updated":"2023-01-17T09:15:18Z","year":"2010","status":"public","title":"Assertion-Based Verification of RTOS Properties","author":[{"last_name":"Oliveira","first_name":"Marcio F. S.","full_name":"Oliveira, Marcio F. S."},{"first_name":"Henning","last_name":"Zabel","full_name":"Zabel, Henning"},{"id":"16243","full_name":"Müller, Wolfgang","last_name":"Müller","first_name":"Wolfgang"}],"conference":{"name":"2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)","location":"Dresden"},"type":"conference","keyword":["Operating systems","Real time systems","Timing","Hardware","Analytical models","Embedded software","Software systems","Processor scheduling","Software performance","Performance analysis"],"department":[{"_id":"672"}],"date_created":"2023-01-17T09:15:10Z","place":"Dresden","abstract":[{"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.","lang":"eng"}],"publication":"Proceedings of DATE’10","citation":{"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} }","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>","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.","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>.","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>"}},{"status":"public","title":"Increased Accuracy through Noise Injection in Abstract RTOS Simulation","year":"2009","publication_identifier":{"isbn":["978-1-4244-3781-8"]},"author":[{"full_name":"Zabel, Henning","last_name":"Zabel","first_name":"Henning"},{"full_name":"Müller, Wolfgang","last_name":"Müller","first_name":"Wolfgang","id":"16243"}],"conference":{"name":"Design, Automation & Test in Europe Conference & Exhibition"},"date_updated":"2023-01-17T11:51:48Z","language":[{"iso":"eng"}],"_id":"37066","user_id":"5786","doi":"10.1109/DATE.2009.5090925","publication":"Proceedings of DATE'09","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>","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} }","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>.","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>.","short":"H. Zabel, W. Müller, in: Proceedings of DATE’09, Nice, France, 2009.","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>","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>."},"abstract":[{"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.","lang":"eng"}],"date_created":"2023-01-17T11:51:44Z","place":"Nice, France","type":"conference","keyword":["Timing","Analytical models","Clocks","Performance analysis","Scheduling","Operating systems","Delay","Real time systems","Application software","Context modeling"],"department":[{"_id":"672"}]}]