| 摘要 |
<p>The present invention provides a method and apparatus for more efficiently validating high-level specifications of sequential digital systems, and in particular, those represented by hybrid models. According to the present invention, the high-level representation of a system is converted into a direct sum EFSM. An operator or a data file then provides an initial configuration or set of initial configurations of states and variable values. The method of the present invention then determines the set of configuration reachable from the initial configuration through symbolic execution of the direct sum EFSM. By representing the transitional relations of the machine as the and-product of Boolean expressions and arithmetic expressions, each class of expressions may be processed separately. When complete, the symbolic execution produces a cover of the set of reachable states. The results may then be reviewed to determine if the given specification produces unexpected or incompatible results. <IMAGE></p> |
