mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-27 02:45:52 +00:00
Code Activity

Merge branch 'eddie/clkpart' into xaig_dff

Browse source
This commit is contained in:
Eddie Hung 2019-11-22 15:38:48 -08:00
commit bd56161775
15 changed files with 591 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

17
frontends/verific/verific.cc
View file

@ -130,7 +130,7 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
bool is_blackbox(Netlist *nl)
{
if (nl->IsBlackBox())
if (nl->IsBlackBox() || nl->IsEmptyBox())
return true;
const char *attr = nl->GetAttValue("blackbox");
@ -784,15 +784,15 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
merge_past_ffs_clock(it.second, it.first.first, it.first.second);
}
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
{
std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
std::string module_name = netlist_name;
if (nl->IsOperator()) {
if (nl->IsOperator() || nl->IsPrimitive()) {
module_name = "$verific$" + module_name;
} else {
if (*nl->Name()) {
if (!norename && *nl->Name()) {
module_name += "(";
module_name += nl->Name();
module_name += ")";
@ -1409,7 +1409,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
std::string inst_type = inst->View()->Owner()->Name();
if (inst->View()->IsOperator()) {
if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) {
inst_type = "$verific$" + inst_type;
} else {
if (*inst->View()->Name()) {
@ -1899,7 +1899,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
VerificImporter importer(false, false, false, false, false, false, false);
importer.import_netlist(design, nl, nl_todo);
importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top);
}
nl_todo.erase(nl);
nl_done.insert(nl);
@ -2373,6 +2373,8 @@ struct VerificPass : public Pass {
if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
cmd_error(args, argidx, "unknown option");
std::set<std::string> top_mod_names;
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");
@ -2401,6 +2403,7 @@ struct VerificPass : public Pass {
for (; argidx < GetSize(args); argidx++)
{
const char *name = args[argidx].c_str();
top_mod_names.insert(name);
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
if (veri_lib) {
@ -2466,7 +2469,7 @@ struct VerificPass : public Pass {
if (nl_done.count(nl) == 0) {
VerificImporter importer(mode_gates, mode_keep, mode_nosva,
mode_names, mode_verific, mode_autocover, mode_fullinit);
importer.import_netlist(design, nl, nl_todo);
importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name()));
}
nl_todo.erase(nl);
nl_done.insert(nl);

2
frontends/verific/verific.h
View file

@ -93,7 +93,7 @@ struct VerificImporter
void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo, bool norename = false);
};
void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst);

42
frontends/verific/verificsva.cc
View file

@ -36,6 +36,8 @@
// basic_property:
// sequence
// not basic_property
// nexttime basic_property
// nexttime[N] basic_property
// sequence #-# basic_property
// sequence #=# basic_property
// basic_property or basic_property (cover only)
@ -1264,6 +1266,26 @@ struct VerificSvaImporter
return node;
}
if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
{
const char *sva_low_s = inst->GetAttValue("sva:low");
const char *sva_high_s = inst->GetAttValue("sva:high");
int sva_low = atoi(sva_low_s);
int sva_high = atoi(sva_high_s);
log_assert(sva_low == sva_high);
int node = start_node;
for (int i = 0; i < sva_low; i++) {
int next_node = fsm.createNode();
fsm.createEdge(node, next_node);
node = next_node;
}
return parse_sequence(fsm, node, inst->GetInput());
}
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
{
const char *sva_low_s = inst->GetAttValue("sva:low");
@ -1590,15 +1612,25 @@ struct VerificSvaImporter
Instance *consequent_inst = net_to_ast_driver(consequent_net);
if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH ||
consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS))
{
bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
Net *until_net = consequent_inst->GetInput2();
consequent_net = consequent_inst->GetInput1();
consequent_inst = net_to_ast_driver(consequent_net);
Net *until_net = nullptr;
if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)
{
consequent_net = consequent_inst->GetInput();
consequent_inst = net_to_ast_driver(consequent_net);
}
else
{
until_net = consequent_inst->GetInput2();
consequent_net = consequent_inst->GetInput1();
consequent_inst = net_to_ast_driver(consequent_net);
}
SigBit until_sig = parse_expression(until_net);
SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0;
SigBit not_until_sig = module->Not(NEW_ID, until_sig);
antecedent_fsm.createEdge(node, node, not_until_sig);

6
frontends/verilog/verilog_lexer.l
View file

@ -188,9 +188,9 @@ YOSYS_NAMESPACE_END
"unique0" { SV_KEYWORD(TOK_UNIQUE); }
"priority" { SV_KEYWORD(TOK_PRIORITY); }
"always_comb" { SV_KEYWORD(TOK_ALWAYS); }
"always_ff" { SV_KEYWORD(TOK_ALWAYS); }
"always_latch" { SV_KEYWORD(TOK_ALWAYS); }
"always_comb" { SV_KEYWORD(TOK_ALWAYS_COMB); }
"always_ff" { SV_KEYWORD(TOK_ALWAYS_FF); }
"always_latch" { SV_KEYWORD(TOK_ALWAYS_LATCH); }
/* use special token for labels on assert, assume, cover, and restrict because it's insanley complex
to fix parsing of cells otherwise. (the current cell parser forces a reduce very early to update some

39
frontends/verilog/verilog_parser.y
View file

@ -141,6 +141,7 @@ struct specify_rise_fall {
%token TOK_INTERFACE TOK_ENDINTERFACE TOK_MODPORT TOK_VAR
%token TOK_INPUT TOK_OUTPUT TOK_INOUT TOK_WIRE TOK_WAND TOK_WOR TOK_REG TOK_LOGIC
%token TOK_INTEGER TOK_SIGNED TOK_ASSIGN TOK_ALWAYS TOK_INITIAL
%token TOK_ALWAYS_FF TOK_ALWAYS_COMB TOK_ALWAYS_LATCH
%token TOK_BEGIN TOK_END TOK_IF TOK_ELSE TOK_FOR TOK_WHILE TOK_REPEAT
%token TOK_DPI_FUNCTION TOK_POSEDGE TOK_NEGEDGE TOK_OR TOK_AUTOMATIC
%token TOK_CASE TOK_CASEX TOK_CASEZ TOK_ENDCASE TOK_DEFAULT
@ -156,7 +157,7 @@ struct specify_rise_fall {
%type <ast> range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int
%type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
%type <string> opt_label opt_sva_label tok_prim_wrapper hierarchical_id hierarchical_type_id
%type <boolean> opt_signed opt_property unique_case_attr
%type <boolean> opt_signed opt_property unique_case_attr always_comb_or_latch always_or_always_ff
%type <al> attr case_attr
%type <specify_target_ptr> specify_target
@ -1581,10 +1582,28 @@ cell_port:
free_attr($1);
};
always_comb_or_latch:
TOK_ALWAYS_COMB {
$$ = false;
} |
TOK_ALWAYS_LATCH {
$$ = true;
};
always_or_always_ff:
TOK_ALWAYS {
$$ = false;
} |
TOK_ALWAYS_FF {
$$ = true;
};
always_stmt:
attr TOK_ALWAYS {
attr always_or_always_ff {
AstNode *node = new AstNode(AST_ALWAYS);
append_attr(node, $1);
if ($2)
node->attributes[ID(always_ff)] = AstNode::mkconst_int(1, false);
ast_stack.back()->children.push_back(node);
ast_stack.push_back(node);
} always_cond {
@ -1595,6 +1614,22 @@ always_stmt:
ast_stack.pop_back();
ast_stack.pop_back();
} |
attr always_comb_or_latch {
AstNode *node = new AstNode(AST_ALWAYS);
append_attr(node, $1);
if ($2)
node->attributes[ID(always_latch)] = AstNode::mkconst_int(1, false);
else
node->attributes[ID(always_comb)] = AstNode::mkconst_int(1, false);
ast_stack.back()->children.push_back(node);
ast_stack.push_back(node);
AstNode *block = new AstNode(AST_BLOCK);
ast_stack.back()->children.push_back(block);
ast_stack.push_back(block);
} behavioral_stmt {
ast_stack.pop_back();
ast_stack.pop_back();
} |
attr TOK_INITIAL {
AstNode *node = new AstNode(AST_INITIAL);
append_attr(node, $1);