diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-11-09 19:33:52 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-09 19:33:52 +0000 |
commit | f2f21f405ae0a1f457f7bc32d5053f0a92959e72 (patch) | |
tree | 86b73d98fee0c3b15ce0be02cc4d54f8946530c0 /src/hls/HTLgen.v | |
parent | 56ea621762c865c1c71bdc7ad99afc4f2c291d5c (diff) | |
download | vericert-kvx-f2f21f405ae0a1f457f7bc32d5053f0a92959e72.tar.gz vericert-kvx-f2f21f405ae0a1f457f7bc32d5053f0a92959e72.zip |
Change and add back HTLgen
Diffstat (limited to 'src/hls/HTLgen.v')
-rw-r--r-- | src/hls/HTLgen.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 68e0293..5f0f8bf 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -358,10 +358,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) - | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm") - (*ret (Vbinop Vdiv (Vvar r) - (Vbinop Vshl (Vlit (ZToValue 1)) - (Vlit (intToValue n))))*) + | Op.Oshrximm n, r::nil => + ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) + (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n))) + (Vbinop Vshru (Vvar r) (Vlit n))) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") |