With the prevalence of timing side channel attacks against software implementations of cryptographic algorithms, the constant time programming paradigm has received increased attention. Constant time programming demands that the execution of a program does not have any exploitable dependencies on secret data. However, implementing a program in such a fashion is not a simple task. In this paper, we propose UPEC-PN, a novel methodology for semi-automatically analyzing a given software binary and verifying its compliance with the constant time paradigm. The methodology is based on property checking and exhaustively checks all possible runs of the target software for security vulnerabilities due to violation of constant-time execution. To ensure scalability, we use program netlists, an ISA-level representation of the software as a combinational hardware circuit, as the underlying computational model. We use a 2-safety approach, instantiating the program netlist under test twice and perform interval property checking. The properties are formulated such that any counterexample shows an exploitable dependency on secret data. We conducted a case study on software implementations of the RSA and AES encryption algorithms compiled for the RISC-V ISA. In both studies, we were able to detect a number of possible side channels due to violation of constant time execution.
Processors require local memory close to the execution units to bridge the long latencies for accessing the comparatively slow main memory. In particular, traditional processor architectures use register files at the top of the memory hierarchy, and compilers focus on making efficient use of registers as an expensive and sparse resource. To further increase performance, processors exploit instruction level parallelism (ILP) of programs by hosting more and more execution units. However, the limited number of registers and access ports of the register file, together with current code generators, limit the use of ILP. Since increasing the number of registers and the number of read/write ports in the register file increases the circuit size prohibitively, first-in-first-out (FIFO) buffers have been proposed as a better scalable alternative local memory close to the execution units. In this paper, we outline two processor designs that use different types of buffers as local memories, and then prove experimentally that these buffers can be implemented as circuits whose size grows linearly with the buffer depth, while the circuit size of register files grows polynomially of at least degree two. We then discuss the linear (quasi-linear due to the interconnect network) scalability of these novel architectures that replace registers with buffers.
The development of chip generators instead of the development of individual chips is an important trend in digital design that is picking up momentum both in academia and industry. The reuse of IP generators has significant potential to increase productivity as the generators can be rerun without manual design work to generate different IPs, optimized for different applications and trade-off criteria. Two key limiting factors for the reuse of IP generators are the need to develop individual IP generators with SoC integration aspects in mind and the need for SoC generators to handle IP integration aspects of different generated IPs. This work proposes a generator architecture based on best-practice software architectural patterns that address these limitations. The proposed architecture allows IP generators to be developed independently from SoC integration aspects and enables communication and collaboration between generators to align on a common, optimal architecture. This also enables the development of SoC infrastructure generators that automatically generate suitable SoC infrastructure based on the information collected from the individual IP generators. The suggested architecture significantly simplifies the task of top-level integration and guarantees that existing generators can be reused in SoC contexts with different infrastructure properties.
Earliest deadline first (EDF) is a well-studied scheduling policy in real-time theory and is known to be optimal for certain task models. Nevertheless EDF is hardly used in practice. A possible reason is that EDF is not decisive for multiple, equal deadlines which can lead to a non-deterministic real-time scheduler. This means EDF has to be extended by a tie-breaking rule. However, the literature on response time analysis of EDF, such as Spuri and Palencia and Harbour, does not formalize such a tie-breaking rule. This can cause an overestimation of the worst-case response time. To address this, we present a new worst-case response time analysis for EDF with tie-breaking. The analysis is demonstrated on a real industrial case study. The results of the experiment show that the inclusion of a tie-breaking rule improves the estimation of worst-case response times for this case study by a factor of 12 on average in comparison to the method by Palencia and Harbour.
RISC-V has received worldwide acceptance in the industry and by the academic community. As of today, multiple RISC-V applications and variants are under investigation for embedded IoT systems, from resource-limited single-core processors up to multi-core systems for High-Performance Computing (HPC). Recently, the Grid of Processing Cells (GPC) platform has been proposed as a scalable parallel grid-oriented network of processor cores with local memories. This paper describes a prototype design of the GPC platform for hardware implementation at Register-Transfer Level (RTL) based on modified RISC-V Rocket processors with scratchpad memories. It introduces a scalable Chisel-based implementation of the modified Rocket cores with RTL generation and a functional test using Verilator simulation. This work also includes the adaptation of the Chipyard software toolchain to extend the compiler to multi-core grids with different local address spaces.
Large Deep Neural Networks (DNNs) are the backbone of today's artificial intelligence due to their ability to make accurate predictions when being trained on huge datasets. With advancing technologies, such as the Internet of Things, interpreting large quantities of data generated by sensors is becoming an increasingly important task. However, in many applications not only the predictive performance but also the energy consumption of deep learning models is of major interest. This paper investigates the efficient deployment of deep learning models on resource-constrained microcontroller architectures via network compression. We present a methodology for the systematic exploration of different DNN pruning, quantization, and deployment strategies, targeting different ARM Cortex-M based low-power systems. The exploration allows to analyze trade-offs between key metrics such as accuracy, memory consumption, execution time, and power consumption. We discuss experimental results on three different DNN architectures and show that we can compress them to below 10\% of their original parameter count before their predictive quality decreases. This also allows us to deploy and evaluate them on Cortex-M based microcontrollers.
SystemC-based Virtual Prototypes (VPs) at the Electronic System Level (ESL) are increasingly adopted by the semiconductor industry. The main reason is that VPs are much earlier available, and their simulation is orders of magnitude faster in comparison to the hardware models at lower levels of abstraction (e.g. RTL). This leads designers to use VPs as reference models for early design verification. Hence, the correctness of VPs is of utmost importance as undetected errors may propagate to less abstract levels in the design process, increasing the fixing cost and effort. In this paper, we introduce a comprehensive simulation-based verification approach to automatically validate the simulation behavior of a given SystemC-based VP against both the TLM-2.0 rules and its specifications, i.e. functional and timing behavior of communications in the VP.
With (PROGRESS) we present a fully automatic and complete approach for Hardware Model Checking under restrictions. We use the PROGRESS approach in the context of PDR/IC3 [9, 18]. Our implementation of PDR/IC3 restricts input signals as well as state bits of a circuit to constants in order to quickly explore long execution paths of the design. We are able to identify spurious proofs of safety along the way and exploit information from these proofs to guide the relaxation of the restrictions. Hence, we greatly improve the capability of PDR to find counterexamples, especially with long error paths. In experiments with HWMCC benchmarks our approach is able to double the amount of detected deep counterexamples in comparison to Bounded Model Checking as well as in comparison to PDR.
Second generation artificial intelligence (AI) migrates inference related computations from cloud towards edge devices [19]. Due to increasingly sophisticated neural network (NN) architecture search, even more complex applications come into range for execution on the edge. This enables a significant drop in latency, power consumption and bandwidth, since data transmission to cloud becomes obsolete. We address challenges to enable edge platforms with computation hardware capable of dealing with more complex applications locally. For NN inferences in general, dot product operation is the most commonly and intensively used. Thus, defining a proper unit supporting the mentioned operation in an efficient way has huge impact. Between different applications the network hyperparameters may change, including the data formats of kernels and activations. Therefor, supporting a wide variety of data formats with the dot product unit, while keeping the area increase low, seems appealing. Additionally, the computational load varies dependent on the particular application, thus a scalable solution is desireable. Next to the configurability and programmability, area as well as power efficiency plays an important role. We propose a scalable, configurable and programmable vector dot product unit, targeting an optimized footprint for low power applications to overcome the challenges of second generation AI on edge devices. The proposed solution is supported by a Python-based HW generator, which enables the derivation of featured dot product units optimized for certain applications. It is developed with the assumption to be utilized as a standalone component as well as loosely or closely coupled component associated with a CPU instruction set extension.
The limited number of globally visible registers restricts the use of instruction-level parallelism in conventional processors. Therefore, some recent architectures expose their internal datapaths so that the compiler can make use of instructions to transfer intermediate values directly between the processing units (PUs) of the processor. Buffered exposed datapath (BED) architectures additionally use first-in-first-out (FIFO) buffers on the communication paths between the PUs to avoid unnecessary synchronizations of the PUs. However, the number of communication paths, and hence, the number of FIFO buffers in a BED architecture, grows quadratically with the number of PUs which may become prohibitive for architectures with many PUs. In this paper, we therefore propose the use of virtual buffers for BED architectures in analogy to virtual channels in networks on chips (NoCs). In particular, we present an implementation of many virtual FIFO buffers with a single combined buffer so that each PU has only a constant number of combined buffers instead of a number of virtual buffers that grows linearly with the number of PUs. Moreover, the circuit size of the combined buffers grows only linearly with their size that we can determine independently of the number of PUs. Hence, using virtual/combined buffers, we can implement BED architectures with a circuit size that scales only quasi-linearly (due to the interconnection network) with the number of PUs and the size of the combined buffers.
In recent years, several formal verification methods based on Symbolic Computer Algebra (SCA) have been proposed to verify complex multipliers. Despite this progress, the complexity of these methods is usually unknown. It raises serious questions regarding the scalability of SCA-based approaches. In this paper, we propose a verification method based on SCA and Binary Decision Diagrams (BDDs) to guarantee the polynomial formal verification of complex multipliers.
During the last years, software model checking has become a reliable technique for the verification of software that is used in safety-critical environments – e.g. to prove the absence of dead code. One technique to perform such proofs is k-induction which considers in its induction step the property and transition relation but ignores the initial states. Therefore, k-induction is very sensitive regarding the encoding of variables which have a constant value – in particular if the encoding depends on the initial states. A recent bachelor thesis addresses this problem. In this paper, we present the main results, describe the integration into the commercial test and verification tool BTC EmbeddedPlatform(r) and evaluate our implementation on a benchmark set with verification tasks originating from the automotive domain.
This work builds upon our model-based synthesis framework for the automatic generation of parallel software from dataflow process networks (DPNs). Our DPNs are described in the RVC-CAL language and our synthesis method employs a two-level scheduling scheme: At the first level, the global scheduler decides which actor executes next, and at the second level, the local scheduler determines which action of the scheduled actor executes next. The global scheduler works thereby in a round-robin fashion and selects the next idle actor without pending calls from the list of actors. In this paper, we propose a data-aware as-soon-as-possible (ASAP) scheduling scheme to modify the global scheduler with the aim to improve the end-to-end performance: First, a data-aware scheme is employed that prevents the global scheduler to redundantly test the source actors if the required data tokens for the desired computation are produced. Second, the scheduler is modified with an ASAP scheme that in contrast to a classical round-robin approach tests actors for scheduling in parallel. Based on our experimental evaluation, the proposed modifications demonstrated a speedup by a factor of up to 12 compared to the previous version.
Albeit an important and versatile model for many practical applications, partially observable Markov Decision Processes (POMDPs) are notoriously hard to analyze. Many interesting properties are either of high complexity or even theoretically undecidable, and while approximative methods often provide good results for, e. g., policy synthesis and the computation of probabilities, other problems remain still unsolved. One such issue is diagnosis – figuring out why a certain specification cannot be met, and what can be done to repair the system. While in deterministic systems like digital circuits, a single execution trace is a sufficient proof of an unsafe system, the situation is less easy in probabilistic systems – typically large sets of traces are required whose joint probability exceeds a maximally tolerable probability. For POMDPs, the restricted observability adds another layer of uncertainty. In this paper we focus on analyzing where the restricted observability needs to be refined in order to satisfy a required safety or performance property. We propose and evaluate different approaches for obtaining such diagnostic information.
Resilience against hardware faults is a major concern for safety-critical embedded systems which has been addressed in several standards. These standards demand a systematic and thorough safety evaluation, especially for the highest safety levels. In order to provide the data for this evaluation, we propose a scalable and formal approach to fault propagation analysis for hardware/software systems. We consider soft errors by single event upsets (SEUs) which corrupt data in hardware registers and examine their effect on the high-level software. Our method identifies all faults of a given fault list that can have an effect on selected objects of the high-level software, such as the specified safety functions, and gives formal guarantees for other faults that do not do any harm.Scalability of our approach results from combining an analysis at the binary and hardware level with an analysis of the high-level source code using Abstract Interpretation. The result is a mapping between a fault in the hardware and affected locations in the source code. Effectiveness and scalability of this method are demonstrated on an industry-oriented software system with about 138 k lines of C code.
RISC-V is a modern open and free Instruction Set Architecture (ISA) that is designed in a very modular way and enables to integrate custom instruction extensions in order to build highly application specific solutions. Extensive verification and validation is crucial to ensure that the design meets all requirements from the specification. Constrained Random Verification (CRV) has been shown to be a very effective technique for this purpose. RISC-V DV is a powerful CRV framework that is tailored for RISC-V and under active development by Google. In this paper we provide an overview, evaluation and discussion of CRV for RISC-V, based on the RISC-V DV framework. In our evaluation we assess the bug hunting capabilities of RISC-V DV by means of mutation samples and we provide additional execution metrics for the framework. Moreover, we add a discussion on the approach and sketch ideas for future research directions in this area to further boost the approach.
As various domain knowledge is prerequired, the embedded systems development is difficult. In the development process, multiple programming languages are used to develop different aspects such as hardware, firmware and formal verification. The semantic gap and inconsistent syntax among these languages escalate further the design efforts. We propose to generate Python-embedded Self-Verifying Domain-Specific Languages (DSLs) from metamodels. Domainspecific semantics are captured in metamodels. With additional configurations, domain-specific functionalities are included in DSLs. Further, tests are generated to assure the DSL quality. To demonstrate the applicability, the proposed approach is applied on an embedded system automation framework that generates hardware, firmware and formal properties for verification. An SoC was generated and verified with the automation framework. Minimal efforts were observed to achieve high code coverage for DSLs. Furthermore, our approach scales well with increasing domain complexity, i.e., the generation took less than 10 seconds for the most complex DSL (129.9k Lines of Code).
We give an overview of the language APPEL, the “AGILA Property and Dependency Description Language”. It is part of the cloud-based tool AGILA that supports agile development methods. The language allows us to structure and document the knowledge about system-wide dependencies in a formal, textual form. APPEL models can be uploaded to the cloud, where they are used as a knowledge-base for continuous verification and validation, from early specification to run-time verification. We describe syntax, semantics, and demonstrate its application for predicting the performance of hardware/software systems in the context of the GENIAL! project.
Fault simulation is a technique used to evaluate the robustness of safety-critical systems. An objective of the technique is to inject faults into a system and to observe its behavior. To deal with the large and complex designs, fast and valid fault simulation techniques are highly demanded. For this purpose fault simulators are used. Fault simulators are software programs that facilitate fault injection on a design model and capture the responses of a design for different fault types. This paper explores methods for extending a hardware simulator with fault injection capability. We consider Verilator, an open source hardware simulator, for fault simulation of complex designs. Towards this end, we extend Verilator with fault injection capability. Verilator’s high performance combined with the added functionality for fault modeling provides accurate and fast results to measure the dependability and robustness of designs. To evaluate and validate the approach, different fault models were injected into several designs. The experimental results show an average slowdown of 23% of the simulator runtime. Furthermore, the technique was used to evaluate the dependability of an SoC with a safety related software flow monitoring algorithm.
Fault coverage analysis and fault simulation are well-established methods for the qualification of test vectors in hardware design. However, their role in virtual prototyping and the correlation to later steps in the design process need further investigation. We introduce a metric for RISC-V instruction and register coverage for binary software. The metric measures if RISC-V instruction types are executed and if GPRs, CSRs, and FPRs are accessed. The analysis is applied by the means of a virtual prototype which is based on an abstract instruction and register model with direct correspondence to their bit level representation. In this context, we analyzed three different openly available test suites: the RISC-V architectural testing framework, the RISC-V unit tests, and programs which are automatically generated by the RISC-V Torture test generator. We discuss their tradeoffs and show that by combining them to a unified test suite we can arrive at a 100% GPR and FPR register coverage and a 98.7% instruction type coverage.
