A behavioural model of a design can be used to verify that design. Such a model is used when there exists a way to represent the design's behaviour in a significantly simplified manner (e.g. if the objective is to build a very fast adder, the design's behaviour could be modeled with a simple "+"). Typically only the main functionality of the design would be modeled while other parts (like processor interface and RAM interfaces) would be ignored. Also in many cases there is no need to model the exact timing relationship as occurs in the design.
In principle the behavioural model will receive the same stimulus as the design and produce the same output. However often the stimulus and response can be represented in a more abstract format. For example if the actual design works on data blocks which are received one byte at a time in four clock cycles, the behavioural model could just operate on a simple hex number.
Often behavioural models are used to generate expected (golden) log files. In this case the the behavioural model operates on a stimulus file and creates a result file. The design is stimulated with the same input file via a file reader (see Reading from Files) and will protocol it's response into a transaction log (see Using Transaction Logs). The transaction log can then be compared with the expected results from the behavioural model (e.g. with Unix' diff utility).
