From 2ca8d483dde46e72f17f862ca117e2dd944e9709 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 9 Feb 2017 12:53:46 +0100 Subject: Add "rand" and "rand const" verific support --- frontends/verific/verific.cc | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) (limited to 'frontends') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index f3b997dc5..3f5cf3f5f 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -617,6 +617,9 @@ struct VerificImporter module->fixup_ports(); + pool anyconst_nets; + pool anyseq_nets; + FOREACH_NET_OF_NETLIST(nl, mi, net) { if (net->IsRamNet()) @@ -646,6 +649,15 @@ struct VerificImporter continue; } + const char *rand_const_attr = net->GetAttValue(" rand_const"); + const char *rand_attr = net->GetAttValue(" rand"); + + if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1")) + anyconst_nets.insert(net); + + else if (rand_attr != nullptr && !strcmp(rand_attr, "1")) + anyseq_nets.insert(net); + if (net_map.count(net)) { // log(" skipping net %s.\n", net->Name()); continue; @@ -700,8 +712,37 @@ struct VerificImporter { // log(" skipping netbus %s.\n", netbus->Name()); } + + SigSpec anyconst_sig; + SigSpec anyseq_sig; + + for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) { + net = netbus->ElementAtIndex(i); + if (net != nullptr && anyconst_nets.count(net)) { + anyconst_sig.append(net_map.at(net)); + anyconst_nets.erase(net); + } + if (net != nullptr && anyseq_nets.count(net)) { + anyseq_sig.append(net_map.at(net)); + anyseq_nets.erase(net); + } + if (i == netbus->LeftIndex()) + break; + } + + if (GetSize(anyconst_sig)) + module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig))); + + if (GetSize(anyseq_sig)) + module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig))); } + for (auto net : anyconst_nets) + module->connect(net_map.at(net), module->Anyconst(NEW_ID)); + + for (auto net : anyseq_nets) + module->connect(net_map.at(net), module->Anyseq(NEW_ID)); + FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) { if (inst->Type() == PRIM_SVA_POSEDGE) { -- cgit v1.2.3 From 848062088cfc702ba2f4616e1091f63c636bbe5b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 9 Feb 2017 13:51:44 +0100 Subject: Add checker support to verilog front-end --- frontends/verilog/verilog_lexer.l | 20 +++++++++++--------- frontends/verilog/verilog_parser.y | 15 +++++++++++++-- 2 files changed, 24 insertions(+), 11 deletions(-) (limited to 'frontends') diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 97af0ae2d..ff2fa5753 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -175,15 +175,17 @@ YOSYS_NAMESPACE_END "always_ff" { SV_KEYWORD(TOK_ALWAYS); } "always_latch" { SV_KEYWORD(TOK_ALWAYS); } -"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); } -"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); } -"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); } -"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); } -"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); } -"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); } -"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); } -"logic" { SV_KEYWORD(TOK_REG); } -"bit" { SV_KEYWORD(TOK_REG); } +"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); } +"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); } +"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); } +"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); } +"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); } +"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); } +"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); } +"checker" { if (formal_mode) return TOK_CHECKER; SV_KEYWORD(TOK_CHECKER); } +"endchecker" { if (formal_mode) return TOK_ENDCHECKER; SV_KEYWORD(TOK_ENDCHECKER); } +"logic" { SV_KEYWORD(TOK_REG); } +"bit" { SV_KEYWORD(TOK_REG); } "input" { return TOK_INPUT; } "output" { return TOK_OUTPUT; } diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 3eb03dfd8..1879ff441 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -116,7 +116,7 @@ static void free_attr(std::map *al) %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME %token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF -%token TOK_RAND TOK_CONST +%token TOK_RAND TOK_CONST TOK_CHECKER TOK_ENDCHECKER %type range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int %type wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list @@ -465,7 +465,18 @@ module_body: module_body_stmt: task_func_decl | param_decl | localparam_decl | defparam_decl | wire_decl | assign_stmt | cell_stmt | - always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property; + always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property | checker_decl; + +checker_decl: + TOK_CHECKER TOK_ID ';' { + AstNode *node = new AstNode(AST_GENBLOCK); + node->str = *$2; + ast_stack.back()->children.push_back(node); + ast_stack.push_back(node); + } module_body TOK_ENDCHECKER { + delete $2; + ast_stack.pop_back(); + }; task_func_decl: attr TOK_DPI_FUNCTION TOK_ID TOK_ID { -- cgit v1.2.3 From eb7b18e897ac908e960bee6c976f744043590881 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Feb 2017 11:09:07 +0100 Subject: Fix extremely stupid typo --- frontends/verific/verific.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'frontends') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 3f5cf3f5f..306bc5d82 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -774,7 +774,7 @@ struct VerificImporter SigBit outsig = net_map.at(out); log_assert(outsig.wire && GetSize(outsig.wire) == 1); - outsig.wire->attributes["\\init"] == Const(0, 1); + outsig.wire->attributes["\\init"] = Const(0, 1); module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out)); continue; -- cgit v1.2.3 From 0b7aac645c482e9f8e80fb74b61b5c9c6c378857 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Feb 2017 11:39:50 +0100 Subject: Improve handling of Verific warnings and error messages --- frontends/verific/verific.cc | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'frontends') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 306bc5d82..36e44fe01 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -57,7 +57,7 @@ PRIVATE_NAMESPACE_BEGIN void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) { - log("VERIFIC-%s [%s] ", + string message = stringf("VERIFIC-%s [%s] ", msg_type == VERIFIC_NONE ? "NONE" : msg_type == VERIFIC_ERROR ? "ERROR" : msg_type == VERIFIC_WARNING ? "WARNING" : @@ -65,10 +65,16 @@ void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefil msg_type == VERIFIC_INFO ? "INFO" : msg_type == VERIFIC_COMMENT ? "COMMENT" : msg_type == VERIFIC_PROGRAM_ERROR ? "PROGRAM_ERROR" : "UNKNOWN", message_id); + if (linefile) - log("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile)); - logv(msg, args); - log("\n"); + message += stringf("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile)); + + message += vstringf(msg, args); + + if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR) + log_warning("%s\n", message.c_str()); + else + log("%s\n", message.c_str()); } struct VerificImporter -- cgit v1.2.3 From fa4a7efe15ccfca6c8200107284d02ee4ddabb9c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Feb 2017 11:40:18 +0100 Subject: Add verific support for initialized variables --- frontends/verific/verific.cc | 50 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 47 insertions(+), 3 deletions(-) (limited to 'frontends') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 36e44fe01..9af4ce047 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -623,6 +623,7 @@ struct VerificImporter module->fixup_ports(); + dict init_nets; pool anyconst_nets; pool anyseq_nets; @@ -655,6 +656,9 @@ struct VerificImporter continue; } + if (net->GetInitialValue()) + init_nets[net] = net->GetInitialValue(); + const char *rand_const_attr = net->GetAttValue(" rand_const"); const char *rand_attr = net->GetAttValue(" rand"); @@ -701,18 +705,38 @@ struct VerificImporter wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex()); import_attributes(wire->attributes, netbus); - for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) { - if (netbus->ElementAtIndex(i)) { + RTLIL::Const initval = Const(State::Sx, GetSize(wire)); + bool initval_valid = false; + + for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) + { + if (netbus->ElementAtIndex(i)) + { + int bitidx = i - wire->start_offset; net = netbus->ElementAtIndex(i); - RTLIL::SigBit bit(wire, i - wire->start_offset); + RTLIL::SigBit bit(wire, bitidx); + + if (init_nets.count(net)) { + if (init_nets.at(net) == '0') + initval.bits.at(bitidx) = State::S0; + if (init_nets.at(net) == '1') + initval.bits.at(bitidx) = State::S1; + initval_valid = true; + init_nets.erase(net); + } + if (net_map.count(net) == 0) net_map[net] = bit; else module->connect(bit, net_map.at(net)); } + if (i == netbus->RightIndex()) break; } + + if (initval_valid) + wire->attributes["\\init"] = initval; } else { @@ -743,6 +767,26 @@ struct VerificImporter module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig))); } + for (auto it : init_nets) + { + Const initval; + SigBit bit = net_map.at(it.first); + log_assert(bit.wire); + + if (bit.wire->attributes.count("\\init")) + initval = bit.wire->attributes.at("\\init"); + + while (GetSize(initval) < GetSize(bit.wire)) + initval.bits.push_back(State::Sx); + + if (it.second == '0') + initval.bits.at(bit.offset) = State::S0; + if (it.second == '1') + initval.bits.at(bit.offset) = State::S1; + + bit.wire->attributes["\\init"] = initval; + } + for (auto net : anyconst_nets) module->connect(net_map.at(net), module->Anyconst(NEW_ID)); -- cgit v1.2.3 From c449f4b86f66ca4ef2396454f09a73d56ff06512 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Feb 2017 11:47:51 +0100 Subject: Fix another stupid bug in the same line --- frontends/verific/verific.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'frontends') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 9af4ce047..cde72a8e3 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -824,7 +824,7 @@ struct VerificImporter SigBit outsig = net_map.at(out); log_assert(outsig.wire && GetSize(outsig.wire) == 1); - outsig.wire->attributes["\\init"] = Const(0, 1); + outsig.wire->attributes["\\init"] = Const(1, 1); module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out)); continue; -- cgit v1.2.3 From cdb6ceb8c63f2c38bdba3f66be7c444def43897e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 11 Feb 2017 15:57:36 +0100 Subject: Add support for verific mem initialization --- frontends/verific/verific.cc | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) (limited to 'frontends') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index cde72a8e3..bc0bd60fc 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -653,6 +653,44 @@ struct VerificImporter memory->width = bits_in_word; memory->size = number_of_bits / bits_in_word; + + const char *ascii_initdata = net->GetWideInitialValue(); + if (ascii_initdata) { + while (*ascii_initdata != 0 && *ascii_initdata != '\'') + ascii_initdata++; + if (*ascii_initdata == '\'') + ascii_initdata++; + if (*ascii_initdata != 0) { + log_assert(*ascii_initdata == 'b'); + ascii_initdata++; + } + for (int word_idx = 0; word_idx < memory->size; word_idx++) { + Const initval = Const(State::Sx, memory->width); + bool initval_valid = false; + for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) { + if (*ascii_initdata == 0) + break; + if (*ascii_initdata == '0' || *ascii_initdata == '1') { + initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1; + initval_valid = true; + } + ascii_initdata++; + } + if (initval_valid) { + RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit"); + cell->parameters["\\WORDS"] = 1; + if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound()) + cell->setPort("\\ADDR", word_idx); + else + cell->setPort("\\ADDR", memory->size - word_idx - 1); + cell->setPort("\\DATA", initval); + cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str()); + cell->parameters["\\ABITS"] = 32; + cell->parameters["\\WIDTH"] = memory->width; + cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1); + } + } + } continue; } -- cgit v1.2.3