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

Update to latest Verific with extensions for initial assertions

This commit is contained in:
Miodrag Milanovic 2021-07-09 09:02:27 +02:00
parent 4446cfa524
commit 7a5ac90985
2 changed files with 10 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -498,7 +498,7 @@ endif
ifeq ($(ENABLE_VERIFIC),1) ifeq ($(ENABLE_VERIFIC),1)
VERIFIC_DIR ?= /usr/local/src/verific_lib VERIFIC_DIR ?= /usr/local/src/verific_lib
VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree extensions
CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC
ifeq ($(OS), Darwin) ifeq ($(OS), Darwin)
LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)) -lz LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)) -lz

23
frontends/verific/verific.cc
View File

@ -50,15 +50,13 @@ USING_YOSYS_NAMESPACE
#include "VhdlUnits.h" #include "VhdlUnits.h"
#include "VeriLibrary.h" #include "VeriLibrary.h"
#if defined(YOSYSHQ_VERIFIC_INITSTATE) || defined(YOSYSHQ_VERIFIC_TEMPLATES) || defined(YOSYSHQ_VERIFIC_FORMALAPPS) #include "InitialAssertions.h"
#include "VeriExtensions.h"
#endif
#ifndef YOSYSHQ_VERIFIC_API_VERSION #ifndef YOSYSHQ_VERIFIC_API_VERSION
# error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific." # error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
#endif #endif
#if YOSYSHQ_VERIFIC_API_VERSION < 20210103 #if YOSYSHQ_VERIFIC_API_VERSION < 20210602
# error "Please update your version of YosysHQ flavored Verific." # error "Please update your version of YosysHQ flavored Verific."
#endif #endif
@ -1474,9 +1472,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue; continue;
} }
#ifdef YOSYSHQ_VERIFIC_INITSTATE
if (inst->Type() == PRIM_YOSYSHQ_INITSTATE) if (inst->Type() == PRIM_YOSYSHQ_INITSTATE)
{ {
if (verific_verbose)
log(" adding YosysHQ init state\n");
SigBit initstate = module->Initstate(new_verific_id(inst)); SigBit initstate = module->Initstate(new_verific_id(inst));
SigBit sig_o = net_map_at(inst->GetOutput()); SigBit sig_o = net_map_at(inst->GetOutput());
module->connect(sig_o, initstate); module->connect(sig_o, initstate);
@ -1484,7 +1483,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (!mode_keep) if (!mode_keep)
continue; continue;
} }
#endif
if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (!mode_keep && verific_sva_prims.count(inst->Type())) {
if (verific_verbose) if (verific_verbose)
log(" skipping SVA cell in non k-mode\n"); log(" skipping SVA cell in non k-mode\n");
@ -1962,10 +1961,8 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
for (const auto &i : parameters) for (const auto &i : parameters)
verific_params.Insert(i.first.c_str(), i.second.c_str()); verific_params.Insert(i.first.c_str(), i.second.c_str());
#ifdef YOSYSHQ_VERIFIC_INITSTATE InitialAssertions::Rewrite("work");
InitialAssertionRewriter rw;
rw.RegisterCallBack();
#endif
if (top.empty()) { if (top.empty()) {
netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params); netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
} }
@ -2850,10 +2847,8 @@ struct VerificPass : public Pass {
std::set<std::string> top_mod_names; std::set<std::string> top_mod_names;
#ifdef YOSYSHQ_VERIFIC_INITSTATE InitialAssertions::Rewrite(work);
InitialAssertionRewriter rw;
rw.RegisterCallBack();
#endif
if (mode_all) if (mode_all)
{ {
log("Running hier_tree::ElaborateAll().\n"); log("Running hier_tree::ElaborateAll().\n");