Skip to content

Commit

Permalink
Verilog: introduce the Verilog indexer
Browse files Browse the repository at this point in the history
This adds a recusive decent parser for quicky indexing large quantities of
Verilog, tolerating parsing errors, for the purpose of creating overview
data very quickly.  A new executable, vlindex, is added to output it.
  • Loading branch information
kroening committed Apr 17, 2024
1 parent d3071f4 commit 7eb881c
Show file tree
Hide file tree
Showing 10 changed files with 1,259 additions and 2 deletions.
8 changes: 8 additions & 0 deletions regression/verilog/case/nested_case1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
nested_case1.v
--bound 0
^EXIT=0$
^SIGNAL=0$
^\[main.property.p1\] .* PROVED up to bound 0$
--
^warning: ignoring
17 changes: 17 additions & 0 deletions regression/verilog/case/nested_case1.v
Original file line number Diff line number Diff line change
@@ -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
6 changes: 4 additions & 2 deletions src/Makefile
Original file line number Diff line number Diff line change
@@ -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)):
Expand All @@ -21,6 +21,8 @@ ebmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir vhdl.dir \
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:
Expand Down
2 changes: 2 additions & 0 deletions src/verilog/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ SRC = expr2verilog.cpp \
verilog_elaborate.cpp \
verilog_expr.cpp \
verilog_generate.cpp \
verilog_indexer.cpp \
verilog_interfaces.cpp \
verilog_interpreter.cpp \
verilog_language.cpp \
Expand Down Expand Up @@ -53,4 +54,5 @@ verilog_preprocessor_lex.yy.cpp: verilog_preprocessor_tokenizer.l
# extra dependencies
verilog_y.tab$(OBJEXT): verilog_y.tab.cpp verilog_y.tab.h
verilog_lex.yy$(OBJEXT): verilog_y.tab.cpp verilog_lex.yy.cpp verilog_y.tab.h
verilog_indexer.cpp: verilog_y.tab.h

Loading

0 comments on commit 7eb881c

Please sign in to comment.