Is a formal specification complete ?
By `formal' we mean a machine-readable description of what is correct or incorrect behaviour. A complete specification might describe all allowable behaviours and prohibit all remaining behaviours, but most formal definitions today are not complete in this sense. For instance, a definition that consists of a list of safety assertions and a few liveness assertions might still allow all sorts of behaviours that the designer knows are wrong. He can go on adding more assertions, but when does he stop ?
One might define a 'complete specification' as one that describes all observable behaviours. Such a specification does not restrict or prescribe the internal implementation in black box terms since this is not observable.
When evaluating an assertion-based test program for an IP block, we can think of various, ad hoc, coverage metrics: e.g. What percentage of rule disjuncts (terms that are ORed) held as dominators (a term that makes the disjunction hold) on their own (without any other term in that disjunction holding) ?
Or, e.g. What percentage of reachable state space was spanned?
But there are no widely accepted such metrics in the industry, but the sytem Verilog 'cover' statement keeps statistics. »System Verilog Assertions
|8: (C) 2012-18, DJ Greaves, University of Cambridge, Computer Laboratory.|