From 59db0f1537038cb355587b12be994b2187e7e8a8 Mon Sep 17 00:00:00 2001 From: hrkrshnn Date: Tue, 10 Aug 2021 12:55:34 +0200 Subject: [PATCH] An equivalence check for SIGNEXTEND opcode Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract --- test/formal/signextend_equivalence.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test/formal/signextend_equivalence.py diff --git a/test/formal/signextend_equivalence.py b/test/formal/signextend_equivalence.py new file mode 100644 index 000000000..1199fff47 --- /dev/null +++ b/test/formal/signextend_equivalence.py @@ -0,0 +1,24 @@ +from rule import Rule +from opcodes import * + +""" +Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract +""" + +rule = Rule() +n_bits = 256 + +x = BitVec('X', n_bits) + +def SIGNEXTEND_native(i, x): + return SignExt(256 - 8 * i - 8, Extract(8 * i + 7, 0, x)) + +for i in range(0, 32): + rule.check( + SIGNEXTEND(BitVecVal(i, n_bits), x), + SIGNEXTEND_native(i, x) + ) + +i = BitVec('I', n_bits) +rule.require(UGT(i, BitVecVal(31, n_bits))) +rule.check(SIGNEXTEND(i, x), x)