In reply to verif_learner:
I consider this a very dangerous attitude for a verification engineer to have which can lead to very expensive design respins. The behavioral model should be 100% accurate to the RTL design. If an implementation decision affects the behavior of the design, then the implementation should be completely specified. There should be no room for interpretation by different engineers as this leads to ambiguity and bugs.
RTL functionality is 100% deterministic. For any given set of inputs, there is exactly one output. It is the job of the verification engineer to determine what this output is and ensure that the DUT functions correctly. Anything less is unacceptable.