• Adam Nelson's avatar
    Clean up exec_terminst, remove $-variables · d4b31059
    Adam Nelson authored
    The current version of the Mu specification does not use $-variables to
    pass return values from terminsts to the normal destination of an EXC
    clause, instead allowing terminsts to have normal SSA return values
    that may be referenced in the EXC clause. This commit updates the
    formalism to match.
    
    Several other refactorings are included, such as making exec_terminst
    only return modified stacks, using a simpler representation of common
    instructions, and defining prefix/infix operators for SSA variables and
    registers in HOL.
    d4b31059
uvmMemoryScript.sml 16.6 KB