search

ymherklotz / vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.
https://vericert.ymhg.org
GNU General Public License v3.0
86 stars 5 forks source link

Implement Oshrximm #9

Closed ymherklotz closed 3 years ago

ymherklotz commented 3 years ago

Currently Oshrximm is not implemented, as it needs to be implemented with a division.

One reason for the mismatch between division and shift is shown below:

-11 / (1 << 1) = -5
-11 >>> 1      = -6

Therefore it will always be more efficient to use unsigned division by a constant compared to signed division by a constant.

Maybe there is a more efficient implementation of this special case.

ymherklotz commented 3 years ago

The following might be the correct, efficient implementation of Oshrximm (x / (2 ^ y)):

q = $signed(x) < 0 ? - ((-x) >> y) : x >> y;