
6.4 Functional Verification 153
Verify
Verify
Properties
(Dynamic)
Properties
(Static)Model
Graph
Model
FSM
FailedSuccessFailed Success
Validation of Dynamic Behavior
Validation of Static Behavior
ADL Specification
FIGURE 6.15
Validation of specification.
such as connectedness, false pipeline, data-transfer paths, completeness, and finite-
ness [9, 30, 31]. The dynamic behavior is verified by analyzing the instr uction flow
in the pipeline using a finite-state machine (FSM)-based model to validate several
important architectural properties such as determinism and in-order execution in
the presence of hazards and multiple exceptions [32–34]. The property checking
framew ...