Added a simple test

mwolf76 · Dec 31, 2012 · 95487f1 · 95487f1
1 parent 17f276b
commit 95487f1
Showing 1 changed file with 20 additions and 0 deletions.
diff --git a/test/shift.smv b/test/shift.smv
@@ -0,0 +1,20 @@
+MODEL lsh
+MODULE main
+
+VAR
+    x : uint32_t;
+    y : uint32_t;
+    c : uint32_t;
+
+INIT
+     (c = 1) & (x = 1) & (y = 1);
+
+TRANS
+     next(x) = ((c = 1) ? ( x << y )
+                        : ( x >> y ));
+
+     next(y) = y;
+
+     next(c) = ((x = 0x100000000) ? 2
+                           : (x = 1) ? 1
+                                     : c);