diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-09 13:44:13 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-09 13:44:13 +0100 |
| commit | 13f0b10dbe42cabd8340b8f9563f2cdd5a4ccd84 (patch) | |
| tree | 8c2172e981fd16c40fa237ae359f3c806ab05c88 /src/hls/HTLgen.v | |
| parent | df8c7a19b06ce5d0e22dca58b182dfa0b7298777 (diff) | |
| download | vericert-13f0b10dbe42cabd8340b8f9563f2cdd5a4ccd84.tar.gz vericert-13f0b10dbe42cabd8340b8f9563f2cdd5a4ccd84.zip | |
Fix merge error in oshrximm
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 052aaad..7d891c3 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -432,7 +432,9 @@ 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") + | 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))) (*ret (Vbinop Vdiv (Vvar r) (Vbinop Vshl (Vlit (ZToValue 1)) (Vlit (intToValue n))))*) |