New phase-free SMV model representation using formulas
Build a unified formula that represents a GADD process. Mark variable assignments by the next phase variable values (create a version of a variable). It is assumed that a variable can be assigned only once during the clock cycle.
Build the phase-free
next() function for the variables using the earlier constructed versions.