Design and Assertion Based Verification of RISC-V Processor Subsystems

RISC-V is an open, free standard architecture. As its open-source architecture, it can be used in multiple applications like embedded processors, IoT, artificial intelligence, machine learning, military and defense applications. The parameters like throughput, performance, high speed etc., become essential in designing processor architecture. Pipelining is one such unique feature supported by RISC-V ISA, which basically involves the execution of multiple instructions in single cycle. This feature helps in improving the performance of the processor architecture. RISC-V ISA supports five stages of pipelining they are instruction fetch, instruction decode, execute, memory and write-back stage. The work covered in this paper involves the design and implementation of the subsystems of the RISC-V ISA which are present in different stages of pipeline architecture. The subsystems included in this work are Floating Point Unit (FPU) of Execute stage, Branch Prediction Unit (BPU) of instruction fetch stage, Forwarding Unit of execution stage, Operand Logic of decode stage and Floating-Point register file of Write-back stage. These subsystems are designed using Verilog Hardware Description Language in Xilinx ISE. Followed by the implementation the verification of the floating-point unit and the forwarding unit is performed using System Verilog Assertions in QuestaSim. The Assertion coverage report for the same is extracted.

Lightweight Microcontroller with Parallelized ECC-Based Code Memory Protection Unit for Robust Instruction Execution in Smart Sensors

Embedded systems typically operate in harsh environments, such as where there is external shock, insufficient power, or an obsolete sensor after the replacement cycle. Despite these harsh environments, embedded systems require data integrity for accurate operation. Unintended data changes can cause a serious error in reduced instruction set computer (RISC)-based small embedded systems. For instance, if communication is performed on an edge, where there is insufficient power supply, the peak threshold is not reached, resulting in data transmission failure or incorrect data transmission. To ensure data integrity, we use an error-correcting code (ECC), which can detect and correct errors. The ECC parity bit and data are stored together using additional ECC memory, and the original data are extracted through the ECC decoding process. The process of extracting the original data is executed in the instruction fetch stage, where a bottleneck appears in the RISC-based structure. When the ECC decoding process is executed in the bottleneck, the instruction fetch stage increases the instruction fetch time and significantly reduces the overall performance. In this study, we attempt to minimize the effect of ECC on the transmission speed by executing the ECC decoding process in parallel to improve speed by degrading the bottleneck. To evaluate the performance of a parallelized ECC decoding block, we applied the proposed method to the tiny processing unit (TPU) with a RISC-based von Neumann structure and compared memory usage, speed, and reliability according to different transmission success rates in each model. The experiment was conducted using a benchmark that repeatedly executed several 3*3 matrix calculations, and reliability improvement was compared by corrupting the stored random date to confirm the reliability of the transmission success rate. As a result, in the proposed model, using the additional parity bits for parallel processing, memory usage increased by 10 bits per instruction, reducing the data rate from 80 to 61%. However, it showed an improvement in overall reliability and a 7% increase in speed.

Memory and Cache Contention Denial-of-Service Attack in Mobile Edge Devices

In this paper, we introduce a memory and cache contention denial-of-service attack and its hardware-based countermeasure. Our attack can significantly degrade the performance of the benign programs by hindering the shared resource accesses of the benign programs. It can be achieved by a simple C-based malicious code while degrading the performance of the benign programs by 47.6% on average. As another side-effect, our attack also leads to greater energy consumption of the system by 2.1× on average, which may cause shorter battery life in the mobile edge devices. We also propose detection and mitigation techniques for thwarting our attack. By analyzing L1 data cache miss request patterns, we effectively detect the malicious program for the memory and cache contention denial-of-service attack. For mitigation, we propose using instruction fetch width throttling techniques to restrict the malicious accesses to the shared resources. When employing our malicious program detection with the instruction fetch width throttling technique, we recover the system performance and energy by 92.4% and 94.7%, respectively, which means that the adverse impacts from the malicious programs are almost removed.

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models

Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g. 100k+ lines for Armv8-A. In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in Sail, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications, which should be valuable also for other verification tasks. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V. By using full-scale and authoritative ISA semantics, this lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of systems functionality, as used by hypervisors and operating systems, e.g. instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch model and self-modifying code examples of Simner et al.

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and “user-mode” concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g. in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g. with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on “user-mode” concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.

PENINGKATAN PERFORMANSI PROSESOR DLX DENGAN METODE PIPELINE

Prosesor DLX adalah sebuah prosesor berbasis RISC (Reduced Instruction Set Computer) yang dirancang sebagai prosesor tujuan umum (general purpose processor). Prosesor ini mempunyai arsitektur load-store dengan panjang semua instruksinya 32 bit. Setiap instruksi dieksekusi dalam beberapa siklus waktu (cycletime). Secara umum time cycle yang digunakan sebanyak lima tahap yang terdiri dari tahap-tahap : Instruction Fetch (IF), Instruction Decode (ID), Execute (EX), Memory Access (MEM), dan Write Back (WB). Kelima tahap ini dikerjakan secara berurutan [2]. Sebagai prosesor multicycle, DLX mempunyai peluang untuk meningkatkan kinerjanya yang diukur dengan kecepatan proses yang dinyatkan sebagai waktu CPU (CPU time). Peningkatan kinerja prosesor DLX dapat diterapkan dengan menggunakan teknik pipeline. Pada jurnal ini telah dianalisis peningkatan performansi prosesor DLX dengan menggunakan teknik pipeline. Uji coba dilakukan terhadap beberapa program aplikasi yang dieksekusi dengan menggunakan teknik pipeline dan tanpa menggunakan teknik pipeline. Secara umum terjadi peningkatan kecepatan pada setiap kumpulan instruksi yang dianalisis. Proses pengujian dilakukan dengan menggunakan simulator windlx yang merupakan simulator prosesor DLX.Kata kunci : Prosesor DLX, RISC, general purpose processor, CPU, Pipeline, windlx