Merge pull request #685 from diffblue/fixup-verilog-implies

Verilog: fix for output of `->`

Author: tautschnig

regression/verilog/expressions/bit-extract6.desc

@@ -1,8 +1,8 @@
 CORE
 bit-extract6.sv
 --module main --bound 0
-^\[main\.p0\] always \(main\.index == 8 |-> main\.vector\[7 - main\.index - 1\] == 1\): PROVED up to bound 0$
-^\[main\.p1\] always \(main\.index >= 1 \&\& main\.index <= 7 |-> main\.vector\[7 - main\.index - 1\] == 0\): PROVED up to bound 0$
+^\[main\.p0\] always main\.index == 8 -> main\.vector\[7 - main\.index - 1\] == 1: PROVED up to bound 0$
+^\[main\.p1\] always main\.index >= 1 \&\& main\.index <= 7 -> main\.vector\[7 - main\.index - 1\] == 0: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/synthesis/always_comb2.desc

@@ -1,9 +1,9 @@
 CORE
 always_comb2.sv
 --bound 0
-^\[main\.property\.p0\] always \(main\.data == 0 |-> main\.decoded == 1\): PROVED up to bound 0$
-^\[main\.property\.p1\] always \(main\.data == 1 |-> main\.decoded == 2\): PROVED up to bound 0$
-^\[main\.property\.p2\] always \(main\.data == 2 |-> main\.decoded == 4\): PROVED up to bound 0$
+^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED up to bound 0$
+^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED up to bound 0$
+^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/verilog/expr2verilog.cpp

@@ -1324,11 +1324,11 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
 
   else if(src.id()==ID_implies)
     return convert_binary(
-      to_multi_ary_expr(src), "|->", precedence = verilog_precedencet::MIN);
+      to_multi_ary_expr(src), "->", precedence = verilog_precedencet::IMPLIES);
 
   else if(src.id()==ID_iff)
     return convert_binary(
-      to_multi_ary_expr(src), "<->", precedence = verilog_precedencet::MIN);
+      to_multi_ary_expr(src), "<->", precedence = verilog_precedencet::IMPLIES);
 
   else if(src.id()==ID_reduction_or)
     return convert_unary(

src/verilog/expr2verilog_class.h

@@ -38,7 +38,7 @@ enum class verilog_precedencet
   AND = 7,       //  &&
   OR = 6,        //  ||
   IF = 5,        //  ?:
-  IMPLIES = 4,   //  ->
+  IMPLIES = 4,   //  -> <->
   ASSIGN = 3,    //  = += -= etc.
   CONCAT = 18,   //  { } concatenation, {{ }} replication
   MIN = 0        //  anything even weaker, e.g., SVA