Verilog: zero-count replication

.github/workflows/pull-request-checks.yaml

@@ -49,6 +49,8 @@ jobs:
         run: make -C regression/ebmc test-z3
       - name: Run the verilog tests
         run: make -C regression/verilog test
+      - name: Run the verilog tests with Z3
+        run: make -C regression/verilog test-z3
       - name: Print ccache stats
         run: ccache -s
 
@@ -100,6 +102,8 @@ jobs:
         run: make -C regression/ebmc test-z3
       - name: Run the verilog tests
         run: make -C regression/verilog test
+      - name: Run the verilog tests with Z3
+        run: make -C regression/verilog test-z3
       - name: Print ccache stats
         run: ccache -s
 

regression/verilog/Makefile

@@ -1,4 +1,9 @@
 default: test
 
+TEST_PL = ../../lib/cbmc/regression/test.pl
+
 test:
-	@../../lib/cbmc/regression/test.pl -c ../../../src/ebmc/ebmc
+	@$(TEST_PL) -c ../../../src/ebmc/ebmc
+
+test-z3:
+	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend

regression/verilog/assignment-to-concatenation/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$

regression/verilog/assignment-to-range1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --bound 1
 ^EXIT=0$

regression/verilog/bit-extract/bit-extract1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 bit-extract1.v
 --bound 1
 ^EXIT=0$

regression/verilog/bit-extract/bit-extract2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 bit-extract2.v
 --module main --bound 1 --trace
 ^EXIT=10$

regression/verilog/case/case3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 case3.v
 --module main --bound 3 --trace
 ^EXIT=10$

regression/verilog/case/case4.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 case4.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/functioncall/functioncall3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 functioncall3.v
 --module main --bound 0
 ^EXIT=0$

regression/verilog/generate/generate-for2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 generate-for2.v
 --bound 0
 ^EXIT=0$

regression/verilog/generate/generate-reg1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 generate-reg1.v
 --module main --bound 0
 ^EXIT=0$

regression/verilog/generate1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/indexed-part-select1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.sv
 --bound 1
 ^EXIT=0$

regression/verilog/modules/ports2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 ports2.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/multiple_assign1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 1
 ^EXIT=0$

regression/verilog/nondet1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.v
 --module main --bound 3 --trace
 ^EXIT=10$

regression/verilog/replication/replication1.desc

@@ -0,0 +1,7 @@
+CORE broken-smt-backend
+replication1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/replication1/main.v → regression/verilog/replication/replication1.v

@@ -13,8 +13,12 @@ module main(in);
   always assert property2:
     {{ 1 { in }}, in } == { in, in };
 
-  // replication of something boolean
+  // 0-replication
   always assert property3:
+    {{ 0 { in }}, in } == { in };
+
+  // replication of something boolean
+  always assert property4:
     {{ 1 { 1'b0 }}, in } == in;
 
 endmodule

regression/verilog/system_verilog_assertion/system_verilog_assertion3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 system_verilog_assertion3.sv
 --module main --bound 1
 ^EXIT=0$

src/verilog/verilog_typecheck_expr.cpp

@@ -1911,7 +1911,7 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
   if(op1.type().id()==ID_bool)
     op1 = typecast_exprt{op1, unsignedbv_typet{1}};
 
-  unsigned width=get_width(expr.op1().type());
+  auto width = get_width(expr.op1().type());
 
   mp_integer op0 = convert_integer_constant_expression(expr.op0());
 
@@ -1921,12 +1921,8 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
       << "number of replications must not be negative";
   }
 
-  if(op0==0)
-  {
-    // ruled out by IEEE 1364-2001
-    throw errort().with_location(expr.source_location())
-      << "number of replications must not be zero";
-  }
+  // IEEE 1800-2017 explicitly allows replication with
+  // count zero.
 
   {
     expr.op0()=from_integer(op0, natural_typet());