working/0.2/HSL2CFLScript.sml

39     (translate_assgn (TMOV dst src) = MMOV (conv_reg dst) (conv_roc src)) /\
41     (translate_assgn (TADD dst (Rg r) src) = MADD (conv_reg dst) (conv_reg r) (conv_roc src)) /\
42     (translate_assgn (TADD dst (Cn v) (Rg r)) = MADD (conv_reg dst) (conv_reg r) (MC v)) /\
43     (translate_assgn (TADD dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1+v2))) /\
44     (translate_assgn (TSUB dst (Rg r) src) = MSUB (conv_reg dst) (conv_reg r) (conv_roc src)) /\
45     (translate_assgn (TSUB dst (Cn v) (Rg r)) = MRSB (conv_reg dst) (conv_reg r) (MC v)) /\
46     (translate_assgn (TSUB dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1-v2))) /\
47     (translate_assgn (TRSB dst (Rg r) src) = MRSB (conv_reg dst) (conv_reg r) (conv_roc src)) /\
48     (translate_assgn (TRSB dst (Cn v) (Rg r)) = MSUB (conv_reg dst) (conv_reg r) (MC v)) /\
49     (translate_assgn (TRSB dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v2-v1))) /\
50     (translate_assgn (TMUL dst (Rg r) src) = MMUL (conv_reg dst) (conv_reg r) (conv_roc src)) /\
51     (translate_assgn (TMUL dst (Cn v) (Rg r)) = MMUL (conv_reg dst) (conv_reg r) (MC v)) /\
52     (translate_assgn (TMUL dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1*v2))) /\
53     (translate_assgn (TAND dst (Rg r) src) = MAND (conv_reg dst) (conv_reg r) (conv_roc src)) /\
54     (translate_assgn (TAND dst (Cn v) (Rg r)) = MAND (conv_reg dst) (conv_reg r) (MC v)) /\
55     (translate_assgn (TAND dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1 && v2))) /\
56     (translate_assgn (TORR dst (Rg r) src) = MORR (conv_reg dst) (conv_reg r) (conv_roc src)) /\
57     (translate_assgn (TORR dst (Cn v) (Rg r)) = MORR (conv_reg dst) (conv_reg r) (MC v)) /\
58     (translate_assgn (TORR dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1 !! v2))) /\
59     (translate_assgn (TEOR dst (Rg r) src) = MEOR (conv_reg dst) (conv_reg r) (conv_roc src)) /\
60     (translate_assgn (TEOR dst (Cn v) (Rg r)) = MEOR (conv_reg dst) (conv_reg r) (MC v)) /\
61     (translate_assgn (TEOR dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1 ?? v2))) /\
63     (translate_assgn (TLSL dst (Rg r) src2_num) = MLSL (conv_reg dst) (conv_reg r) src2_num) /\
64     (translate_assgn (TLSL dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v << w2n src2_num))) /\
65     (translate_assgn (TLSR dst (Rg r) src2_num) = MLSR (conv_reg dst) (conv_reg r) src2_num) /\
66     (translate_assgn (TLSR dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v >>> w2n src2_num))) /\
67     (translate_assgn (TASR dst (Rg r) src2_num) = MASR (conv_reg dst) (conv_reg r) src2_num) /\
68     (translate_assgn (TASR dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v >> w2n src2_num))) /\
69     (translate_assgn (TROR dst (Rg r) src2_num) = MROR (conv_reg dst) (conv_reg r) src2_num) /\
70     (translate_assgn (TROR dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v #>> w2n src2_num)))