# US 2014/0157217 A1 · Sequential non-deterministic detection in hardware design

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 2014/0157217 A1
- Document ID: US20140157217A1
- Status: Published application
- Kind: A1
- Application number: 13/909,747
- Filed: 2013-06-04
- Published: 2014-06-05
- Earliest claimed: 2012-06-04
- Assignees: Reveal Design Automation
- Applicants: Reveal Design Automation
- Inventors: Akram Baransi; Michael Zajac; Zaher Andraus
- Web page: https://patentgrep.com/patent/US20140157217A1

## CPC

- G06F 30/3323: using formal methods, e.g. equivalence checking or property checking
- G06F 30/33: Design verification, e.g. functional simulation or model checking
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)

## Abstract

The use of X's in RTL design is widely common for improving synthesis results and, in some cases, verification effectiveness. However, it has certain implications on verification completeness. Human design error or flawed synthesis may lead to undesirable non-determinism on design outputs, not always detected consistently by simulators. This disclosure presents a framework for formalizing observable behavior on digital design output, and a proof methodology for detecting non-determinism or proving correctness with respect to observable X, using a model checker.

## Claims

### Claim 1

A computer-implemented method for verifying a hardware design for an electronic circuit, comprising:
providing a hardware design description for the electronic circuit;
extracting a set of design elements from the hardware design description, where the set of design elements represent the electronic circuit in terms of signals and logical operations performed on the signals and the set of design elements includes deterministic elements having a value selected from zero or one and at least one non-deterministic element having a value denoted by a variable;
assigning a first set of values to the deterministic elements of the electronic circuit;
checking one or more sample points of the electronic circuit using the first set of values for the deterministic elements and across all possible values for the at least one non-deterministic element; and
detecting non-determinism of the non-deterministic element on the one or more sample points of the electronic circuit when two values assigned to the at least one non-deterministic element yield different values at the one or more sampling points, wherein at least the steps of checking one or more sample points and detecting non-determinism are executed by a computer processor.