Software-Based Self-Tests (SBST) allow for at-speed testing of on-chip devices via a processor core. However, creating SBSTs requires time-consuming manual labour that is expensive and requires in-depth knowledge of the device’s architecture for targeting hard-to-test faults. Introducing cell-aware testing to this task further exacerbates the necessary effort. In contrast, automating the complex parts of SBST generation using Bounded Model Checking (BMC) allows using sophisticated, state-of-theart BMC solvers to automatically generate vast parts of the SBST. Thereby, a virtual circuit called Validity Checker Module (VCM) is used to encode constraints for the SBST. In this paper, we focus on generating a cell-aware SBST for a Core Local Interrupt Controller (CLIC) that is executed via a RISC-V processor core. We first d erive a constraint s et that creates SBST-like conditions during ATPG, which allows for transformation into instructions later on. We implement a cellaware test model via a re-entrant Mealy state machine that allows complex behaviors of the faulty cell. Experimentally, we extend the CLIC with a test interface that is controlled via a custom CSR of the processor core to reduce SBST generation time and enhance fault coverage. We conclude with the evaluation of our approach on the PULP CLIC implementation that shows cellaware SBST generation to be feasible while achieving acceptable fault coverages and practical generation runtimes.

Graphics Processing Units (GPUs) are becoming widespread, even in safety-critical applications. In that case, it is imperative to guarantee that the probability of producing critical failures due to hardware faults is lower than a given threshold. To detect possible permanent hardware faults as soon as they appear during the operational phase (e.g., due to aging), Software Test Libraries (STLs) have gained significant traction as a widely adopted test solution due to their effectiveness in terms of fault detection capabilities, test application time, and flexibility. However, a major drawback of this solution is the lack of automation in the STL generation phase. As a result, high manual labor is required for their generation. This becomes even more arduous in complex architectures that require in-depth knowledge to cover hard-to-test faults. In this article, we introduce a methodology based on Bounded Model Checking to support the generation and improvement of stuck-at-oriented STLs for hard-to-test units in GPUs, showing that we can enhance the test coverage achieved by pre-existing STLs while also identifying a set of functionally untestable faults. To experimentally validate the proposed method’s effectiveness, we use the FlexGripPlus GPU model to target two hard-to-test units, one medium to low complexity sub-unit and one high complexity sub-unit, as study cases. For both units, we had pre-existing STLs written for the stuck-at model. Resorting to the proposed method, the STLs’ test coverage was increased by 9.57% and 2.19%, respectively. In addition, the method also identified a significant number of functionally untestable faults.

We revisit the topic of generalizing proof obligations in bit-level Property Directed Reachability (PDR). We provide a comprehensive study which determines the complexity of the problem, thoroughly analyzes limitations of existing methods, introduces approaches to proof obligation generalization that have never been used in the context of PDR, compares the strengths of different methods from a theoretical point of view, and intensively evaluates the methods on various benchmarks from Hardware Model Checking as well as from AI Planning.

The synthesis problem for partially observable Markov decision processes (POMDPs) is to compute a policy that provably adheres to one or more specifications. Yet, the general problem is undecidable, and policies require full (and thus potentially unbounded) traces of execution history. To provide good approximations of such policies, POMDP agents often employ randomization over action choices. We consider the problem of computing simpler policies for POMDPs, and provide several approaches to still ensure their expressiveness. Key aspects are (1) the combination of an arbitrary number of specifications the policies need to adhere to, (2) a restricted form of randomization, and (3) a light-weight preprocessing of the POMDP model to encode memory. We provide a novel encoding as a mixed-integer linear program as baseline to solve the underlying problems. Our experiments demonstrate that the policies we obtain are more robust, smaller, and easier to implement for an engineer than those obtained from state-of-the-art POMDP solvers.

With the continued success of the open RISC-V architecture, practical deployment of RISC-V processors necessitates an in-depth consideration of their testability, safety and security aspects. This survey provides an overview of recent developments in this quickly-evolving field. We start with discussing the application of state-of-the-art functional and system-level test solutions to RISC-V processors. Then, we discuss the use of RISC-V processors for safety-related applications; to this end, we outline the essential techniques necessary to obtain safety both in the functional and in the timing domain and review recent processor designs with safety features. Finally, we survey the different aspects of security with respect to RISC-V implementations and discuss the relationship between cryptographic protocols and primitives on the one hand and the RISC-V processor architecture and hardware implementation on the other. We also comment on the role of a RISC-V processor for system security and its resilience against side-channel attacks.

In this article, we revisit the topic of generalizing proof obligations (POs) in bit-level property directed reachability (PDR). We provide a comprehensive study which: 1) determines the complexity of the problem; 2) thoroughly analyzes limitations of existing methods; 3) introduces approaches to PO generalization that have never been used in the context of PDR; 4) compares the strengths of different methods from a theoretical point of view; and 5) intensively evaluates the methods on various benchmarks from the hardware model checking as well as from AI planning.

Abstract It is well-established that party identity biases the processing of political information and the evaluation of political actors. This is presumed to avoid cognitive dissonance and achieve positive affect. What happens, however, when individuals diverge from this pattern and do make identity-inconsistent evaluations of political actors – how does this translate into positive and negative emotions toward the candidates? The paper addresses this question using large-N data from the main televised debate of the 2017 German national election by combining survey responses with viewer perceptions measured during the debate. The findings suggest that candidate ratings made during the debate have different valence depending on a person’s party identity. Strikingly, a stronger party identity does not mean a reduced impact of identity-inconsistent evaluations on emotional responses toward a candidate. Rather, only evaluations in accordance with one’s party identity, and hence with lower information value, show a reduced effect on emotional responses.

The shift towards advanced electricity metering infrastructure gained traction because of several smart meter roll-outs during the last decade. This increased the interest in Non-Intrusive Load Monitoring. Nevertheless, adoption is low, not least because the algorithms cannot simply be integrated into the existing smart meters due to the resource constraints of the embedded systems. We evaluated 27. features and four classifiers regarding their suitability for event-based NILM in a standalone and combined feature analysis. Active power was found to be the best scalar and WaveForm Approximation the best multidimensional feature. We propose the feature set [ P,cos ,TRI,WFA] in combination with a Random Forest classifier. Together, these lead to F_1 -scores of up to 0.98 on average across four publicly available datasets. Still, feature extraction and classification remains computationally lightweight and allows processing on resource constrained embedded systems.

Graphics Processing Units (GPUs) boost the development of high-performance safety-critical applications. The reliability of such systems is of utmost importance since faults affecting the hardware may occur at any time during the systems' operational life. Thus, methods to effectively test these devices during their in-field operation are necessary. One popular solution relies on Software Test Libraries (STLs), which recently have been started being used for GPUs as well, since they are effective in terms of fault detection capabilities, intrusiveness, flexibility, and test duration. A drawback of the STL approach for GPUs is the extensive effort used to develop effective test routines for complex structures, e.g., controllers, due to the complicated constraints stemming from the ISA, the available compilation flows and parallelism constraints. We propose a novel technique based on formal methods to support the generation of stimuli and enhance the quality of pre-existing STLs for GPUs. To validate the proposed method, we resort to an open-source GPU model (FlexGripPlus). Experimental results show that the method can effectively generate complementary code fragments to be added to existing STLs and increase their fault coverage. In the case of the GPU's decoding unit, the stuck-at fault coverage was increased by nearly 10%.

This paper introduces the project Scale4Edge. The project is focused on enabling an effective RISC-V ecosystem for optimization of edge applications. We describe the basic components of this ecosystem and introduce the envisioned demonstrators, which will be used in their evaluation.

In several test and reliability problems (from test generation to FMECA and Burn In) it is important to preliminarily identify those lines in a circuit netlist, which can not be controlled, i.e., can not be toggled to both logic values no matter the applied stimuli. Several techniques have been proposed in the past to attack this problem. In this paper we consider the case where the circuit is a pipelined processor, discuss the specific challenges of this scenario and propose some techniques to automatically identify some of the uncontrollable lines. The approach we devised uses SAT solving as underlying technology. We report the results we gathered on the OR1200 processor, showing that our method allows to trade off between the required computational effort and the achieved results. When compared with results produced by a commercial tool, our approach is able to identify a much higher number of uncontrollable lines with reasonable computational requirements.

If embedded systems are used in safety-critical environments, they need to meet several standards. For example, in the automotive domain the ISO 26262 standard requires that the software running on such systems does not contain unreachable code. Software model checking is one effective approach to automatically detect such dead code. Being used in a commercial product, iSAT3 already performs very well in this context. In this paper we integrate IC3 into iSAT3 in order to improve its dead code detection capabilities even further.

The increasing amount and diversity of System-On-a-Chip (SoC) devices with short development times pose numerous challenges. The RISC-V initiative targets this market with a free and open ISA that supports custom instruction set extensions and accelerators to adapt to application specific scenarios and meet varying constraints w.r.t. efficiency, security, safety and computational power. In this context we target an appropriate test strategy to find manufacturing defects during production, and moreover, to detect degradation in the field. An essential part of this strategy will be so-called Software-Based Self-Tests (SBST). Manually developing SBST programs is a tedious and time-consuming task that requires the expertise of a skilled engineer with detailed knowledge about the specific architecture of the processor at hand. In contrast we present a staggered SBST approach for the automatic creation of SBST programs for RISC-V architectures with the help of SAT-based test pattern generation. First experimental results to demonstrate the feasibility of our approach are provided by test generation results for two exemplary RISC-V processor, each in two variants.

In order to reduce the electricity consumption in our homes, a first step is to make the user aware of it. Raising such awareness, however, demands to pinpoint users of specific appliances that unnecessarily consume electricity. A retrofittable and scalable way to provide appliance-specific consumption is provided by Non-Intrusive Load Monitoring methods. These methods use a single electricity meter to record the aggregated consumption of all appliances and disaggregate it into the consumption of each individual appliance using advanced algorithms usually utilizing machine-learning approaches. Since these approaches are often supervised, labelled ground-truth data need to be collected in advance. Labeling on-phases of devices is already a tedious process, but, if further information about internal device states is required (e.g., intensity of an HVAC), manual post-processing quickly becomes infeasible. We propose a novel data collection and labeling framework for Non-Intrusive Load Monitoring. The framework is comprised of the hardware and software required to record and (semi-automatically) label the data. The hardware setup includes a smart-meter device to record aggregated consumption data and multiple socket meters to record appliance level data. Labeling is performed in a semi-automatic post-processing step guided by a graphical user interface, which reduced the labeling effort by 72% compared to a manual approach. We evaluated our framework and present the FIRED dataset. The dataset features uninterrupted, time synced aggregated, and individual device voltage and current waveforms with distinct state transition labels for a total of 101 days.

ZusammenfassungKönnen virtualisierte Erhebungen rezeptionsbegleitend gemessener Kandidatenbewertungen in Echtzeit über das Internet valide und reliable Daten generieren? Seitdem Reinemann et al. vor 15 Jahren die Reliabilität und Validität von sogenannten Real-Time-Response-Messungen (RTR) mit physischen Eingabegeräten in laborexperimentellen Erhebungssettings in dieser Zeitschrift belegt haben, hat die Messtechnik eine weitreichende Veränderung erfahren, die durch die Virtualisierung ihres Instrumentariums gekennzeichnet ist. Allerdings liegen bislang kaum methodologische Erkenntnisse über den grundlegenden Wandel dieser Schlüsseltechnik vor. Der hier vorliegende Beitrag untersucht deshalb anhand von drei Fernsehduellen zu Landtagswahlen in Deutschland, inwiefern Daten, die mit einem virtualisierten Messinstrument der RTR-Messung in einer Feldstudie erhoben wurden, etablierten Standards der Datenqualität entsprechen. In unserer Analyse finden wir deutliche Belege für die Validität des Messverfahrens. Darüber hinaus zeigt unser Beitrag, dass diese neuartige Form der Erhebung von Echtzeitreaktionen reliable Daten mit einer hohen internen Konsistenz generieren kann, wenngleich die Befunde in Teilen ambivalent bleiben. Wir schlussfolgern, dass die Virtualisierung des RTR-Messinstrumentariums einen komplementären Ansatz zu den dominierenden Erhebungen mit laborexperimentellen Forschungsdesigns etabliert, wodurch die Analyse von Publikumsreaktionen auf landespolitische TV-Duelle in natürlichen Rezeptionssituationen zugänglich und die technische Implementierung von RTR-Studien über das Internet auch in Zeiten der COVID-19-Pandemie gewährleistet wird.

Abstract When real-time response data from viewers of a televised debate is collected via the internet, the server timestamps of the received responses may not match the correct times of the debate. This paper addresses the question of how the data could be aligned in retrospect, using an algorithm that approximates the playout delay difference between each viewer’s TV signal. The validity is shown by successfully approximating distinctive delays for viewers with satellite or cable TV.

Modern competitive solvers employ various preprocessing techniques to efficiently tackle complex problems. This work introduces two preprocessing techniques to improve solving weighted partial MaxSAT problems: Generalized Boolean Multilevel Optimization (GBMO) and Trimming MaxSAT (TrimMaxSAT). GBMO refines and extends Boolean Multilevel Optimization (BMO), thereby splitting instances due to their distribution of weights into multiple less complex subproblems, which are solved one after the other to obtain the overall solution. The second technique, TrimMaxSAT, finds unsatisfiable soft clauses and removes them from the instance. This reduces the complexity of the MaxSAT instance and works especially well in combination with GBMO. The proposed algorithm works incrementally in a binary search fashion, testing the satisfiability of every soft clause. Furthermore, as a by-product, typically an initial weight close to the maximum is found, which is in turn advantageous w.r.t. the size of e.g. the Dynamic Polynomial Watchdog (DPW) encoding. Both techniques can be used by all MaxSAT solvers, though our focus lies on Pseudo Boolean constraint based MaxSAT solvers. Experimental results show the effectiveness of both techniques on a large set of benchmarks from a hardware security application and from the 2019 MaxSAT Evaluation. In particular for the hardest of the application benchmarks, the solver Pacose with GBMO and TrimMaxSAT performs best compared to the MaxSAT Evaluation solvers of 2019. For the benchmarks of the 2019 MaxSAT Evaluation, we show that with the proposed techniques the top solver combination solves significantly more instances.

Using embedded systems in safety-critical environments requires a rigorous testing of the components these systems are composed of. For example, the software running on such a system has to be evaluated regarding its code coverage – in particular, unreachable code fragments have to be avoided according to the ISO 26262 standard. Software model checking allows to detect such dead code automatically. While the recent case study compares several academic software model checkers with the commercial test and verification tool BTC EmbeddedPlatform (Registered Trade Mark) (BTC EP), we want to focus on a lower level – i.e. the back-end solvers within BTC EP. Therefore, we evaluate the performance of off-the-shelf SMT solvers supporting the theory of floating-point as well as the theory of bitvectors on floating-point dominated benchmark instances originating from the automotive domain. Furthermore, we compare these off-the-shelf SMT solvers with the back-end solvers used by BTC EP.

The growing request for eco-feedback and smart living concepts accelerated the development of Non-Intrusive Load Monitoring (NILM) algorithms during the last decade. Comparing and evaluating these algorithms still remains challenging due to the absence of a common benchmark datasets, and missing best practises for their application. Despite the fact that multiple datasets were recorded for the purpose of comparing NILM algorithms, many researchers still have to record their own dataset in order to meet the requirements of their specific application. Adding ground truth labels to these datasets is a cumbersome and time consuming process as it requires an expert to visually inspect all the data manually. Therefore, we propose the Annoticity inspection and labeling tool which simplifies the process of visualizing and labeling of electricity data. We use an event detector based on the log likelihood ratio test which achieved an F1 score of 90.07 % in our experiments. Preliminary results indicate that the effort of generating event labels is reduced by 80.35 % using our tool.

Reconfigurable Scan Networks (RSNs) allow flexible access to embedded instruments for post-silicon validation and debug or diagnosis. However, the increased observability and controllability can be exploited by an attacker to manipulate or read out sensitive data, if no adequate precautions are taken by the designer. For large RSNs taking those precautions without algorithmic support is virtually impossible. This work proposes a method to automatically generate “minimal witnesses” demonstrating security weaknesses w.r.t. data flow in RSNs. The method provides condensed information to the designer on how to prevent data flow attacks, e.g. by locally modifying the RSN or by preventing active scan paths which contain those minimal witnesses. Experimental results confirm the applicability of the proposed method to diverse benchmark sets, including large designs. Additionally, the benefit of generating “minimal witnesses” for security weaknesses is shown.