Browse Prior Art Database

A Novel method for Verifying Multi/Fixed Cycle Instructions in the Pipeline

IP.com Disclosure Number: IPCOM000245203D
Publication Date: 2016-Feb-18
Document File: 6 page(s) / 76K

Publishing Venue

The IP.com Prior Art Database

Abstract

This paper will provide a novel method for verifying multi/fixed cycle instruction in sequencing – covering different kinds of flushes and instruction interactions. This method uses splitting the complex problem into phases by constructing internal equivalences (over time/conditional) and performing conditional merges.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 44% of the total text.

Page 01 of 6

A Novel method for Verifying Multi/Fixed Cycle Instructions in the Pipeline

Description

As Verification of hardware systems is increasingly difficult with more complex designs like multi-core architectures. Formal verification is a technique to cope with the increased complexity and, although not suitable for all verification problems, is established industry practice in a wide range of applications. Formal verification can be helpful to conclusively prove correctness of systems by virtue of analysis of all the states which is lacking in simulation based approaches.

One such application is verification of Floating-Point (FP) data flow and control. This area is particularly suitable due to existence of complex corner cases which aren't covered by simulation, and FV is able to provide exhaustive coverage (with effort to "manage" computational complexity by decomposing/abstracting the problem), Recent extensions make control verification amenable by allowing sequences of instructions, hence exercising complex control as it relates to inter-instructions interactions and pipeline control [2]. However there are limitation to these idea, it does not address the full proof of MC (Multi cycle) instructions and fixed cycle complex instruction.It does not leverage the domain/design knowledge to full extent to decompose the problem complexity, Albeit it uses different instance of the same design as a reference, finding internal equivalences is difficult as far as MC instructions are concerned, i.e. number of gates/registers are only equivalent at particular time (not always) and operations performed by design instance over time, is orthogonal to operations performed by reference instance. Both these designs converge only in the end/end of execution phase. If the verification result concluded as unsolved (mostly the case due to complexity), it is hard to measure the verification progress.

This method addresses the solution for verifying multi/fixed cycle instruction in sequencing by splitting the complex problem into phases by constructing internal equivalences (over time/conditional) and performing conditional merges. We will discuss the details in following subsections by providing basics on pipeline.

Pipeline

An instruction pipeline is a technique used in the design of computers to increase their instruction throughput (the number of instructions that can be executed in a unit of time). The basic instruction cycle is broken up into a series called a pipeline. Rather than processing each instruction sequentially (one at a time, finishing one instruction before starting the next), each instruction is split up into a sequence of steps so different steps can be executed concurrently (at the same time) and in parallel (by different circuitry).

1


Page 02 of 6

Pipelining increases instruction throughput by performing multiple operations at the same time (concurrently), but does not reduce instruction latency, which is the time to complete a singl...