We present the compilation process of synthesizable, transaction-level hardware designs into Gallina code. This allows the Coq theorem prover to execute formal verification scripts on top of the automatically generated code to prove individual theorems. The novelty of this work is the use of PDVL (Programming Design and Verification Language), which adds specific language constructs to System Verilog to enable an aspect-oriented, transaction-level design style. In this paper, we show that PDVL code can also be compiled into Gallina code, with the advantage that it is highly usable for theorem proving and perfect for using the Coq proof assistant. We outline individual proof strategies for theorem proving, sequential equivalence checking, property checking, and show applications of symbolic simulation techniques. This is done by using a complex timer peripheral, AES and UART modules as well as RISC-V based designs.

We demonstrate how dynamic verification (e.g. simulation) can be replaced by deductive formal verification and how to benefit from the advantages of symbolic verification and the reuse of verification proofs. To do this, we swap the well-known module-hierarchy based concept with a transaction-level (TL) based alternative, which still allows us to describe the design as precisely as on RTL. We enhance the aspect-oriented and TL oriented language PDVL to support the definition of functional coverage (FC) and assertions at all levels of a TL-hierarchy.We then show how to use a deductive formal verification (DFV) flow which compiles PDVL code into Gallina code to be used by the Coq theorem prover. It can be argued that FC can be converted into proof obligations and that proving them is equivalent to 100% coverage. We also demonstrate how lower-level proofs can be reused when verifying aspects at higher-levels of a TL-hierarchy. We argue that the traditional assertion-based verification (ABV) methodology is still supported and SVA can be proven using DFV.

With increasing aging problems of advanced technologies, in-field testing becomes an inevitable challenge, on top of the already demanding requirements, such as the ISO26262 for automotive safety. SOCs used in space, automotive or military applications in particular are worst affected as the in-field failures in these applications could even be life threatening. We focus on on-line and in-field testing for Single Event Upsets (SEU, caused by a single ionizing particle) and aging defects (such as delay variation and stuck-at faults) which may appear during normal operation of the device. Interrupting normal operations for aging defects testing is a major challenge for the OS. Additionally, checkpointing with rollback-recovery can be costly and mission critical data can be lost in case of an SEU event. We eliminate many of these problems with our non-interfering in-field testing and recovery solution.We apply a hardware performance improvement technique called System Hyper Pipelining (SHP), which combines well-known context switching (Barrel CPU) and C-slow retiming techniques. The SoC is enhanced with an SEU detection and ultra-fast recovery mechanism. We also use an RTL ATPG framework that enables the generation of software-based self-tests to achieve 100% coverage of all testable stuck-at-faults. The paper finishes with very promising performance-per-area and test-cycles-per-net results. We argue that our robust system architecture and EDA solution, designed and developed primarily for in-field testing of SoCs, can also be used for production and on-line testing as well as other applications.

The compilation of Verilog RTL designs into C or C++ models to be used in model-driven prototyping environments has recently become the subject of new research projects and publications. Our work describes the process of compiling Verilog RTL designs into C++ models which support intermediate representations. Depending on the given library, the compiled code can then be used for user-defined simulation targets, especially for object-oriented, model-driven prototyping scenarios. This allows user defined data, e.g. coverage points, to be propagated and modified throughout the design during simulation. We present examples such as symbolic RTL simulation, power consumption estimation on RTL as well as RTL ATPG for in-system stuck-at testing. We also present run-time comparison results.

The idea to use functional test pattern for production tests has been gaining more and more attention throughout the last years. We argue, that the gate inherent fault (GIF) model can add substantial value to this field. The GIF model allows synthesis independent RTL ATPG which achieves 100% stuck-at fault coverage on gate level. This paper proposes an RTL ATPG flow based on the GIF model. The peak memory usage can be adjusted. The test sets generated on RTL are then applied on 3 essential different test structures. The paper demonstrates the benefits of using multi-cycle-capture test sets which can efficiently be generated on RTL using the GIF model.

Many traditional technologies exist in the dynamic verification field. These are for instance virtual prototyping, simulation, emulation, FPGA based in-system verification and FPGA based system prototyping. Many attempts have been made in the past to find hybrid solutions which are supposed to be superior to these basic technologies. The goal is to find the right trade-off between cost, bring-up time, compile/synthesis time, design capacity, execution speed and their possibilities to be used in-system. This paper proposes a novel many-core hardware system and a design compilation flow, which combines most advantages of the aforementioned methodologies. Most noteworthy are the low cost, the high signal visibility, the fast execution speed and its extremely high capacity of multi-billion gate designs.

With growing design complexity, the reuse of module and subsystem level verification knowledge on electronic system level (ESL) becomes more and more challenging. The “Portable Stimulus Specification Working Group” intends to offer solutions such as stimuli reuse for today's verification challenges. This paper proposes a novel Inside-Out Verification (IOV) methodology, which makes module level dynamic verification knowledge highly reusable on system level by using transactions and inverse transactions. IOV can be combined with System Verilog based UVM. The examples in this paper are based on PDVL (a super-sub-set of SystemVerilog) and SystemC.

This paper proposes a novel aspect and transaction oriented programming, design and verification language (PDVL). The electronic system level (ESL) language is inspired by SystemVerilog, SystemC and many others, but adds for example program paradigms such as aspect and transaction oriented programming. To name a few improvement over existing languages, the method to define inverse transactions is added, software sequences become integral part of static verification, auto-abstraction during runtime is proposed and the paradigm of a design hierarchy becomes only relevant when required. PDVL offers novel solutions for state-of-the-art topics such as portable stimulus, intelligent testbench generation and various other ESL methodologies.

A promising technique to improve the performance per area factor for multithreaded soft-processors on FPGAs is System Hyper Pipelining (SHP), which can be efficiently applied on the register rich reconfigurable technologies with their distributed memory structures. SHP overcomes the limitations of C-Slow Retiming by adding context switching to enable thread stalling and thread bypassing possibilities. This enables thread reordering and dynamic thread scheduling techniques. The paper concentrates on acceleration techniques to improve the performance of an individual thread of a SHP based multithreaded CPU. This can be done by combining SHP with concepts such as cycle scaling, deep pipelining and out-of-order execution. The given results based on a Cortex M3 CPU mapped on a Virtex-6 FPGA are very promising.

This paper discusses a novel RTL to RTL partitioner flow to better cope with the challenges of modern rapid system prototyping on Multi-FPGA sytems. The proposed system partitioner flow is timing driven to evaluate the best achievable system performance within a given search space, reduces turn-around times if RTL code changes and enables more efficient debugging capabilities. System prototyping is often compared to emulation as alternative verification method, whereas system performance is used as one of the comparison points. This paper highlights some fundamental aspects for the achievable system performance of rapid system prototyping on Multi-FPGA systems.

This paper proposes a new single cycle access test structure for logic test. It eliminates the peak power consumption problem of conventional shift-based scan chains and reduces the activity during shift and capture cycles. This leads to more realistic circuit behavior during stuck-at and at-speed tests. It enables the complete test to run at much higher frequencies equal or close to the one in functional mode. It will be shown, that a lesser number of test cycles can be achieved compared to other published solutions. The test cycles per net based on a simple test pattern generator algorithm without test pattern compression is below 1 for larger designs and is independent of the design size. Results are compared to other published solutions on ISCAS'89 netlists. The structure allows an additional on-chip debugging signal visibility for each register. The method is backward compatible to full scan designs and existing test pattern generators and simulators can be used with a minor enhancement. It is shown how to combine the proposed solution with built-in self test (BIST) and massive parallel scan chains.

This paper addresses the problem of finding the right system prototyping hardware which can handle all different kinds of routing graphs for various designs and applications. A structure of multiple field-programmable gate arrays (FPGAs) and their concentric arrangement is proposed. The connectivity is switch based and has no routing limitation. Therefore, no routing limitations must be considered during the design partitioning process. The delays between FPGA pins are short compared to alternative concepts and can be considered as equal. This equal length concept between FPGA pins enables a novel method of wave-pipelined multiplexed data transfer. The flexible routing, the short delays and the equal length aspect enable faster system speeds compared to alternative concepts. The predictive and constant delay between FPGAs eases board level timing models for timing driven system partitioning algorithms.