Verilog: introduce the Verilog indexer

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

@@ -51,6 +51,8 @@ jobs:
         run: make -C regression/verilog test
       - name: Run the verilog tests with Z3
         run: make -C regression/verilog test-z3
+      - name: Run the vlindex tests
+        run: make -C regression/vlindex test
       - name: Print ccache stats
         run: ccache -s
 
@@ -103,6 +105,8 @@ jobs:
         run: make -C regression/verilog test
       - name: Run the verilog tests with Z3
         run: make -C regression/verilog test-z3
+      - name: Run the vlindex tests
+        run: make -C regression/vlindex test
       - name: Print ccache stats
         run: ccache -s
       - name: Upload the ebmc binary
@@ -181,6 +185,8 @@ jobs:
           make -C regression/ebmc test
       - name: Run the verilog tests
         run: make -C regression/verilog test
+      - name: Run the vlindex tests
+        run: make -C regression/vlindex test
       - name: Print ccache stats
         run: ccache -s
 
@@ -222,6 +228,8 @@ jobs:
         run: make -C regression/verilog test
       - name: Run the verilog tests with Z3
         run: make -C regression/verilog test-z3
+      - name: Run the vlindex tests
+        run: make -C regression/vlindex test
       - name: Print ccache stats
         run: ccache -s
 

regression/verilog/case/nested_case1.desc

@@ -0,0 +1,8 @@
+CORE
+nested_case1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[main.property.p1\] .* PROVED up to bound 0$
+--
+^warning: ignoring

regression/verilog/case/nested_case1.v

@@ -0,0 +1,17 @@
+module main(input x, input y);
+
+  reg result;
+
+  always @(x, y)
+    case(x)
+      0: result = 0;
+      1:
+        case(y)
+          1: result = 1;
+          0: result = 0;
+        endcase
+    endcase
+
+  always assert p1: result == (x && y);
+
+endmodule

regression/vlindex/Makefile

@@ -0,0 +1,6 @@
+default: test
+
+TEST_PL = ../../lib/cbmc/regression/test.pl
+
+test:
+	@$(TEST_PL) -e -p -c ../../../src/vlindex/vlindex

regression/vlindex/hierarchy1/hierarchy1.desc

@@ -0,0 +1,8 @@
+CORE
+
+--hierarchy
+^sub$
+^subsub$
+^top$
+^EXIT=0$
+^SIGNAL=0$

regression/vlindex/hierarchy1/hierarchy1.v

@@ -0,0 +1,11 @@
+module top;
+  sub instance1();
+  sub instance2();
+endmodule
+
+module sub;
+  subsub instance3();
+endmodule 
+
+module subsub;
+endmodule

regression/vlindex/modules1/modules1.desc

@@ -0,0 +1,9 @@
+CORE
+
+--modules
+^nested modules1.v line 5$
+^sub modules1.v line 4$
+^top modules1.v line 1$
+^EXIT=0$
+^SIGNAL=0$
+

regression/vlindex/modules1/modules1.v

@@ -0,0 +1,7 @@
+module top;
+endmodule 
+
+module sub;
+  module nested;
+  endmodule
+endmodule 

src/Makefile

@@ -1,10 +1,10 @@
 DIRS = ebmc hw-cbmc temporal-logic trans-word-level trans-netlist \
-       verilog vhdl smvlang ic3 aiger
+       verilog vhdl smvlang ic3 aiger vlindex
 
 EBMC_DIR:=$(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 CPROVER_DIR:=../lib/cbmc/src
 
-all: hw-cbmc.dir ebmc.dir
+all: hw-cbmc.dir ebmc.dir vlindex.dir
 
 .PHONY: $(patsubst %, %.dir, $(DIRS))
 $(patsubst %, %.dir, $(DIRS)):
@@ -25,6 +25,8 @@ endif
 hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
          vhdl.dir smvlang.dir cprover.dir temporal-logic.dir
 
+vlindex.dir: cprover.dir verilog.dir
+
 # building cbmc proper
 .PHONY: cprover.dir
 cprover.dir:

src/verilog/verilog_preprocessor.cpp

@@ -182,6 +182,8 @@ Function: verilog_preprocessort::preprocessor
 
 void verilog_preprocessort::preprocessor()
 {
+  bool error_found = false;
+
   try
   {
     // set up the initial defines
@@ -221,7 +223,18 @@ void verilog_preprocessort::preprocessor()
         // Read a token.
         auto token = tokenizer().next_token();
         if(token == '`')
-          directive();
+        {
+          try
+          {
+            directive();
+          }
+          catch(const verilog_preprocessor_errort &e)
+          {
+            error().source_location = context().make_source_location();
+            error() << e.what() << eom;
+            error_found = true;
+          }
+        }
         else if(condition)
         {
           auto a_it = context().define_arguments.find(token.text);
@@ -256,8 +269,11 @@ void verilog_preprocessort::preprocessor()
     if(!context_stack.empty())
       error().source_location = context().make_source_location();
     error() << e.what() << eom;
-    throw 0;
+    error_found = true;
   }
+
+  if(error_found)
+    throw 0;
 }
 
 /*******************************************************************\

src/vlindex/Makefile

@@ -0,0 +1,26 @@
+SRC = \
+      verilog_indexer.cpp \
+      vlindex_main.cpp \
+      vlindex_parse_options.cpp \
+      #empty line
+
+OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \
+      $(CPROVER_DIR)/langapi/langapi$(LIBEXT) \
+      $(CPROVER_DIR)/big-int/big-int$(LIBEXT) \
+      ../verilog/verilog$(LIBEXT)
+
+include ../config.inc
+include ../common
+
+CLEANFILES = vlindex$(EXEEXT)
+
+all: vlindex$(EXEEXT)
+
+ifdef DEBUG
+CXXFLAGS += -DDEBUG
+endif
+
+###############################################################################
+
+vlindex$(EXEEXT): $(OBJ)
+	$(LINKBIN)