Browse Prior Art Database

Method to Verify the Retention of a Consistent State of a Processor in check stop Disclosure Number: IPCOM000246906D
Publication Date: 2016-Jul-13
Document File: 2 page(s) / 106K

Publishing Venue

The Prior Art Database


Today's verification methods for state retention of check stops in entire processor cores are very limited. Simulation and pure formal verification both suffer from the big state space. Our approach combines the two methods to leverage their individual strengths.

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

Page 01 of 2

Method to Verify the Retention of a Consistent State of a Processor in check stop

1 Background

It is critical for CP Sparing and for floor debug that the core once check stopped doesn't restart or change its state despite clocks still running. In other words the state of the core has to be retained to allow consistent debug and analysis.

Today we can't verify if there is any unwanted activity in the processor after check stop which would corrupt the core's state. Therefore the processor could still see activity due to secondary effects like sympathy checkers firing in case a counter times out which makes analysis of such cases hard. However it is not feasible in simulation to analyze the processor's behavior during a check stop with significant confidence due to the large possible state space. Even a purely formal analysis is not feasible as the state space of the design is too large. This methodology provides a way to verify that the processor core retains its state by leveraging a combination of simulation and formal verification.

2 Summary

As outlined above we present a methodology for verifying that the processor core retains its state This method consists of the following steps:

Start a simulation using the random simulation environment to reach a check stop


state of the core (y)

Use this check stop state (y) in the formal environment.


Load the inputs, register values and internal inputs from the state (y) .Set the inputs to


a constant value

Use this as a starting point for formal verification


Define properties that ensure that no output changes and no additional error


conditions occur

Perform formal verification with various saved checkpoints from different random


simulation runs

The method utilizes simulation to get deep into the state space of the core, which due to the state space of the processor would be very hard to do with a formal model only. Once the check stop has been reached the core's state is extracted and loaded into the equivalent formal model of the processor...