Page 38 - Mechatronic Systems Modelling and Simulation with HDLs

2.5 MODEL VERIFICATION AND VALIDATION 27

the design of digital circuits is increasingly based upon modelling in hardware
description languages, we can no longer differentiate the verification methods for
the designs from the verification of the corresponding models. Now if the design
and simulation models are exactly the same, there is no need for verification.
Occasionally, however, models have also been specially prepared for the simu-
lation, which may be necessary for performance reasons. In this case it may be
useful to perform a formal verification. This can be divided into two main fields:
‘equivalence checking’ and ‘model checking’.
In the first case we are concerned with the functional comparison of a de-
scription with a reference description. One example could be the comparison
between a gate net list and a reference model on register-transfer level, which
has been intensively simulated during the design process. This largely corre-
sponds with the verification based upon alternative models. However, in this
case simulation results are not compared, as is the case for the alternative
model verification. Instead formal, mathematical methods are used to find proof
of equivalence.
‘Model checking’, on the other hand, is concerned with using mathematical
methods to verify certain predictions about a circuit. So, for example, for a traffic
light circuit you could exclude the possibility of all sides showing a green light
[211]. This is based upon the automatic construction of a formalised proof for the
prediction in question. A similar principle is followed by Damm et al. in [77] for
the formal verification of state diagrams of automotive systems. ‘Model checking’
can also be used for the validation of a model.

2.5.3 Model validation

Introduction
The validity of a model is always partially dependent upon the desired applications.
This is clearly illustrated by the validation criteria listed below, see also Murray-
Smith [288]:
Empirical validity Correspondence between measurements and simulations.

Theoretical validity Consistency of a model with accepted theories.

Pragmatic validity Capability of the model to fulfil the desired purpose, e.g. as
part of a regulator.
Heuristic validity Potential for testing hypotheses, for the explanation of phe-
nomena and for the discovery of relationships.

These different validation requirements are the reason for the development of a
whole range of validation strategies. In addition to the methods presented in the
following sections there are also a few basic strategies that improve the degree to