SMV: xnor operator

NuSMV adds the xnor operator to the SMV languaage.

Author: kroening

CHANGELOG

@@ -2,7 +2,7 @@
 
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
-* SMV: LTL V operator
+* SMV: LTL V operator, xnor operator
 
 # EBMC 5.5
 

regression/smv/expressions/xnor1.desc

@@ -0,0 +1,7 @@
+CORE
+xnor1.smv
+
+^\[spec1\] G x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/smv/expressions/xnor1.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR x : boolean;
+
+ASSIGN init(x) := TRUE;
+ASSIGN next(x) := x xnor x;
+
+LTLSPEC G x

src/smvlang/expr2smv.cpp

@@ -552,6 +552,12 @@ bool expr2smvt::convert(
   else if(src.id()==ID_implies)
     return convert_binary(src, dest, "->", precedence = precedencet::IMPLIES);
 
+  else if(src.id() == ID_xor)
+    return convert_binary(src, dest, "xor", precedence = precedencet::OR);
+
+  else if(src.id() == ID_xnor)
+    return convert_binary(src, dest, "xnor", precedence = precedencet::OR);
+
   else if(
     src.id() == ID_AG || src.id() == ID_EG || src.id() == ID_AF ||
     src.id() == ID_EF || src.id() == ID_AX || src.id() == ID_EX ||

src/smvlang/parser.y

@@ -280,7 +280,7 @@ static void new_module(YYSTYPE &module)
 %right IMPLIES_Token
 %left  EQUIV_Token
 %left  IF_Token
-%left  xor_Token
+%left  xor_Token xnor_Token
 %left  OR_Token
 %left  AND_Token
 %left  NOT_Token
@@ -676,6 +676,7 @@ term       : variable_name
            | term EQUIV_Token term    { binary($$, $1, ID_smv_iff, $3); }
            | term IMPLIES_Token term  { binary($$, $1, ID_implies, $3); }
            | term xor_Token term      { j_binary($$, $1, ID_xor, $3); }
+           | term xnor_Token term     { binary($$, $1, ID_xnor, $3); }
            | term OR_Token term       { j_binary($$, $1, ID_or, $3); }
            | term AND_Token term      { j_binary($$, $1, ID_and, $3); }
            | NOT_Token term           { init($$, ID_not); mto($$, $2); }

src/smvlang/smv_typecheck.cpp

@@ -698,7 +698,7 @@ void smv_typecheckt::typecheck_expr_rec(
   }
   else if(
     expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_xor ||
-    expr.id() == ID_not || expr.id() == ID_implies)
+    expr.id() == ID_xnor || expr.id() == ID_not || expr.id() == ID_implies)
   {
     for(auto &op : expr.operands())
       typecheck_expr_rec(op, mode);