On Design Validation Using Verification Technology

Despite great advances in the area of Formal Verification during the last ten years, simulation is currently the primary means for performing design verification. The definition of an accurate and pragmatic measure for the coverage achieved by a suite of simulation vectors and the related problem of coverage directed automatic test generation are of great importance. In this paper we introduce a new set of metrics, called the Event Sequence Coverage Metrics (ESCMs). Our approach is based on a simple and automatic method to extract the control flow of a circuit so that the resulting state space can be explored for validation coverage analysis and automatic test generation. During simulation we monitor, in addition to state and transition coverage, whether certain control event sequences take place or not. We then combine formal verification techniques, using BDDs as the underlying representation, with traditional ATPG and behavioral test generation techniques to automatically generate additional sequences which traverse uncovered parts of the control state graph, or exercise an uninstantiated control event sequence.     

Specification, synthesis, and verification of hazard-free asynchronous circuits

This article describes three aspects of asynchronous design from a Petri-net specification called asignal transition graph (STG). First, we show that the STG defined by Chu [1] is too restrictive for specifying general asynchronous behavior and propose extensions to the STG which allow for more general and compact representation. Second, we show that syntactic constraints on STGs are not sufficient to guarantee hazard-free implementations under the unbounded gate delay model, and present techniques to synthesize two-level implementations which are hazard-free under the multiple signal change condition. To remove all hazards under the multiple signal change condition, the initial specification may need to be modified. Finally, we show that behavior containment test using the event coordination model [2] is a powerful tool for the formal verification of asynchronous circuits. This verification method can provide sanity checks for all synthesis methods that use the unbounded gate delay model, and provides a mechanism for designers to validate some manual gate-level changes to the final design.     

Design and verification of a frequency domain equalizer

In this work we provide a methodology for the design and verification of a frequency domain equalizer. The performance analysis of the equalizer is conducted using two methods: simulation based verification in Simulink and System Generator and theorem proving techniques in Higher Order Logic. We conduct both floating-point and fixed-point error estimations for the design in Simulink and System Generator, respectively. Then, we use formal error analysis based on the theorem proving to verify an implementation of the frequency domain equalizer based on the Fast LMS algorithm. The formal error analysis and simulation based error estimation of the algorithm intend to show that, when converting from one number domain to another, the algorithm produces the same values with an accepted error margin caused by the round-off error accumulation. This work shows the efficiency of combining simulation and formal verification based methods in verifying complex systems such as the frequency domain equalizer.     

Frequency Response Verification of Analog Circuits Using Global Optimization Techniques

This paper develops a new formal technique to verify the frequency response of analog circuits using global optimization techniques. Since simulation-based approaches are unable to cover the design space, there is a need for formal approaches to verify large circuits. Drawing parallels from the digital domain, the verification problem in the analog domain is modeled as a non-linear optimization problem and solved using global optimization techniques by ensuring that the implementation response is bounded within an envelope around the specification. We also address the problem of verifying frequency response under the influence of parameter variations. Direct as well as indirect techniques are illustrated using accurate frequency response models. Experimental results are presented to show the effectiveness of the proposed methodology.     

Real-Time Embedded Software Design for Mobile and Ubiquitous Systems

Currently available application frameworks that target at the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements for mobile and ubiquitous systems. In this work, we present the internal architecture and design flow of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates three techniques namely software component-based reuse, formal synthesis, and formal verification. The proposed architecture for VERTAF is component-based which allows plug-and-play for the scheduler and the verifier. The architecture is also easily extensible because reusable hardware and software design components can be added. Application examples developed using VERTAF demonstrate significantly reduced relative design effort, which shows how high-level reuse of software components combined with automatic synthesis and verification increases design productivity.     

Questasim的高级应用技巧在工程实践中的应用

Questasim在硬件设计和仿真验证中得到了广泛的应用,除基础仿真应用外,工具提供的代码覆盖率分析和仿真波形比较两种功能在实际应用中具有重要意义,可以有效地提高测试效率,减少冗余代码,缩短设计和验证时间,加强测试激励的完整性。本文介绍了如何在设计中应用上述两种功能,并结合实际项目分析了其在设计流程中应用的意义。     

An Automatic Functional Coverage for Digital Systems Through a Binary Particle Swarm Optimization Algorithm with a Reinitialization Mechanism

At present, functional verification represents the most expensive part of the digital systems design. Moreover, different problems such as: clock synchronization, code compatibility, simulation automation, new design methodologies, proper use of coverage metrics, among others represent challenges in this area. The automated test vector generation is involved in these problems. In this work, an automated functional test sequences generation for digital systems based on the use of coverage models and a binary Particle Swarm Optimization algorithm with a reinitialization mechanism (BPSOr) is described. Also, a comparison with other meta-heuristic algorithms such as: Genetic algorithms (GA) and pseudo-random generation is presented using different fitness functions, coverage models and devices under verification. The main strategy is based on the combination of the simulation and meta-heuristic algorithms to test the device behavior through the generation of test vector sequences. According to the results, the proposed test generation method represents a good alternative to increase the functional coverage during the automated functional verification of block-level digital systems verification.     

An automated parallel simulation flow for cyber-physical system design

Parallel and distributed simulation (PDS) is often employed to tackle the computational intensity of system-level simulation of real-world complex embedded and cyber-physical systems (CPSs). However, CPS models comprise heterogeneous components with diverge semantics for which incompatible PDS approaches are developed. We propose an automated PDS flow based on a formal modeling framework—with necessary extensions—targeting heterogeneous embedded and CPS design. The proposed flow characterizes the sequential executable specification of a heterogeneous model and generates a PDS cluster. State-of-the-art graph partitioning methods are adopted and a new extensible constraint-base formulation of the model partitioning problem is developed. The applicability, effectiveness, and scalability of the proposed flow is demonstrated using case studies.     

Verification Simulation Acceleration Using Code-Perturbation

We propose a simulation approach that can take a large design and swiftly cover its valid code-level operating states. The approach perturbs the program-control flow during the simulation to dynamically exhaust all branching possibilities in a verification code/program. The heuristic uses the program branching information from preprocessing the test/verification code. Using the branching information the simulation allows automatic run-time forced branching to make possible a full coverage of the instruction space spanned by the verification code/program. The aim is (1) to improve the verification simulation speed and (2) to get higher coverage rate for large core-base designs such as microprocessors or digital-signal-processing (DSP) products. A case study of a 32-bit RISC processor, used in a network system, is conducted. The application code for the processor (MCP, Myrinet control program) is used as a verification program. Despite the deviation from the valid software-reachable state of the system due to forced branching, a significant number of hard-to-reach hardware states (that can be reached only through the right mix of codes, often the code segments of an application software) are covered. Using the MCP program over 30% additional coverage is achieved with the proposed approach over ordinary code-based simulation for a fixed verification time. Further, compared to the conventional simulation approach, the proposed heuristic takes about 43% less compute-cycles to achieve same state coverage level.     

Analyzing encryption protocols using formal verification techniques

An approach to analyzing encryption protocols using machine-aided formal verification techniques is presented. The properties that the protocol should preserve are expressed as state invariants, and the theorems that must be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and several weaknesses that were revealed by attempting to verify and test the specification formally are discussed.<>     

Functional verification of instruction processing units through control flow modeling

The design verification of state-of-the-art high-performance microprocessors has become a significant challenge for test engineers. Deep pipelines, multiple execution units, out-of-order and speculative execution techniques, typically found in such microprocessors, contribute much to this complexity. Conventional methods, which treat the processor as a logic state machine or apply architectural level tests, fail to provide coverage of all possible corner cases in the design. This paper presents a functional verification method for modern microprocessors, which is based on innovative models of the microprocessor architecture, intended to cover the testing of all corner cases. In order to test the models presented in this work, an architecture independent coverage measurement system has been developed. The models were tested with both random code and real world applications in order to determine which of the two achieves higher coverage.     

Formal Methods in Communication Protocol Design

While early protocol design efforts had to rely largely on seat-of-the-pants methods, a variety of more rigorous techniques have been developed recently. This paper surveys the formal methods being applied to the problems of protocol specification, verification, and implementation. In the specification area, both the service that a protocol layer provides to its users and the internal operations of the entities that compose the layer must be defined. Verification then consists of a demonstration that the layer will meet its service specification and that each of the components is correctly implemented. Formal methods for accomplishing these tasks are discussed, including state transition models, program verification, symbolic execution, and design rules.     

Tracking down the chip killers [IC design verification]

As integration levels soar, formal methods are playing an increasing role in helping to crack the chip verification conundrum. This article considers the process of IC design, verification, simulation and test, with emphasis on formal verification and assertion methods.     

SoC设计验证策略及方法学

验证在SoC设计过程中有十分重要的作用,它将影响到芯片的整体开销和质量.本文首先介绍了当前业界比较常用的一些验证技术的特点,包括仿真技术、静态验证技术、形式验证、物理验证等,然后通过实例论述在SoC设计验证中的关键技术--重用技术、随机约束验证、自检技术和形式断言验证.     

Formal verification of timed systems: a survey and perspective

An overview of the current state of the art of formal verification of real-time systems is presented. We discuss commonly accepted models, specification languages, verification frameworks, state-space representation schemes, state-space construction procedures, reduction techniques, pioneering tools, and finally some new related issues. We also make a few comments according to our experience with verification tool design and implementation.     

Formal Verification of Analog and Mixed Signal Designs Using SPICE Circuit Simulation Traces

Analog and Mixed Signal (AMS) designs can be formally modeled as hybrid systems [45] and therefore formal verification techniques applicable to hybrid systems can be deployed to verify them. An extension to a formal verification approach applicable to hybrid systems is proposed to verify AMS designs [31]. In this approach formal verification (FV) is carried out on an AMS block using simulation traces from SPICE, a simulator widely used in the design and verification of analog and AMS blocks. A broader implication of this approach is the ability to carry out hierarchical verification using relevant simulation traces obtained at different abstraction levels of a design when modeled in appropriate platforms. This enables a seamless transition of design and verification artifacts from the highest level of abstraction to the lowest level of implementation at the transistor level of any AMS design and a resulting increase in confidence on the correctness of the final implementation. The proposed approach has been justified with its applications to different AMS design blocks. For each design, its formal model and the proposed computational techniques have been incorporated into CheckMate [11] - a FV tool for hybrid systems based on MATLAB and the Simulink/Stateflow framework from MathWorks. A further justification of the proposed approach is the resulting improvements observed in terms of reduced verification time for different specifications in each design.     

Efficient test case generation for validation of UML activity diagrams

Unified Modeling Language (UML) is widely used as a system level specification language in embedded system design. Due to the increasing complexity of embedded systems, the analysis and validation of UML specifications is becoming a challenge. UML activity diagram is promising to modeling the overall system behavior. However, lack of techniques for automated test case generation is one major bottleneck in the UML activity diagram validation. This article presents a methodology for automatically generating test cases based on various model checking techniques. It makes three primary contributions: First, we propose coverage-driven mapping rules that can automatically translate activity diagram to formal models. Next, we present a procedure for automatic property generation according to error models. Finally, we apply various model checking based test case generation techniques to enable efficient test case generation. Our experimental results demonstrate that our approach can reduce the validation effort drastically by reducing both test case generation time and required number of test cases to achieve a functional coverage goal.     

A formal model for proving hardware timing properties and identifying timing channels

Timing channels are becoming a critical threat to hardware security. When exploited, secret information can be revealed by analyzing the execution time statistically. There are a variety of methods for detecting timing channels such as statistical analysis, testing and formal verification. However, existing methods cannot guarantee that the timing channels can be identified due to limited test coverage or high performance overhead. In this work, we introduce a novel model for evaluating timing variations of the hardware design. Furthermore, we propose a systematical solution that integrates time label enhanced tracking logic and formally verifies the timing invariant property of hardware designs in order to identify hardware timing channels. We demonstrate our solution on several hardware implementations, including arithmetic units, cryptographic cores and cache. The proof results show that our solution can detect hardware timing channels effectively.