diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-04-17 11:54:42 +0200 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2018-04-19 05:17:42 -0400 |
| commit | 0f8743609b6f7c01eea84e541537eae9b00f9335 (patch) | |
| tree | 1294b1436e336b93a28e3b913b6b82279ce8587c /src/Util/ZUtil | |
| parent | 4326f7a49a41a8635d73f5bf00f3e8d9bc95cec6 (diff) | |
add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparation for reifying barrett; tweaked definition of cc_l
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Definitions.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index 2c87a9497..67ccbc772 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -17,7 +17,7 @@ Module Z. Definition cc_m s x := if dec (2 ^ (Z.log2 s) = s) then x >> (Z.log2 s - 1) else x / (s / 2). (* least significant bit *) - Definition cc_l x := Z.land x (Z.ones 1). + Definition cc_l x := x mod 2. (* two-register right shift *) Definition rshi s hi lo n := |