Commit f370892c authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

optimised 96-bit version

parent 9d308b2c
......@@ -862,21 +862,13 @@ assert { reg[30] = 0xFF -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2
mov r30 r31;
asr r30;
assert { reg[30] = if reg[31] = 0xFF then 0xFF else 0 };
assert { forall t. BV8.eq BV8.zeros (BV8.asr (bitset BV8.zeros 0 t) 1) };
assert { forall t. BV8.eq BV8.ones (BV8.asr (bitset BV8.ones 0 t) 1) };
'QQ:
bld r30 0;
assert { at reg[30] 'QQ = 0xFF -> reg[30] = 0xFE + ?tf };
assert { at reg[30] 'QQ = 0x00 -> reg[30] = ?tf };
asr r30;
assert { reg[30] = if reg[31] = 0xFF then 0xFF else 0 };
assert { ?cf = 1 - at ?tf 'B };
check { ?cf = 0 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = abs(at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*abs(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) };
check { ?cf = 1 -> uint 2 reg 6 + pow2 16*uint 4 reg 26 + pow2 48*uint 2 reg 12 + pow2 64*uint 4 reg 8 = (pow2 96 - 1) - abs(at(uint 6 reg 14)'L11 - at(uint 6 mem (uint 2 reg rX))'S)*abs(at(uint 6 reg 8)'L11 - at(uint 6 mem (uint 2 reg rY))'S) };
S.modify_r6(); S.modify_r7();
S.modify_r26(); S.modify_r27(); S.modify_r28(); S.modify_r29();
S.modify_r12(); S.modify_r13();
......
This diff is collapsed.
No preview for this file type
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment