SMV: abs, bool, count, max, min, toint, word1

This adds the NuSMV operators abs, bool, count, max, min, toint, word to the
SMV frontend.

Author: kroening

CHANGELOG

@@ -6,6 +6,7 @@
 * SystemVerilog: fix for #-# and #=# for empty matches
 * SystemVerilog: fix for |-> and |=> for empty matches
 * LTL/SVA to Buechi with --buechi
+* SMV: abs, bool, count, max, min, toint, word1
 
 # EBMC 5.6
 

regression/smv/expressions/smv_abs1.desc

@@ -0,0 +1,12 @@
+CORE
+smv_abs1.smv
+
+^\[.*\] abs\(0\) = 0: PROVED .*$
+^\[.*\] abs\(1\) = 1: PROVED .*$
+^\[.*\] abs\(2\) = 2: PROVED .*$
+^\[.*\] abs\(-1\) = 1: PROVED .*$
+^\[.*\] abs\(-2\) = 2: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_abs1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC abs(0) = 0
+CTLSPEC abs(1) = 1
+CTLSPEC abs(2) = 2
+CTLSPEC abs(-1) = 1
+CTLSPEC abs(-2) = 2

regression/smv/expressions/smv_bool1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_bool1.smv
+
+^\[.*\] !bool\(0\): PROVED .*$
+^\[.*\] bool\(1\): PROVED .*$
+^\[.*\] bool\(2\): PROVED .*$
+^\[.*\] !bool\(0ud1_0\): PROVED .*$
+^\[.*\] bool\(0ud1_1\): PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/smv/expressions/smv_bool1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC !bool(0)
+CTLSPEC bool(1)
+CTLSPEC bool(2)
+CTLSPEC !bool(uwconst(0, 1))
+CTLSPEC bool(uwconst(1, 1))

regression/smv/expressions/smv_count1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+smv_count1.smv
+
+^\[.*\] count\(FALSE\) = 0: PROVED .*$
+^\[.*\] count\(TRUE\) = 1: PROVED .*$
+^\[.*\] count\(FALSE, TRUE\) = 1: PROVED .*$
+^\[.*\] count\(TRUE, FALSE\) = 1: PROVED .*$
+^\[.*\] count\(TRUE, TRUE, TRUE\) = 3: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_count1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+CTLSPEC count(FALSE) = 0
+CTLSPEC count(TRUE) = 1
+CTLSPEC count(FALSE, TRUE) = 1
+CTLSPEC count(TRUE, FALSE) = 1
+CTLSPEC count(TRUE, TRUE, TRUE) = 3

regression/smv/expressions/smv_max1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_max1.smv
+
+^\[.*\] max\(0, 1\) = 1: PROVED .*$
+^\[.*\] max\(-1, -2\) = -1: PROVED .*$
+^\[.*\] max\(-1, 1\) = 1: PROVED .*$
+^\[.*\] max\(1, 2\) = 2: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/smv/expressions/smv_max1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+CTLSPEC max(0, 1) = 1
+CTLSPEC max(-1, -2) = -1
+CTLSPEC max(-1, 1) = 1
+CTLSPEC max(1, 2) = 2

regression/smv/expressions/smv_min1.desc

@@ -0,0 +1,11 @@
+CORE
+smv_min1.smv
+
+^\[.*\] min\(0, 1\) = 0: PROVED .*$
+^\[.*\] min\(-1, -2\) = -2: PROVED .*$
+^\[.*\] min\(-1, 1\) = -1: PROVED .*$
+^\[.*\] min\(1, 2\) = 1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+--