Transformation of simple subset of PSL into SERE implication formulas for verification with model checking and simulation engines using semantic preserving rewrite rules
AssigneeCadence Design Systems, Inc.
InventorsVinaya Singh, Tarun Garg
Life of this patent
Estimating the term…
Abstract
The disclosure presents a formulation to support simulatable subset (also known as ‘simple-subset’) of a property specification language. This method is applicable for model checking and simulation. In this formulation, the ‘simple-subset’ is transformed to a set of basic formulas. Verification engines are required to support the basic formula only. The basic formula is a form of automata in the property specification language. This is called SERE implication. The efficiency of verification is dependent on size of automata. Miscellaneous opportunistic rules are applied to optimize SERE implication formulas.
Claims51
A method for transforming a formula in a simple-subset, comprising:
- inputting a property specification language formula, the formula comprising a plurality of forms;
- and
- applying one or more of a set of transformation rules to transform the property specification language formula into a Sugar Extended Regular Expression (SERE) implication, the SERE implication being of one form.
A method of converting a simple subset formula into a Sugar Extended Regular Expression (SERE) implication comprising:
- applying a set of rules to the simple subset formula, the rules preserving the semantics of the simple subset formula while transforming the formula into SERE implication.
A system for transforming a formula in a simple-subset, comprising:
- means for inputting a property specification language formula, the formula comprising a plurality of forms;
- and
- means for applying one or more of a set of transformation rules to transform the property specification language formula into a Sugar Extended Regular Expression (SERE) implication, the SERE implication being of one form.
A computer program product embodied on computer readable medium, the computer readable medium having stored thereon a sequence of instructions which, when executed by a processor, causes the processor to execute a method for a method for transforming a formula in a simple-subset, the method comprising:
- inputting a property specification language formula, the formula comprising a plurality of forms;
- and
- applying one or more of a set of transformation rules to transform the property specification language formula into a Sugar Extended Regular Expression (SERE) implication, the SERE implication being of one form.
Dependencies are inferred from the claim text.