Verilog: generate property description prior to expression synthesis

This generates the property description from the expression prior to
synthsis, which is closer to the Verilog source code.

Author: kroening

regression/verilog/SVA/immediate1.desc

@@ -1,7 +1,7 @@
 CORE
 immediate1.sv
 --bound 20
-^\[main\.assert\.1\] always \(main\.x == 11 \|-> main\.x & 1\): PROVED up to bound 20$
+^\[main\.assert\.1\] always main\.x & 1: PROVED up to bound 20$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/immediate2.desc

@@ -1,7 +1,7 @@
 CORE broken-smt-backend
 immediate2.sv
 --bound 0
-^\[main\.assert\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
+^\[main\.assume\.1\] assume always 0: ASSUMED$
 ^\[main\.assert\.2\] always main\.index < 10: PROVED up to bound 0$
 ^\[main\.assert\.3\] always 0: REFUTED$
 ^EXIT=10$

regression/verilog/SVA/initial2.desc

@@ -1,7 +1,7 @@
 CORE
 initial2.sv
 --module main --bound 1
-^\[main\.assert\.1\] 1 == 1: PROVED up to bound 1
+^\[main\.assert\.1\] main\.counter == 1: PROVED up to bound 1
 ^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound 1
 ^EXIT=0$
 ^SIGNAL=0$

regression/verilog/SVA/named_property1.desc

@@ -1,7 +1,7 @@
 CORE
 named_property1.sv
 --bound 0
-^\[main\.assert\.1\] always main\.x == 10: PROVED up to bound 0$
+^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/unbounded1.desc

@@ -1,7 +1,7 @@
 CORE
 unbounded1.sv
 --module main --bound 1
-^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$
+^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/verilog/enums/enum4.desc

@@ -3,5 +3,5 @@ enum4.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main.A == main.A: PROVED up to bound 0$
+^\[main\.p1\] always main\.A == 1: PROVED up to bound 0$
 --

regression/verilog/enums/enum_base_type1.desc

@@ -3,5 +3,5 @@ enum_base_type1.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always 8 == 8: PROVED up to bound 0$
+^\[.*\] always \$bits\(main\.A\) == 8: PROVED up to bound 0$
 --

regression/verilog/enums/enum_base_type2.desc

@@ -3,5 +3,5 @@ enum_base_type2.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always 8 == 8: PROVED up to bound 0$
+^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED up to bound 0$
 --

regression/verilog/expressions/concatenation2.desc

@@ -3,7 +3,7 @@ concatenation2.v
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.pA\] always -1 == -1: PROVED up to bound 0$
-^\[main\.property\.pB\] always 15 == 15: PROVED up to bound 0$
+^\[main\.property\.pA\] always main\.A == -1: PROVED up to bound 0$
+^\[main\.property\.pB\] always main\.B == 15: PROVED up to bound 0$
 --
 ^warning: ignoring

regression/verilog/expressions/static_cast1.desc

@@ -3,6 +3,6 @@ static_cast1.sv
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p0\] always 255 == 255: PROVED up to bound 0$
+^\[main\.p0\] always 'hFFFF == 255: PROVED up to bound 0$
 --
 ^warning: ignoring