diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-04 12:08:34 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-04 12:08:34 +0100 |
| commit | c7ffca253cf1767ae1416160e1a50bb5450c339f (patch) | |
| tree | edf492f9541aba7c9b0e9a282aa832d013c6e2f5 | |
| parent | 7460cf22bc3502fa1948915bf596f85a73f1fd01 (diff) | |
| download | vericert-kvx-c7ffca253cf1767ae1416160e1a50bb5450c339f.tar.gz vericert-kvx-c7ffca253cf1767ae1416160e1a50bb5450c339f.zip | |
Remove mulhs and mulhu
| -rw-r--r-- | src/translation/HTLgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 4cde0c8..9a82aa8 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -324,8 +324,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Omulimm n, r::nil => ret (boplit Vmul r n) - | Op.Omulhs, r1::r2::nil => ret (bop Vmul r1 r2) - | Op.Omulhu, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) |