Intent-driven functional verification of digital designs

A method of detecting errors in a hardware design comprising:

• receiving a representation of a hardware design and information regarding an intended flow of logical signals among a plurality of variables in the representation;
• extracting the information regarding the intended flow from one or more inline annotations embedded within the representation of the hardware design, the one or more inline annotations having a predetermined format including a comment start marker, a directive marker, and a directive name;
• and
• inferring existence of one or more errors in the representation of the hardware design based upon the information regarding the intended flow of logical signals by
• translating the information regarding the intended flow of logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals, and
• determining whether one or more of the plurality of design verification checks are violated by the hardware design.

A method of detecting errors in a hardware design comprising:

• receiving a representation of a hardware design and information regarding an intended flow of logical signals among a plurality of variables in the representation, the information regarding the intended flow of logical signals specifying desired temporal behavior among the logical signals from which inferences are drawn regarding integrity of data conveyed by the logical signals;
• extracting the information regarding the intended flow from one or more inline annotations embedded within the representation of the hardware design, the one or more inline annotations having a predetermined format including a comment start marker, a directive marker, and a directive name;
• translating the information regarding the intended flow of logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals;
• and
• detecting existence of one or more errors in the hardware design by determining if one or more of the plurality of design verification checks are violated by the hardware design.

A method of detecting errors in a hardware design comprising:

• receiving a representation of a hardware design and information regarding an intended flow of logical signals among a plurality of variables in the representation, the information regarding the intended flow of logical signals comprises implied design intent that is inferred from the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• and
• inferring existence of one or more errors in the representation of the hardware design based upon the information regarding the intended flow of logical signals by
• translating the information regarding the intended flow of logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals, and
• determining whether one or more of the plurality of design verification checks are violated by the hardware design.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a representation of a hardware design and information regarding an intended flow of logical signals among a plurality of variables in the representation, the information regarding the intended flow of logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• and
• infer existence of one or more errors in the hardware design based upon the information regarding the intended flow of logical signals by
• translating the information regarding the intended flow of logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals, and
• determining whether one or more of the plurality of design verification checks are violated by the hardware design.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a representation of a hardware design and information regarding an intended flow of logical signals among a plurality of variables in the representation, the information regarding the intended flow of logical signals indicating one or more of desired temporal behavior and desired functional behavior of the logical signals from which inferences are drawn regarding integrity of data conveyed by the logical signals, wherein the information regarding the intended flow of logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• translate the information regarding the intended flow of logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals;
• and
• detect existence of one or more errors in the hardware design by determining whether one or more of the plurality of checks are violated by the hardware design.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a hardware design described in a hardware description language (HDL);
• receive one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a block enable property that relates to whether conditions enabling execution of a particular block of code in the HDL will never be satisfied;
• produce a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• detect existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a hardware design described in a hardware description language (HDL);
• receive one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the HDL through assignment operations appearing in the HDL;
• produce a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• detect existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a hardware design described in a hardware description language (HDL);
• receive one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers;
• produce a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• detect existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a hardware design described in a hardware description language (HDL);
• receive one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value;
• produce a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• detect existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a hardware design described in a hardware description language (HDL);
• receive one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a constant value variable property that relates to determining whether a variable in the HDL will always hold a constant value;
• produce a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• detect existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a representation of a hardware design and information regarding an intended behavior of logical signals associated with a plurality of variables in the representation, the information regarding the intended behavior of the logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• infer existence of one or more errors in the hardware design based upon the information regarding the intended behavior of the logical signals by
• translating the information regarding the intended behavior of the logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended behavior of the logical signals, and
• determining if one or more of the plurality of design verification checks are violated by the hardware design.

A machine-readable medium having stored thereon data representing instructions which, when executed by a processor, cause said processor to:

• receive a representation of a hardware design and information regarding an intended flow of logical signals among a plurality of variables in the representation, the information regarding the intended flow of logical signals indicating one or more of desired temporal behavior and desired functional behavior of the logical signals from which inferences are drawn regarding the integrity of data conveyed by the logical signals, the information regarding the intended flow of logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• translate the information regarding the intended flow of logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended flow of logical signals;
• and
• detect existence of one or more errors in the hardware design by determining if one or more of the plurality of checks can be violated by the hardware design.

A method comprising:

• receiving a hardware design described in a hardware description language (HDL);
• receiving one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a block enable property that relates to whether conditions enabling execution of a particular block of code in the HDL will never be satisfied;
• producing a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the design intent;
• and
• detecting existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A method comprising:

• a step for receiving a hardware design described in a hardware description language (HDL);
• a step for receiving one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a block enable property that relates to whether conditions enabling execution of a particular block of code in the HDL will never be satisfied;
• a step for producing a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• a step for detecting existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

An apparatus comprising:

• a means for receiving a hardware design described in a hardware description language (HDL);
• a means for receiving one or more indications of design intent, the one or more indications of design intent include information regarding implied design intent that is inferred from the hardware design by applying one or more predetermined properties to signal propagation among one or more variables in the HDL, the one or more predetermined properties include a block enable property that relates to whether conditions enabling execution of a particular block of code in the HDL will never be satisfied;
• a means for producing a failure model by generating a plurality of design verification checks based upon the HDL and the design intent, each of the plurality of design verification checks symptomatic of one or more errors in the hardware design;
• and
• a means for detecting existence of one or more errors in the hardware design by analyzing each design verification check of the plurality of design verification checks.

A method comprising:

• receiving a representation of a hardware design and information regarding an intended behavior of logical signals associated with a plurality of variables in the representation, the information regarding the intended behavior of the logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• inferring existence of one or more errors in the hardware design based upon the information regarding the intended behavior of the logical signals by
• translating the information regarding the intended behavior of the logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended behavior of logical signals, and
• determining if one or more of the plurality of design verification checks are violated by the hardware design.

A method comprising:

• a step for receiving a representation of a hardware design and information regarding an intended behavior of logical signals associated with a plurality of variables in the representation, the information regarding the intended behavior of the logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• a step for inferring existence of one or more errors in the hardware design based upon the information regarding the intended behavior of the logical signals by
• translating the information regarding the intended behavior of the logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended behavior of the logical signals, and
• determining if one or more of the plurality of design verification checks are violated by the hardware design.

A method comprising:

• receiving a representation of a hardware design and information regarding an intended behavior of logical signals associated with a plurality of variables in the representation, the information regarding the intended behavior of the logical signals indicating one or more of desired temporal behavior and desired functional behavior of the logical signals from which inferences are drawn regarding the integrity of data conveyed by the logical signals, the information regarding the intended behavior of the logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• translating the information regarding the intended behavior of the logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended behavior of the logical signals;
• and
• detecting existence of one or more errors in the hardware design by determining if one or more of the plurality of checks can be violated by the hardware design.

A method comprising:

• a step for receiving a representation of a hardware design and information regarding an intended behavior of logical signals associated with a plurality of variables in the representation, the information regarding the intended behavior of the logical signals indicating one or more of desired temporal behavior and desired functional behavior of the logical signals from which inferences are drawn regarding the integrity of data conveyed by the logical signals, the information regarding the intended behavior of the logical signals comprises implied design intent that is inferred from the representation of the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• a step for translating the information regarding the intended behavior of the logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended behavior of the logical signals;
• and
• a step for detecting existence of one or more errors in the hardware design by determining if one or more of the plurality of checks can be violated by the hardware design.

A method comprising:

• a step for receiving a representation of a hardware design and information regarding an intended behavior of logical signals associated with a plurality of variables in the representation, the information regarding the intended behavior of the logical signals comprises implied design intent that is inferred from the hardware design and a set of predetermined properties including one or more of:
• a block enable property that relates to whether conditions enabling execution of a particular block of code in the representation will never be satisfied,
• an assignment execution property that relates to checking whether each logical value can be assigned to a variable in the representation through assignment operations appearing in the representation,
• a conflicting assignments property that relates to checking whether a wire in the hardware design is driven by multiple conflicting drivers,
• a constant value memory element property that relates to determining whether a memory element in the hardware design will always hold a constant value, and
• a constant value variable property that relates to determining whether a variable in the representation will always hold a constant value;
• and
• a step for inferring existence of one or more errors in the representation of the hardware design based upon the information regarding the intended behavior of the logical signals by
• translating the information regarding the intended behavior of the logical signals into a plurality of design verification checks, each of the plurality of design verification checks representing a condition that must hold true in order for the hardware design to operate in accordance with the intended behavior of the logical signals, and
• determining whether one or more of the plurality of design verification checks are violated by the hardware design.