diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py
index 64991f73b..6098d01ed 100644
--- a/test/formal/opcodes.py
+++ b/test/formal/opcodes.py
@@ -64,3 +64,18 @@ def BYTE(i, x):
 		BitVecVal(0, x.size()),
 		(LShR(x, (x.size() - bit))) & 0xff
 	)
+
+def SIGNEXTEND(i, x):
+	bitBV = i * 8 + 7
+	bitInt = BV2Int(i) * 8 + 7
+	test = BitVecVal(1, x.size()) << bitBV
+	mask = test - 1
+	return If(
+		bitInt >= x.size(),
+		x,
+		If(
+			(x & test) == 0,
+			x & mask,
+			x | ~mask
+		)
+	)
diff --git a/test/formal/signextend.py b/test/formal/signextend.py
new file mode 100644
index 000000000..32d374261
--- /dev/null
+++ b/test/formal/signextend.py
@@ -0,0 +1,37 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+1) SIGNEXTEND(A, X) -> X if A >= Pattern::WordSize / 8 - 1;
+
+2) SIGNEXTEND(X, SIGNEXTEND(X, Y)) -> SIGNEXTEND(X, Y)
+
+3) SIGNEXTEND(A, SIGNEXTEND(B, X)) -> SIGNEXTEND(min(A, B), X)
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule1 = Rule()
+# Requirements
+rule1.require(UGE(A, BitVecVal(n_bits // 8 - 1, n_bits)))
+rule1.check(SIGNEXTEND(A, X), X)
+
+rule2 = Rule()
+rule2.check(
+    SIGNEXTEND(X, SIGNEXTEND(X, Y)),
+    SIGNEXTEND(X, Y)
+)
+
+rule3 = Rule()
+rule3.check(
+    SIGNEXTEND(A, SIGNEXTEND(B, X)),
+    SIGNEXTEND(If(ULT(A, B), A, B), X)
+)
+
diff --git a/test/formal/signextend_and.py b/test/formal/signextend_and.py
new file mode 100644
index 000000000..66ec40d7c
--- /dev/null
+++ b/test/formal/signextend_and.py
@@ -0,0 +1,26 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+AND(A, SIGNEXTEND(B, X)) -> AND(A, X)
+given
+    B < WordSize / 8 - 1 AND
+    A & (1 << ((B + 1) * 8)) == A
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+# Requirements
+rule.require(ULT(B, BitVecVal(n_bits // 8 - 1, n_bits)))
+rule.require((A & ((BitVecVal(1, n_bits) << ((B + 1) * 8)) - 1)) == A)
+rule.check(
+    AND(A, SIGNEXTEND(B, X)),
+    AND(A, X)
+)
diff --git a/test/formal/signextend_shift.py b/test/formal/signextend_shift.py
new file mode 100644
index 000000000..dc7cd119d
--- /dev/null
+++ b/test/formal/signextend_shift.py
@@ -0,0 +1,42 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+1) SHL(A, SIGNEXTEND(B, X)) -> SIGNEXTEND(A / 8 + B, SHL(A, B))
+given A % 8 == 0 AND A / 8 + B >= B
+
+2) SIGNEXTEND(A, SHR(B, X)) -> SAR(B, X)
+given
+    B % 8 == 0 AND
+    A <= WordSize
+    B <= wordSize
+    (WordSize - B) / 8 == A + 1
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule1 = Rule()
+rule1.require(A % 8 == 0)
+rule1.require(UGE(A / 8 + B, B))
+rule1.check(
+    SHL(A, SIGNEXTEND(B, X)),
+    SIGNEXTEND(A / 8 + B, SHL(A, X))
+)
+
+rule2 = Rule()
+rule2.require(B % 8 == 0)
+rule2.require(ULE(A, n_bits))
+rule2.require(ULE(B, n_bits))
+rule2.require((BitVecVal(n_bits, n_bits) - B) / 8 == A + 1)
+rule2.check(
+    SIGNEXTEND(A, SHR(B, X)),
+    SAR(B, X)
+)
+