Method of selecting a prover

1. A computer implemented method of selecting a schedule of one or more provers among a plurality of provers for a set of property checks to be resolved within a design of an electronic circuit under formal verification, comprising:

injecting into a transformer module in a computing device a plurality of input features relating to design parameters;

transforming, by said transformer module in said computing device, the plurality of input features, to obtain a plurality of transformed features, wherein transforming the plurality of input features comprises scaling and principal component analysis of the plurality of input features;

classifying, using a classification module in said computing device, provers from the plurality of provers in which the classification module is adapted to predict a probability that a specific prover resolves a specific property check faster than the remaining provers of the plurality of provers using the transformed input features;

modelling, by a regression module in said computing device, a dependency of a step size on the design parameters and expected time to check the assertion, and

selecting one or more prover schedule based on the results of the classification.

2. The method of claim 1 , wherein the transforming of the plurality of input features comprises removing cross correlation of the input features.

3. The method of claim 2 , wherein the step of removing the cross correlation of input features comprises:

standardizing, by a standard scaler module, the input features of the plurality of features to a unit variance to standardized features; and

applying, by a principal component analysis module in said computing device, an orthogonal transformation as a principal component analysis to the standardized features, and keeping the components resulting from the principal component analysis having a significant ratio of explained variance.

4. The method of claim 1 , wherein the classification module is pre-trained by collecting a set of training data pertaining to a set of designs, design parameters and runtimes for a plurality of provers, transforming the set of training data, and classifying the provers using the transformed set of training data.

5. The method of claim 1 , in which the classifying step comprises assigning, for a property, a probability to a prover using a multi class logistic regression based on design features and an expected result of the property.

6. The method of claim 1 , further comprising configuring the provers of the plurality of provers using linear regression modeling dependency of a step size on the design and an expected time of the prover to check the assertion.

7. The method of claim 6 , in which a prover is configured using a LASSO regression model having dependent variables and independent variables, in which the dependent variable of the regression model is a number of steps and the independent variable of the regression model are design statistics and expected check time.

8. The method of claim 1 , further comprising grouping provers in a plurality of prover groups and grouping properties in a plurality of properties, based on runtimes for each property and prover.

9. The method of claim 8 , further comprising assigning a prover group to a property group, in particular in which the assigned prover group of the plurality of prover groups has a minimum sum of runtimes.

10. The method of claim 9 , further comprising selecting, for each assigned prover group, the prover of the prover group having the minimum runtimes over the properties of the property group to which the assigned prover group is assigned.

11. The method of claim 9 , further comprising running the selected provers from the assigned prover groups in parallel.

12. A computer program product comprising a non-transitory computer medium having a computer program stored therein to cause a computer to perform the steps of a method according to claim 1 .