| 摘要 |
This method uses 2 copies of the design under test. These 2 copies use different values (including primary inputs and initial states) to feed the supposedly irrelevant logic while using the same (or consistent as desired) values to feed the feature being verified. Symbolic method is used to efficiently determine whether the feature being verified behaves identically (or consistently as expected) in the 2 copies for all possible cases in the supposedly irrelevant logic.
|
