riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #4459 from YosysHQ/micko/vanilla_verific 

Verific build support improvements
This commit is contained in:
Miodrag Milanović 2024-06-18 10:50:20 +02:00 committed by GitHub
parent 74a1dd99ac dfde792288
commit 8024688b1d
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 393 additions and 285 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
Makefile
View File

@ -17,10 +17,12 @@ ENABLE_READLINE := 1
ENABLE_EDITLINE := 0
ENABLE_GHDL := 0
ENABLE_VERIFIC := 0
ENABLE_VERIFIC_SYSTEMVERILOG := 1
ENABLE_VERIFIC_VHDL := 1
ENABLE_VERIFIC_HIER_TREE := 1
ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1
ENABLE_VERIFIC_EDIF := 0
ENABLE_VERIFIC_LIBERTY := 0
DISABLE_VERIFIC_EXTENSIONS := 0
DISABLE_VERIFIC_VHDL := 0
ENABLE_COVER := 1
ENABLE_LIBYOSYS := 0
ENABLE_ZLIB := 1
@ -471,8 +473,24 @@ endif
LIBS_VERIFIC =
ifeq ($(ENABLE_VERIFIC),1)
VERIFIC_DIR ?= /usr/local/src/verific_lib
VERIFIC_COMPONENTS ?= verilog database util containers hier_tree
ifneq ($(DISABLE_VERIFIC_VHDL),1)
VERIFIC_COMPONENTS ?= database util containers
ifeq ($(ENABLE_VERIFIC_HIER_TREE),1)
VERIFIC_COMPONENTS += hier_tree
CXXFLAGS += -DVERIFIC_HIER_TREE_SUPPORT
else
ifneq ($(wildcard $(VERIFIC_DIR)/hier_tree),)
VERIFIC_COMPONENTS += hier_tree
endif
endif
ifeq ($(ENABLE_VERIFIC_SYSTEMVERILOG),1)
VERIFIC_COMPONENTS += verilog
CXXFLAGS += -DVERIFIC_SYSTEMVERILOG_SUPPORT
else
ifneq ($(wildcard $(VERIFIC_DIR)/verilog),)
VERIFIC_COMPONENTS += verilog
endif
endif
ifeq ($(ENABLE_VERIFIC_VHDL),1)
VERIFIC_COMPONENTS += vhdl
CXXFLAGS += -DVERIFIC_VHDL_SUPPORT
else
@ -488,9 +506,13 @@ ifeq ($(ENABLE_VERIFIC_LIBERTY),1)
VERIFIC_COMPONENTS += synlib
CXXFLAGS += -DVERIFIC_LIBERTY_SUPPORT
endif
ifneq ($(DISABLE_VERIFIC_EXTENSIONS),1)
ifeq ($(ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS),1)
VERIFIC_COMPONENTS += extensions
CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS
else
ifneq ($(wildcard $(VERIFIC_DIR)/extensions),)
VERIFIC_COMPONENTS += extensions
endif
endif
CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC
ifeq ($(OS), Darwin)

2
frontends/verific/Makefile.inc
View File

@ -10,7 +10,7 @@ EXTRA_TARGETS += share/verific
share/verific:
$(P) rm -rf share/verific.new
$(Q) mkdir -p share/verific.new
ifneq ($(DISABLE_VERIFIC_VHDL),1)
ifeq ($(ENABLE_VERIFIC_VHDL),1)
$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1987/. share/verific.new/vhdl_vdbs_1987
$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1993/. share/verific.new/vhdl_vdbs_1993
$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_2008/. share/verific.new/vhdl_vdbs_2008

638
frontends/verific/verific.cc
View File

File diff suppressed because it is too large Load Diff

6
frontends/verific/verificsva.cc
View File

@ -80,6 +80,7 @@ USING_YOSYS_NAMESPACE
using namespace Verific;
#endif
#ifdef VERIFIC_SYSTEMVERILOG_SUPPORT
PRIVATE_NAMESPACE_BEGIN
// Non-deterministic FSM
@ -1878,5 +1879,8 @@ bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net)
worker.importer = importer;
return worker.net_to_ast_driver(net) != nullptr;
}
#else
YOSYS_NAMESPACE_BEGIN
pool<int> verific_sva_prims = {};
#endif
YOSYS_NAMESPACE_END