Merge pull request #1148 from diffblue/onehot1

Verilog: constant folding for `$onehot` and `$onehot0`

Author: tautschnig

CHANGELOG

@@ -2,6 +2,7 @@
 
 * Verilog: `elsif preprocessor directive
 * Verilog: fix for named generate blocks
+* Verilog: $onehot and $onehot0 are now elaboration-time constant
 * LTL/SVA to Buechi with --buechi
 
 # EBMC 5.6

regression/verilog/system-functions/onehot1.desc

@@ -0,0 +1,13 @@
+CORE
+onehot1.sv
+--module main
+^\[main\.pA0\] always \$onehot\(8\) == 1: PROVED .*$
+^\[main\.pA1\] always \$onehot\(10\) == 0: PROVED .*$
+^\[main\.pA2\] always \$onehot\(247\) == 0: PROVED .*$
+^\[main\.pB0\] always \$onehot0\(8\) == 0: PROVED .*$
+^\[main\.pB1\] always \$onehot0\(10\) == 0: PROVED .*$
+^\[main\.pB2\] always \$onehot0\(247\) == 1: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/onehot1.sv

@@ -0,0 +1,15 @@
+module main;
+
+  pA0: assert final ($onehot(8'b00001000)==1);
+  pA1: assert final ($onehot(8'b00001010)==0);
+  pA2: assert final ($onehot(8'b11110111)==0);
+
+  pB0: assert final ($onehot0(8'b00001000)==0);
+  pB1: assert final ($onehot0(8'b00001010)==0);
+  pB2: assert final ($onehot0(8'b11110111)==1);
+
+  // $onehot and $onehot0 yield elaboration-time constants
+  parameter Q1 = $onehot(3'b101);
+  parameter P1 = $onehot0(3'b101);
+
+endmodule

src/verilog/verilog_simplifier.cpp

@@ -33,6 +33,26 @@ countones(const constant_exprt &expr, const namespacet &ns)
     return to_constant_expr(simplified);
 }
 
+static constant_exprt onehot(const constant_exprt &expr, const namespacet &ns)
+{
+  if(numeric_cast_v<mp_integer>(countones(expr, ns)) == 1)
+    return true_exprt();
+  else
+    return false_exprt();
+}
+
+static constant_exprt onehot0(const constant_exprt &expr, const namespacet &ns)
+{
+  if(
+    numeric_cast_v<mp_integer>(countones(expr, ns)) ==
+    to_bitvector_type(expr.type()).get_width() - 1)
+  {
+    return true_exprt();
+  }
+  else
+    return false_exprt();
+}
+
 static exprt verilog_simplifier_rec(exprt expr, const namespacet &ns)
 {
   // Remember the Verilog type.
@@ -129,6 +149,18 @@ static exprt verilog_simplifier_rec(exprt expr, const namespacet &ns)
       ops.push_back(replication.op());
     expr = concatenation_exprt{ops, expr.type()};
   }
+  else if(expr.id() == ID_onehot)
+  {
+    auto &op = to_onehot_expr(expr).op();
+    if(op.is_constant())
+      expr = onehot(to_constant_expr(op), ns);
+  }
+  else if(expr.id() == ID_onehot0)
+  {
+    auto &op = to_onehot0_expr(expr).op();
+    if(op.is_constant())
+      expr = onehot0(to_constant_expr(op), ns);
+  }
 
   // We fall back to the simplifier to approximate
   // the standard's definition of 'constant expression'.