performance verification using partial evaluation and interval analysis
Summary form only given. A performance model for a typical design represented in a high-level description language can be generated by augmenting the design components with attributes and evaluation rules. An attribute represents some performance aspect of a design that can be either assigned a base initial value or calculated using an evaluation rule. Heat dissipation, dynamic power consumption, and maximum throughput rate are just a few examples of various performance aspects that can be represented with attributes. Evaluation rules contained in the performance model can be classified as either equational or procedural. An equational performance model is a model containing only evaluation rules that are composed of mathematical operations such as addition, subtraction, and so forth. Likewise, a procedural performance model may contain equational rules, but it also has rules composed of complex programming constructs such as an assignment statement, if-then-else, case, and while control constructs and procedure calls. Our method for performance verification involves placing relational constraints on attributes in the performance model and determining whether all constraints can be satisfied simultaneously. Interval mathematics provides a convenient technique to represent relational constraints as intervals. Each attribute has an initial interval from negative infinity to positive infinity. Further constraints are specified by the user, the interval analysis technique is applied, and a verification result is produced.
performance verification partial evaluation interval analysis performance model high-level description language attributes evaluation rules equational performance model procedural performance model relational constraints interval mathematics formal verification pdl