diff options
Diffstat (limited to 'frontends')
-rw-r--r-- | frontends/ast/ast.cc | 2 | ||||
-rw-r--r-- | frontends/ast/ast.h | 1 | ||||
-rw-r--r-- | frontends/ast/genrtlil.cc | 34 | ||||
-rw-r--r-- | frontends/ast/simplify.cc | 229 | ||||
-rw-r--r-- | frontends/blif/blifparse.cc | 5 | ||||
-rw-r--r-- | frontends/json/jsonparse.cc | 34 | ||||
-rw-r--r-- | frontends/verific/README | 2 | ||||
-rw-r--r-- | frontends/verific/verific.cc | 602 | ||||
-rw-r--r-- | frontends/verific/verific.h | 3 | ||||
-rw-r--r-- | frontends/verific/verificsva.cc | 12 | ||||
-rw-r--r-- | frontends/verilog/preproc.cc | 10 | ||||
-rw-r--r-- | frontends/verilog/verilog_lexer.l | 15 | ||||
-rw-r--r-- | frontends/verilog/verilog_parser.y | 5 |
13 files changed, 574 insertions, 380 deletions
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 7be8ab565..6097f02f5 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -344,7 +344,7 @@ void AstNode::dumpAst(FILE *f, std::string indent) const } if (!multirange_swapped.empty()) { fprintf(f, " multirange_swapped=["); - for (auto v : multirange_swapped) + for (bool v : multirange_swapped) fprintf(f, " %d", v); fprintf(f, " ]"); } diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index 48ec9a063..80497c131 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -268,6 +268,7 @@ namespace AST struct varinfo_t { RTLIL::Const val; int offset; + bool range_swapped; bool is_signed; AstNode *arg = nullptr; bool explicitly_sized; diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index ed709aa33..d81c53dfb 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -877,7 +877,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun this_width = id_ast->children[0]->range_left - id_ast->children[0]->range_right + 1; if (children.size() > 1) range = children[1]; - } else if (id_ast->type == AST_STRUCT_ITEM) { + } else if (id_ast->type == AST_STRUCT_ITEM || id_ast->type == AST_STRUCT) { AstNode *tmp_range = make_struct_member_range(this, id_ast); this_width = tmp_range->range_left - tmp_range->range_right + 1; delete tmp_range; @@ -932,7 +932,8 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun if (children.at(0)->type != AST_CONSTANT) log_file_error(filename, location.first_line, "Static cast with non constant expression!\n"); children.at(1)->detectSignWidthWorker(width_hint, sign_hint); - width_hint = children.at(0)->bitsAsConst().as_int(); + this_width = children.at(0)->bitsAsConst().as_int(); + width_hint = max(width_hint, this_width); if (width_hint <= 0) log_file_error(filename, location.first_line, "Static cast with zero or negative size!\n"); break; @@ -1083,15 +1084,20 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun sub_sign_hint = true; children.at(0)->detectSignWidthWorker(sub_width_hint, sub_sign_hint); width_hint = max(width_hint, sub_width_hint); - sign_hint = false; + sign_hint &= sub_sign_hint; } break; } + if (str == "\\$size" || str == "\\$bits" || str == "\\$high" || str == "\\$low" || str == "\\$left" || str == "\\$right") { + width_hint = max(width_hint, 32); + break; + } if (current_scope.count(str)) { // This width detection is needed for function calls which are - // unelaborated, which currently only applies to calls to recursive - // functions reached by unevaluated ternary branches. + // unelaborated, which currently applies to calls to functions + // reached via unevaluated ternary branches or used in case or case + // item expressions. const AstNode *func = current_scope.at(str); if (func->type != AST_FUNCTION) log_file_error(filename, location.first_line, "Function call to %s resolved to something that isn't a function!\n", RTLIL::unescape_id(str).c_str()); @@ -1102,8 +1108,8 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun break; } log_assert(wire && wire->type == AST_WIRE); - sign_hint = wire->is_signed; - width_hint = 1; + sign_hint &= wire->is_signed; + int result_width = 1; if (!wire->children.empty()) { log_assert(wire->children.size() == 1); @@ -1116,10 +1122,11 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun if (left->type != AST_CONSTANT || right->type != AST_CONSTANT) log_file_error(filename, location.first_line, "Function %s has non-constant width!", RTLIL::unescape_id(str).c_str()); - width_hint = abs(int(left->asInt(true) - right->asInt(true))); + result_width = abs(int(left->asInt(true) - right->asInt(true))); delete left; delete right; } + width_hint = max(width_hint, result_width); break; } YS_FALLTHROUGH @@ -1525,13 +1532,20 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) // changing the size of signal can be done directly using RTLIL::SigSpec case AST_CAST_SIZE: { RTLIL::SigSpec size = children[0]->genRTLIL(); - RTLIL::SigSpec sig = children[1]->genRTLIL(); if (!size.is_fully_const()) log_file_error(filename, location.first_line, "Static cast with non constant expression!\n"); int width = size.as_int(); if (width <= 0) log_file_error(filename, location.first_line, "Static cast with zero or negative size!\n"); - sig.extend_u0(width, sign_hint); + // determine the *signedness* of the expression + int sub_width_hint = -1; + bool sub_sign_hint = true; + children[1]->detectSignWidth(sub_width_hint, sub_sign_hint); + // generate the signal given the *cast's* size and the + // *expression's* signedness + RTLIL::SigSpec sig = children[1]->genWidthRTLIL(width, sub_sign_hint); + // context may effect this node's signedness, but not that of the + // casted expression is_signed = sign_hint; return sig; } diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 777f46bd7..2d9d6dc79 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -307,6 +307,10 @@ static int size_packed_struct(AstNode *snode, int base_offset) if (node->type == AST_STRUCT || node->type == AST_UNION) { // embedded struct or union width = size_packed_struct(node, base_offset + offset); + // set range of struct + node->range_right = base_offset + offset; + node->range_left = base_offset + offset + width - 1; + node->range_valid = true; } else { log_assert(node->type == AST_STRUCT_ITEM); @@ -493,14 +497,12 @@ static void add_members_to_scope(AstNode *snode, std::string name) // in case later referenced in assignments log_assert(snode->type==AST_STRUCT || snode->type==AST_UNION); for (auto *node : snode->children) { + auto member_name = name + "." + node->str; + current_scope[member_name] = node; if (node->type != AST_STRUCT_ITEM) { // embedded struct or union add_members_to_scope(node, name + "." + node->str); } - else { - auto member_name = name + "." + node->str; - current_scope[member_name] = node; - } } } @@ -673,6 +675,128 @@ void add_wire_for_ref(const RTLIL::Wire *ref, const std::string &str) current_scope[str] = wire; } +enum class IdentUsage { + NotReferenced, // target variable is neither read or written in the block + Assigned, // target variable is always assigned before use + SyncRequired, // target variable may be used before it has been assigned +}; + +// determines whether a local variable a block is always assigned before it is +// used, meaning the nosync attribute can automatically be added to that +// variable +static IdentUsage always_asgn_before_use(const AstNode *node, const std::string &target) +{ + // This variable has been referenced before it has necessarily been assigned + // a value in this procedure. + if (node->type == AST_IDENTIFIER && node->str == target) + return IdentUsage::SyncRequired; + + // For case statements (which are also used for if/else), we check each + // possible branch. If the variable is assigned in all branches, then it is + // assigned, and a sync isn't required. If it used before assignment in any + // branch, then a sync is required. + if (node->type == AST_CASE) { + bool all_defined = true; + bool any_used = false; + bool has_default = false; + for (const AstNode *child : node->children) { + if (child->type == AST_COND && child->children.at(0)->type == AST_DEFAULT) + has_default = true; + IdentUsage nested = always_asgn_before_use(child, target); + if (nested != IdentUsage::Assigned && child->type == AST_COND) + all_defined = false; + if (nested == IdentUsage::SyncRequired) + any_used = true; + } + if (any_used) + return IdentUsage::SyncRequired; + else if (all_defined && has_default) + return IdentUsage::Assigned; + else + return IdentUsage::NotReferenced; + } + + // Check if this is an assignment to the target variable. For simplicity, we + // don't analyze sub-ranges of the variable. + if (node->type == AST_ASSIGN_EQ) { + const AstNode *ident = node->children.at(0); + if (ident->type == AST_IDENTIFIER && ident->str == target) + return IdentUsage::Assigned; + } + + for (const AstNode *child : node->children) { + IdentUsage nested = always_asgn_before_use(child, target); + if (nested != IdentUsage::NotReferenced) + return nested; + } + return IdentUsage::NotReferenced; +} + +static const std::string auto_nosync_prefix = "\\AutoNosync"; + +// mark a local variable in an always_comb block for automatic nosync +// consideration +static void mark_auto_nosync(AstNode *block, const AstNode *wire) +{ + log_assert(block->type == AST_BLOCK); + log_assert(wire->type == AST_WIRE); + block->attributes[auto_nosync_prefix + wire->str] = AstNode::mkconst_int(1, + false); +} + +// block names can be prefixed with an explicit scope during elaboration +static bool is_autonamed_block(const std::string &str) { + size_t last_dot = str.rfind('.'); + // unprefixed names: autonamed if the first char is a dollar sign + if (last_dot == std::string::npos) + return str.at(0) == '$'; // e.g., `$fordecl_block$1` + // prefixed names: autonamed if the final chunk begins with a dollar sign + return str.rfind(".$") == last_dot; // e.g., `\foo.bar.$fordecl_block$1` +} + +// check a procedural block for auto-nosync markings, remove them, and add +// nosync to local variables as necessary +static void check_auto_nosync(AstNode *node) +{ + std::vector<RTLIL::IdString> attrs_to_drop; + for (const auto& elem : node->attributes) { + // skip attributes that don't begin with the prefix + if (elem.first.compare(0, auto_nosync_prefix.size(), + auto_nosync_prefix.c_str())) + continue; + + // delete and remove the attribute once we're done iterating + attrs_to_drop.push_back(elem.first); + + // find the wire based on the attribute + std::string wire_name = elem.first.substr(auto_nosync_prefix.size()); + auto it = current_scope.find(wire_name); + if (it == current_scope.end()) + continue; + + // analyze the usage of the local variable in this block + IdentUsage ident_usage = always_asgn_before_use(node, wire_name); + if (ident_usage != IdentUsage::Assigned) + continue; + + // mark the wire with `nosync` + AstNode *wire = it->second; + log_assert(wire->type == AST_WIRE); + wire->attributes[ID::nosync] = AstNode::mkconst_int(1, false); + } + + // remove the attributes we've "consumed" + for (const RTLIL::IdString &str : attrs_to_drop) { + auto it = node->attributes.find(str); + delete it->second; + node->attributes.erase(it); + } + + // check local variables in any nested blocks + for (AstNode *child : node->children) + check_auto_nosync(child); +} + // convert the AST into a simpler AST that has all parameters substituted by their // values, unrolled for-loops, expanded generate blocks, etc. when this function // is done with an AST it can be converted into RTLIL using genRTLIL(). @@ -980,6 +1104,11 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, } } } + + for (AstNode *child : children) + if (child->type == AST_ALWAYS && + child->attributes.count(ID::always_comb)) + check_auto_nosync(child); } // create name resolution entries for all objects with names @@ -1224,6 +1353,16 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, case AST_PARAMETER: case AST_LOCALPARAM: + // if parameter is implicit type which is the typename of a struct or union, + // save information about struct in wiretype attribute + if (children[0]->type == AST_IDENTIFIER && current_scope.count(children[0]->str) > 0) { + auto item_node = current_scope[children[0]->str]; + if (item_node->type == AST_STRUCT || item_node->type == AST_UNION) { + attributes[ID::wiretype] = item_node->clone(); + size_packed_struct(attributes[ID::wiretype], 0); + add_members_to_scope(attributes[ID::wiretype], str); + } + } while (!children[0]->basic_prep && children[0]->simplify(false, false, false, stage, -1, false, true) == true) did_something = true; children[0]->detectSignWidth(width_hint, sign_hint); @@ -1389,11 +1528,10 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, if (const_fold && type == AST_CASE) { - int width_hint; - bool sign_hint; detectSignWidth(width_hint, sign_hint); while (children[0]->simplify(const_fold, at_zero, in_lvalue, stage, width_hint, sign_hint, in_param)) { } if (children[0]->type == AST_CONSTANT && children[0]->bits_only_01()) { + children[0]->is_signed = sign_hint; RTLIL::Const case_expr = children[0]->bitsAsConst(width_hint, sign_hint); std::vector<AstNode*> new_children; new_children.push_back(children[0]); @@ -1903,7 +2041,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, if (name_has_dot(str, sname)) { if (current_scope.count(str) > 0) { auto item_node = current_scope[str]; - if (item_node->type == AST_STRUCT_ITEM) { + if (item_node->type == AST_STRUCT_ITEM || item_node->type == AST_STRUCT) { // structure member, rewrite this node to reference the packed struct wire auto range = make_struct_member_range(this, item_node); newNode = new AstNode(AST_IDENTIFIER, range); @@ -2226,6 +2364,16 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, { expand_genblock(str + "."); + // if this is an autonamed block is in an always_comb + if (current_always && current_always->attributes.count(ID::always_comb) + && is_autonamed_block(str)) + // track local variables in this block so we can consider adding + // nosync once the block has been fully elaborated + for (AstNode *child : children) + if (child->type == AST_WIRE && + !child->attributes.count(ID::nosync)) + mark_auto_nosync(this, child); + std::vector<AstNode*> new_children; for (size_t i = 0; i < children.size(); i++) if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM || children[i]->type == AST_TYPEDEF) { @@ -2579,6 +2727,18 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, while (wire_data->simplify(true, false, false, 1, -1, false, false)) { } current_ast_mod->children.push_back(wire_data); + int shamt_width_hint = -1; + bool shamt_sign_hint = true; + shift_expr->detectSignWidth(shamt_width_hint, shamt_sign_hint); + + AstNode *wire_sel = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(shamt_width_hint-1, true), mkconst_int(0, true))); + wire_sel->str = stringf("$bitselwrite$sel$%s:%d$%d", filename.c_str(), location.first_line, autoidx++); + wire_sel->attributes[ID::nosync] = AstNode::mkconst_int(1, false); + wire_sel->is_logic = true; + wire_sel->is_signed = shamt_sign_hint; + while (wire_sel->simplify(true, false, false, 1, -1, false, false)) { } + current_ast_mod->children.push_back(wire_sel); + did_something = true; newNode = new AstNode(AST_BLOCK); @@ -2595,39 +2755,44 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, ref_data->id2ast = wire_data; ref_data->was_checked = true; + AstNode *ref_sel = new AstNode(AST_IDENTIFIER); + ref_sel->str = wire_sel->str; + ref_sel->id2ast = wire_sel; + ref_sel->was_checked = true; + AstNode *old_data = lvalue->clone(); if (type == AST_ASSIGN_LE) old_data->lookahead = true; - AstNode *shamt = shift_expr; + AstNode *s = new AstNode(AST_ASSIGN_EQ, ref_sel->clone(), shift_expr); + newNode->children.push_back(s); - int shamt_width_hint = 0; - bool shamt_sign_hint = true; - shamt->detectSignWidth(shamt_width_hint, shamt_sign_hint); + AstNode *shamt = ref_sel; + + // convert to signed while preserving the sign and value + shamt = new AstNode(AST_CAST_SIZE, mkconst_int(shamt_width_hint + 1, true), shamt); + shamt = new AstNode(AST_TO_SIGNED, shamt); + // offset the shift amount by the lower bound of the dimension int start_bit = children[0]->id2ast->range_right; - bool use_shift = shamt_sign_hint; + shamt = new AstNode(AST_SUB, shamt, mkconst_int(start_bit, true)); - if (start_bit != 0) { - shamt = new AstNode(AST_SUB, shamt, mkconst_int(start_bit, true)); - use_shift = true; - } + // reflect the shift amount if the dimension is swapped + if (children[0]->id2ast->range_swapped) + shamt = new AstNode(AST_SUB, mkconst_int(source_width - result_width, true), shamt); + + // AST_SHIFT uses negative amounts for shifting left + shamt = new AstNode(AST_NEG, shamt); AstNode *t; t = mkconst_bits(std::vector<RTLIL::State>(result_width, State::S1), false); - if (use_shift) - t = new AstNode(AST_SHIFT, t, new AstNode(AST_NEG, shamt->clone())); - else - t = new AstNode(AST_SHIFT_LEFT, t, shamt->clone()); + t = new AstNode(AST_SHIFT, t, shamt->clone()); t = new AstNode(AST_ASSIGN_EQ, ref_mask->clone(), t); newNode->children.push_back(t); t = new AstNode(AST_BIT_AND, mkconst_bits(std::vector<RTLIL::State>(result_width, State::S1), false), children[1]->clone()); - if (use_shift) - t = new AstNode(AST_SHIFT, t, new AstNode(AST_NEG, shamt)); - else - t = new AstNode(AST_SHIFT_LEFT, t, shamt); + t = new AstNode(AST_SHIFT, t, shamt); t = new AstNode(AST_ASSIGN_EQ, ref_data->clone(), t); newNode->children.push_back(t); @@ -3065,6 +3230,7 @@ skip_dynamic_range_lvalue_expansion:; reg->str = stringf("$past$%s:%d$%d$%d", filename.c_str(), location.first_line, myidx, i); reg->is_reg = true; + reg->is_signed = sign_hint; current_ast_mod->children.push_back(reg); @@ -3284,7 +3450,7 @@ skip_dynamic_range_lvalue_expansion:; else { result = width * mem_depth; } - newNode = mkconst_int(result, false); + newNode = mkconst_int(result, true); goto apply_newNode; } @@ -5009,6 +5175,8 @@ bool AstNode::replace_variables(std::map<std::string, AstNode::varinfo_t> &varia width = min(std::abs(children.at(0)->range_left - children.at(0)->range_right) + 1, width); } offset -= variables.at(str).offset; + if (variables.at(str).range_swapped) + offset = -offset; std::vector<RTLIL::State> &var_bits = variables.at(str).val.bits; std::vector<RTLIL::State> new_bits(var_bits.begin() + offset, var_bits.begin() + offset + width); AstNode *newNode = mkconst_bits(new_bits, variables.at(str).is_signed); @@ -5066,7 +5234,8 @@ AstNode *AstNode::eval_const_function(AstNode *fcall, bool must_succeed) log_file_error(filename, location.first_line, "Incompatible re-declaration of constant function wire %s.\n", stmt->str.c_str()); } variable.val = RTLIL::Const(RTLIL::State::Sx, width); - variable.offset = min(stmt->range_left, stmt->range_right); + variable.offset = stmt->range_swapped ? stmt->range_left : stmt->range_right; + variable.range_swapped = stmt->range_swapped; variable.is_signed = stmt->is_signed; variable.explicitly_sized = stmt->children.size() && stmt->children.back()->type == AST_RANGE; @@ -5151,8 +5320,12 @@ AstNode *AstNode::eval_const_function(AstNode *fcall, bool must_succeed) int width = std::abs(range->range_left - range->range_right) + 1; varinfo_t &v = variables[stmt->children.at(0)->str]; RTLIL::Const r = stmt->children.at(1)->bitsAsConst(v.val.bits.size()); - for (int i = 0; i < width; i++) - v.val.bits.at(i+offset-v.offset) = r.bits.at(i); + for (int i = 0; i < width; i++) { + int index = i + offset - v.offset; + if (v.range_swapped) + index = -index; + v.val.bits.at(index) = r.bits.at(i); + } } delete block->children.front(); diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 19844bda6..73d1f0ea7 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -166,7 +166,10 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool goto error; module = new RTLIL::Module; lastcell = nullptr; - module->name = RTLIL::escape_id(strtok(NULL, " \t\r\n")); + char *name = strtok(NULL, " \t\r\n"); + if (name == nullptr) + goto error; + module->name = RTLIL::escape_id(name); obj_attributes = &module->attributes; obj_parameters = nullptr; if (design->module(module->name)) diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc index 50c25abda..1aab81015 100644 --- a/frontends/json/jsonparse.cc +++ b/frontends/json/jsonparse.cc @@ -60,10 +60,38 @@ struct JsonNode break; if (ch == '\\') { - int ch = f.get(); + ch = f.get(); - if (ch == EOF) - log_error("Unexpected EOF in JSON string.\n"); + switch (ch) { + case EOF: log_error("Unexpected EOF in JSON string.\n"); break; + case '"': + case '/': + case '\\': break; + case 'b': ch = '\b'; break; + case 'f': ch = '\f'; break; + case 'n': ch = '\n'; break; + case 'r': ch = '\r'; break; + case 't': ch = '\t'; break; + case 'u': + int val = 0; + for (int i = 0; i < 4; i++) { + ch = f.get(); + val <<= 4; + if (ch >= '0' && '9' >= ch) { + val += ch - '0'; + } else if (ch >= 'A' && 'F' >= ch) { + val += 10 + ch - 'A'; + } else if (ch >= 'a' && 'f' >= ch) { + val += 10 + ch - 'a'; + } else + log_error("Unexpected non-digit character in \\uXXXX sequence: %c.\n", ch); + } + if (val < 128) + ch = val; + else + log_error("Unsupported \\uXXXX sequence in JSON string: %04X.\n", val); + break; + } } data_string += ch; diff --git a/frontends/verific/README b/frontends/verific/README index 952fb1e0c..921873af3 100644 --- a/frontends/verific/README +++ b/frontends/verific/README @@ -1,7 +1,7 @@ This directory contains Verific bindings for Yosys. -Use Tabby CAD Suite from YosysHQ if you need Yosys+Verifc. +Use Tabby CAD Suite from YosysHQ if you need Yosys+Verific. https://www.yosyshq.com/ Contact YosysHQ at contact@yosyshq.com for free evaluation diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 47020f105..ab527a253 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -53,8 +53,11 @@ USING_YOSYS_NAMESPACE #include "VhdlUnits.h" #endif +#include "VerificStream.h" +#include "FileSystem.h" + #ifdef YOSYSHQ_VERIFIC_EXTENSIONS -#include "InitialAssertions.h" +#include "VerificExtensions.h" #endif #ifndef YOSYSHQ_VERIFIC_API_VERSION @@ -83,7 +86,7 @@ bool verific_import_pending; string verific_error_msg; int verific_sva_fsm_limit; -vector<string> verific_incdirs, verific_libdirs; +vector<string> verific_incdirs, verific_libdirs, verific_libexts; void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) { @@ -118,6 +121,34 @@ string get_full_netlist_name(Netlist *nl) return nl->CellBaseName(); } +class YosysStreamCallBackHandler : public VerificStreamCallBackHandler +{ +public: + YosysStreamCallBackHandler() : VerificStreamCallBackHandler() { } + virtual ~YosysStreamCallBackHandler() { } + + virtual verific_stream *GetSysCallStream(const char *file_path) + { + if (!file_path) return nullptr; + + linefile_type src_loc = GetFromLocation(); + + char *this_file_name = nullptr; + if (src_loc && !FileSystem::IsAbsolutePath(file_path)) { + const char *src_file_name = LineFile::GetFileName(src_loc); + char *dir_name = FileSystem::DirectoryPath(src_file_name); + if (dir_name) { + this_file_name = Strings::save(dir_name, "/", file_path); + Strings::free(dir_name); + file_path = this_file_name; + } + } + verific_stream *strm = new verific_ifstream(file_path); + Strings::free(this_file_name); + return strm; + } +}; + // ================================================================== VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : @@ -169,7 +200,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att FOREACH_ATTRIBUTE(obj, mi, attr) { if (attr->Key()[0] == ' ' || attr->Value() == nullptr) continue; - attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); + std::string val = std::string(attr->Value()); + if (val.size()>1 && val[0]=='\"' && val.back()=='\"') + val = val.substr(1,val.size()-2); + attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(val); } if (nl) { @@ -198,7 +232,7 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att p = nullptr; else for (auto q = p+2; *q != '\0'; q++) - if (*q != '0' && *q != '1') { + if (*q != '0' && *q != '1' && *q != 'x' && *q != 'z') { p = nullptr; break; } @@ -798,28 +832,14 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr } if (inst->Type() == OPER_NTO1MUX) { - cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput())); + cell = module->addBmux(inst_name, IN2, IN1, net_map_at(inst->GetOutput())); import_attributes(cell->attributes, inst); return true; } if (inst->Type() == OPER_WIDE_NTO1MUX) { - SigSpec data = IN2, out = OUT; - - int wordsize_bits = ceil_log2(GetSize(out)); - int wordsize = 1 << wordsize_bits; - - SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)}; - - SigSpec padded_data; - for (int i = 0; i < GetSize(data); i += GetSize(out)) { - SigSpec d = data.extract(i, GetSize(out)); - d.extend_u0(wordsize); - padded_data.append(d); - } - - cell = module->addShr(inst_name, padded_data, sel, out); + cell = module->addBmux(inst_name, IN2, IN1, OUT); import_attributes(cell->attributes, inst); return true; } @@ -896,7 +916,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr for (offset = 0; offset < GetSize(sig_acond); offset += width) { for (width = 1; offset+width < GetSize(sig_acond); width++) if (sig_acond[offset] != sig_acond[offset+width]) break; - cell = clocking.addAldff(inst_name, sig_acond[offset], sig_adata.extract(offset, width), + cell = clocking.addAldff(module->uniquify(inst_name), sig_acond[offset], sig_adata.extract(offset, width), sig_d.extract(offset, width), sig_q.extract(offset, width)); import_attributes(cell->attributes, inst); } @@ -922,7 +942,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr if (sig_acond[offset] != sig_acond[offset+width]) break; RTLIL::SigSpec sig_set = module->Mux(NEW_ID, RTLIL::SigSpec(0, width), sig_adata.extract(offset, width), sig_acond[offset]); RTLIL::SigSpec sig_clr = module->Mux(NEW_ID, RTLIL::SigSpec(0, width), module->Not(NEW_ID, sig_adata.extract(offset, width)), sig_acond[offset]); - cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), sig_set, sig_clr, + cell = module->addDlatchsr(module->uniquify(inst_name), net_map_at(inst->GetControl()), sig_set, sig_clr, sig_d.extract(offset, width), sig_q.extract(offset, width)); import_attributes(cell->attributes, inst); } @@ -998,6 +1018,7 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates) for (auto cell : candidates) { + if (cell->type != ID($dff)) continue; SigBit clock = cell->getPort(ID::CLK); bool clock_pol = cell->getParam(ID::CLK_POLARITY).as_bool(); database[make_pair(clock, int(clock_pol))].insert(cell); @@ -1022,7 +1043,7 @@ static std::string sha1_if_contain_spaces(std::string str) return str; } -void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename) +void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::map<std::string,Netlist*> &nl_todo, bool norename) { std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name(); std::string module_name = netlist_name; @@ -1103,20 +1124,32 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size()); wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex()); + wire->upto = portbus->IsUp(); import_attributes(wire->attributes, portbus, nl); - if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN) + bool portbus_input = portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN; + if (portbus_input) wire->port_input = true; if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT) wire->port_output = true; for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) { if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) { + bool bit_input = portbus_input; + if (portbus->GetDir() == DIR_NONE) { + Port *p = portbus->ElementAtIndex(i); + bit_input = p->GetDir() == DIR_INOUT || p->GetDir() == DIR_IN; + if (bit_input) + wire->port_input = true; + if (p->GetDir() == DIR_INOUT || p->GetDir() == DIR_OUT) + wire->port_output = true; + } net = portbus->ElementAtIndex(i)->GetNet(); - RTLIL::SigBit bit(wire, i - wire->start_offset); + int bitidx = wire->upto ? (wire->width - 1 - (i - wire->start_offset)) : (i - wire->start_offset); + RTLIL::SigBit bit(wire, bitidx); if (net_map.count(net) == 0) net_map[net] = bit; - else if (wire->port_input) + else if (bit_input) module->connect(net_map_at(net), bit); else module->connect(bit, net_map_at(net)); @@ -1277,6 +1310,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex()); + wire->upto = netbus->IsUp(); MapIter mibus; FOREACH_NET_OF_NETBUS(netbus, mibus, net) { if (net) @@ -1291,7 +1325,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se { if (netbus->ElementAtIndex(i)) { - int bitidx = i - wire->start_offset; + int bitidx = wire->upto ? (wire->width - 1 - (i - wire->start_offset)) : (i - wire->start_offset); net = netbus->ElementAtIndex(i); RTLIL::SigBit bit(wire, bitidx); @@ -1527,23 +1561,45 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se log_assert(inst->Input1Size() == inst->OutputSize()); - SigSpec sig_d, sig_q, sig_o; - sig_q = module->addWire(new_verific_id(inst), inst->Input1Size()); + unsigned width = inst->Input1Size(); - for (int i = int(inst->Input1Size())-1; i >= 0; i--){ + SigSpec sig_d, sig_dx, sig_qx, sig_o, sig_ox; + sig_dx = module->addWire(new_verific_id(inst), width * 2); + sig_qx = module->addWire(new_verific_id(inst), width * 2); + sig_ox = module->addWire(new_verific_id(inst), width * 2); + + for (int i = int(width)-1; i >= 0; i--){ sig_d.append(net_map_at(inst->GetInput1Bit(i))); sig_o.append(net_map_at(inst->GetOutputBit(i))); } if (verific_verbose) { + for (unsigned i = 0; i < width; i++) { + log(" NEX with A=%s, B=0, Y=%s.\n", + log_signal(sig_d[i]), log_signal(sig_dx[i])); + log(" EQX with A=%s, B=1, Y=%s.\n", + log_signal(sig_d[i]), log_signal(sig_dx[i + width])); + } log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); + log_signal(sig_dx), log_signal(sig_qx), log_signal(clocking.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", - log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); + log_signal(sig_dx), log_signal(sig_qx), log_signal(sig_ox)); + log(" AND with A=%s, B=%s, Y=%s.\n", + log_signal(sig_ox.extract(0, width)), log_signal(sig_ox.extract(width, width)), log_signal(sig_o)); + } + + for (unsigned i = 0; i < width; i++) { + module->addNex(new_verific_id(inst), sig_d[i], State::S0, sig_dx[i]); + module->addEqx(new_verific_id(inst), sig_d[i], State::S1, sig_dx[i + width]); } - clocking.addDff(new_verific_id(inst), sig_d, sig_q); - module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o); + Const qx_init = Const(State::S1, width); + qx_init.bits.resize(2 * width, State::S0); + + clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, qx_init); + module->addXnor(new_verific_id(inst), sig_dx, sig_qx, sig_ox); + + module->addAnd(new_verific_id(inst), sig_ox.extract(0, width), sig_ox.extract(width, width), sig_o); if (!mode_keep) continue; @@ -1557,17 +1613,25 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se SigSpec sig_d = net_map_at(inst->GetInput1()); SigSpec sig_o = net_map_at(inst->GetOutput()); - SigSpec sig_q = module->addWire(new_verific_id(inst)); + SigSpec sig_dx = module->addWire(new_verific_id(inst), 2); + SigSpec sig_qx = module->addWire(new_verific_id(inst), 2); if (verific_verbose) { + log(" NEX with A=%s, B=0, Y=%s.\n", + log_signal(sig_d), log_signal(sig_dx[0])); + log(" EQX with A=%s, B=1, Y=%s.\n", + log_signal(sig_d), log_signal(sig_dx[1])); log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); - log(" XNOR with A=%s, B=%s, Y=%s.\n", - log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); + log_signal(sig_dx), log_signal(sig_qx), log_signal(clocking.clock_sig)); + log(" EQ with A=%s, B=%s, Y=%s.\n", + log_signal(sig_dx), log_signal(sig_qx), log_signal(sig_o)); } - clocking.addDff(new_verific_id(inst), sig_d, sig_q); - module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o); + module->addNex(new_verific_id(inst), sig_d, State::S0, sig_dx[0]); + module->addEqx(new_verific_id(inst), sig_d, State::S1, sig_dx[1]); + + clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, Const(1, 2)); + module->addEq(new_verific_id(inst), sig_dx, sig_qx, sig_o); if (!mode_keep) continue; @@ -1601,13 +1665,20 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_o = net_map_at(inst->GetOutput()); SigBit sig_q = module->addWire(new_verific_id(inst)); + SigBit sig_d_no_x = module->addWire(new_verific_id(inst)); - if (verific_verbose) + if (verific_verbose) { + log(" EQX with A=%s, B=%d, Y=%s.\n", + log_signal(sig_d), inst->Type() == PRIM_SVA_ROSE, log_signal(sig_d_no_x)); log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); + log_signal(sig_d_no_x), log_signal(sig_q), log_signal(clocking.clock_sig)); + log(" EQ with A={%s, %s}, B={0, 1}, Y=%s.\n", + log_signal(sig_q), log_signal(sig_d_no_x), log_signal(sig_o)); + } - clocking.addDff(new_verific_id(inst), sig_d, sig_q); - module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o); + module->addEqx(new_verific_id(inst), sig_d, inst->Type() == PRIM_SVA_ROSE ? State::S1 : State::S0, sig_d_no_x); + clocking.addDff(new_verific_id(inst), sig_d_no_x, sig_q, State::S0); + module->addEq(new_verific_id(inst), {sig_q, sig_d_no_x}, Const(1, 2), sig_o); if (!mode_keep) continue; @@ -1660,10 +1731,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se } import_verific_cells: - nl_todo.insert(inst->View()); - std::string inst_type = inst->View()->Owner()->Name(); + nl_todo[inst_type] = inst->View(); + if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) { inst_type = "$verific$" + inst_type; } else { @@ -1873,15 +1944,19 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX) break; - if (!inst_mux->GetInput1()->IsPwr()) + bool pwr1 = inst_mux->GetInput1()->IsPwr(); + bool pwr2 = inst_mux->GetInput2()->IsPwr(); + + if (!pwr1 && !pwr2) break; - Net *sva_net = inst_mux->GetInput2(); + Net *sva_net = pwr1 ? inst_mux->GetInput2() : inst_mux->GetInput1(); if (!verific_is_sva_net(importer, sva_net)) break; body_net = sva_net; cond_net = inst_mux->GetControl(); + cond_pol = pwr1; } while (0); clock_net = net; @@ -2042,7 +2117,7 @@ struct VerificExtNets string name = stringf("___extnets_%d", portname_cnt++); Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN); nl->Add(new_port); - net->Connect(new_port); + nl->Buf(net)->Connect(new_port); // create new Net in up Netlist Net *new_net = final_net; @@ -2158,7 +2233,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par { verific_sva_fsm_limit = 16; - std::set<Netlist*> nl_todo, nl_done; + std::map<std::string,Netlist*> nl_todo, nl_done; VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1); Array *netlists = NULL; @@ -2174,7 +2249,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par verific_params.Insert(i.first.c_str(), i.second.c_str()); #ifdef YOSYSHQ_VERIFIC_EXTENSIONS - InitialAssertions::Rewrite("work", &verific_params); + VerificExtensions::ElaborateAndRewrite("work", &verific_params); #endif if (top.empty()) { @@ -2211,10 +2286,10 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par int i; FOREACH_ARRAY_ITEM(netlists, i, nl) { - if (top.empty() && nl->CellBaseName() != top) + if (!top.empty() && nl->CellBaseName() != top) continue; nl->AddAtt(new Att(" \\top", NULL)); - nl_todo.insert(nl); + nl_todo.emplace(nl->CellBaseName(), nl); } delete netlists; @@ -2223,29 +2298,38 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par log_error("%s\n", verific_error_msg.c_str()); for (auto nl : nl_todo) - nl->ChangePortBusStructures(1 /* hierarchical */); + nl.second->ChangePortBusStructures(1 /* hierarchical */); VerificExtNets worker; for (auto nl : nl_todo) - worker.run(nl); + worker.run(nl.second); while (!nl_todo.empty()) { - Netlist *nl = *nl_todo.begin(); - if (nl_done.count(nl) == 0) { + auto it = nl_todo.begin(); + Netlist *nl = it->second; + if (nl_done.count(it->first) == 0) { VerificImporter importer(false, false, false, false, false, false, false); + nl_done[it->first] = it->second; importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top); } - nl_todo.erase(nl); - nl_done.insert(nl); + nl_todo.erase(it); } +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + VerificExtensions::Reset(); +#endif + hier_tree::DeleteHierarchicalTree(); veri_file::Reset(); #ifdef VERIFIC_VHDL_SUPPORT vhdl_file::Reset(); #endif Libset::Reset(); + Message::Reset(); + RuntimeFlags::DeleteAllFlags(); + LineFile::DeleteAllLineFiles(); verific_incdirs.clear(); verific_libdirs.clear(); + verific_libexts.clear(); verific_import_pending = false; if (!verific_error_msg.empty()) @@ -2285,7 +2369,7 @@ struct VerificPass : public Pass { log("\n"); log("Additional -D<macro>[=<value>] options may be added after the option indicating\n"); log("the language version (and before file names) to set additional verilog defines.\n"); - log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n"); + log("The macros YOSYS, SYNTHESIS, and VERIFIC are defined implicitly.\n"); log("\n"); log("\n"); log(" verific -formal <verilog-file>..\n"); @@ -2300,29 +2384,36 @@ struct VerificPass : public Pass { log("\n"); log("\n"); #endif - log(" verific {-f|-F} <command-file>\n"); + log(" verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n"); + log(" -sv2012|-sv|-formal] <command-file>\n"); log("\n"); log("Load and execute the specified command file.\n"); - log("\n"); - log("Command file parser supports following commands:\n"); - log(" +define - defines macro\n"); - log(" -u - upper case all identifier (makes Verilog parser case insensitive)\n"); - log(" -v - register library name (file)\n"); - log(" -y - register library name (directory)\n"); - log(" +incdir - specify include dir\n"); - log(" +libext - specify library extension\n"); - log(" +liborder - add library in ordered list\n"); - log(" +librescan - unresolved modules will be always searched starting with the first\n"); - log(" library specified by -y/-v options.\n"); - log(" -f/-file - nested -f option\n"); - log(" -F - nested -F option\n"); - log("\n"); - log(" parse mode:\n"); + log("Override verilog parsing mode can be set.\n"); + log("The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly.\n"); + log("\n"); + log("Command file parser supports following commands in file:\n"); + log(" +define+<MACRO>=<VALUE> - defines macro\n"); + log(" -u - upper case all identifier (makes Verilog parser\n"); + log(" case insensitive)\n"); + log(" -v <filepath> - register library name (file)\n"); + log(" -y <filepath> - register library name (directory)\n"); + log(" +incdir+<filepath> - specify include dir\n"); + log(" +libext+<filepath> - specify library extension\n"); + log(" +liborder+<id> - add library in ordered list\n"); + log(" +librescan - unresolved modules will be always searched\n"); + log(" starting with the first library specified\n"); + log(" by -y/-v options.\n"); + log(" -f/-file <filepath> - nested -f option\n"); + log(" -F <filepath> - nested -F option (relative path)\n"); + log(" parse files:\n"); + log(" <filepath>\n"); + log(" +systemverilogext+<filepath>\n"); + log(" +verilog1995ext+<filepath>\n"); + log(" +verilog2001ext+<filepath>\n"); + log("\n"); + log(" analysis mode:\n"); log(" -ams\n"); - log(" +systemverilogext\n"); log(" +v2k\n"); - log(" +verilog1995ext\n"); - log(" +verilog2001ext\n"); log(" -sverilog\n"); log("\n"); log("\n"); @@ -2349,6 +2440,11 @@ struct VerificPass : public Pass { log("find undefined modules.\n"); log("\n"); log("\n"); + log(" verific -vlog-libext <extension>..\n"); + log("\n"); + log("Add Verilog library extensions, used when searching in library directories.\n"); + log("\n"); + log("\n"); log(" verific -vlog-define <macro>[=<value>]..\n"); log("\n"); log("Add Verilog defines.\n"); @@ -2404,6 +2500,9 @@ struct VerificPass : public Pass { log(" -v, -vv\n"); log(" Verbose log messages. (-vv is even more verbose than -v.)\n"); log("\n"); + log(" -pp <filename>\n"); + log(" Pretty print design after elaboration to specified file.\n"); + log("\n"); log("The following additional import options are useful for debugging the Verific\n"); log("bindings (for Yosys and/or Verific developers):\n"); log("\n"); @@ -2444,66 +2543,14 @@ struct VerificPass : public Pass { log(" Save output for VHDL design units.\n"); log("\n"); log("\n"); - log(" verific -app <application>..\n"); - log("\n"); - log("Execute YosysHQ formal application on loaded Verilog files.\n"); - log("\n"); - log("Application options:\n"); - log("\n"); - log(" -module <module>\n"); - log(" Run formal application only on specified module.\n"); - log("\n"); - log(" -blacklist <filename[:lineno]>\n"); - log(" Do not run application on modules from files that match the filename\n"); - log(" or filename and line number if provided in such format.\n"); - log(" Parameter can also contain comma separated list of file locations.\n"); - log("\n"); - log(" -blfile <file>\n"); - log(" Do not run application on locations specified in file, they can represent filename\n"); - log(" or filename and location in file.\n"); - log("\n"); - log("Applications:\n"); - log("\n"); -#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS) - VerificFormalApplications vfa; - log("%s\n",vfa.GetHelp().c_str()); -#else - log(" WARNING: Applications only available in commercial build.\n"); - -#endif - log("\n"); - log("\n"); - log(" verific -template <name> <top_module>..\n"); - log("\n"); - log("Generate template for specified top module of loaded design.\n"); - log("\n"); - log("Template options:\n"); - log("\n"); - log(" -out\n"); - log(" Specifies output file for generated template, by default output is stdout\n"); - log("\n"); - log(" -chparam name value \n"); - log(" Generate template using this parameter value. Otherwise default parameter\n"); - log(" values will be used for templat generate functionality. This option\n"); - log(" can be specified multiple times to override multiple parameters.\n"); - log(" String values must be passed in double quotes (\").\n"); - log("\n"); - log("Templates:\n"); - log("\n"); -#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES) - VerificTemplateGenerator vfg; - log("%s\n",vfg.GetHelp().c_str()); -#else - log(" WARNING: Templates only available in commercial build.\n"); - log("\n"); -#endif - log("\n"); - log("\n"); log(" verific -cfg [<name> [<value>]]\n"); log("\n"); log("Get/set Verific runtime flags.\n"); log("\n"); log("\n"); +#if defined(YOSYS_ENABLE_VERIFIC) and defined(YOSYSHQ_VERIFIC_EXTENSIONS) + VerificExtensions::Help(); +#endif log("Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"); log("https://www.yosyshq.com/\n"); log("\n"); @@ -2542,10 +2589,12 @@ struct VerificPass : public Pass { RuntimeFlags::SetVar("veri_extract_dualport_rams", 0); RuntimeFlags::SetVar("veri_extract_multiport_rams", 1); + RuntimeFlags::SetVar("veri_allow_any_ram_in_loop", 1); #ifdef VERIFIC_VHDL_SUPPORT RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0); RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1); + RuntimeFlags::SetVar("vhdl_allow_any_ram_in_loop", 1); RuntimeFlags::SetVar("vhdl_support_variable_slice", 1); RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0); @@ -2593,6 +2642,8 @@ struct VerificPass : public Pass { int argidx = 1; std::string work = "work"; + YosysStreamCallBackHandler cb; + veri_file::RegisterCallBackVerificStream(&cb); if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" || args[argidx] == "-set-info" || args[argidx] == "-set-ignore")) @@ -2628,6 +2679,12 @@ struct VerificPass : public Pass { goto check_error; } + if (GetSize(args) > argidx && args[argidx] == "-vlog-libext") { + for (argidx++; argidx < GetSize(args); argidx++) + verific_libexts.push_back(args[argidx]); + goto check_error; + } + if (GetSize(args) > argidx && args[argidx] == "-vlog-define") { for (argidx++; argidx < GetSize(args); argidx++) { string name = args[argidx]; @@ -2667,14 +2724,54 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && (args[argidx] == "-f" || args[argidx] == "-F")) { - unsigned verilog_mode = veri_file::VERILOG_95; // default recommended by Verific + unsigned verilog_mode = veri_file::UNDEFINED; + bool is_formal = false; + const char* filename = nullptr; Verific::veri_file::f_file_flags flags = (args[argidx] == "-f") ? veri_file::F_FILE_NONE : veri_file::F_FILE_CAPITAL; - Array *file_names = veri_file::ProcessFFile(args[++argidx].c_str(), flags, verilog_mode); + for (argidx++; argidx < GetSize(args); argidx++) { + if (args[argidx] == "-vlog95") { + verilog_mode = veri_file::VERILOG_95; + continue; + } else if (args[argidx] == "-vlog2k") { + verilog_mode = veri_file::VERILOG_2K; + continue; + } else if (args[argidx] == "-sv2005") { + verilog_mode = veri_file::SYSTEM_VERILOG_2005; + continue; + } else if (args[argidx] == "-sv2009") { + verilog_mode = veri_file::SYSTEM_VERILOG_2009; + continue; + } else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal") { + verilog_mode = veri_file::SYSTEM_VERILOG; + if (args[argidx] == "-formal") is_formal = true; + continue; + } else if (args[argidx].compare(0, 1, "-") == 0) { + cmd_error(args, argidx, "unknown option"); + goto check_error; + } + + if (!filename) { + filename = args[argidx].c_str(); + continue; + } else { + log_cmd_error("Only one filename can be specified.\n"); + } + } + if (!filename) + log_cmd_error("Filname must be specified.\n"); + + unsigned analysis_mode = verilog_mode; // keep default as provided by user if not defined in file + Array *file_names = veri_file::ProcessFFile(filename, flags, analysis_mode); + if (analysis_mode != verilog_mode) + log_warning("Provided verilog mode differs from one specified in file.\n"); + + veri_file::DefineMacro("YOSYS"); veri_file::DefineMacro("VERIFIC"); + veri_file::DefineMacro(is_formal ? "FORMAL" : "SYNTHESIS"); - if (!veri_file::AnalyzeMultipleFiles(file_names, verilog_mode, work.c_str(), veri_file::MFCU)) { + if (!veri_file::AnalyzeMultipleFiles(file_names, analysis_mode, work.c_str(), veri_file::MFCU)) { verific_error_msg.clear(); log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n"); } @@ -2703,6 +2800,7 @@ struct VerificPass : public Pass { else log_abort(); + veri_file::DefineMacro("YOSYS"); veri_file::DefineMacro("VERIFIC"); veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS"); @@ -2727,6 +2825,8 @@ struct VerificPass : public Pass { veri_file::AddIncludeDir(dir.c_str()); for (auto &dir : verific_libdirs) veri_file::AddYDir(dir.c_str()); + for (auto &ext : verific_libexts) + veri_file::AddLibExt(ext.c_str()); while (argidx < GetSize(args)) file_names.Insert(args[argidx++].c_str()); @@ -2778,101 +2878,6 @@ struct VerificPass : public Pass { } #endif -#ifdef YOSYSHQ_VERIFIC_FORMALAPPS - if (argidx < GetSize(args) && args[argidx] == "-app") - { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx, "No formal application specified.\n"); - - VerificFormalApplications vfa; - auto apps = vfa.GetApps(); - std::string app = args[++argidx]; - std::vector<std::string> blacklists; - if (apps.find(app) == apps.end()) - log_cmd_error("Application '%s' does not exist.\n", app.c_str()); - - FormalApplication *application = apps[app]; - application->setLogger([](std::string msg) { log("%s",msg.c_str()); } ); - VeriModule *selected_module = nullptr; - - for (argidx++; argidx < GetSize(args); argidx++) { - std::string error; - if (application->checkParams(args, argidx, error)) { - if (!error.empty()) - cmd_error(args, argidx, error); - continue; - } - - if (args[argidx] == "-module" && argidx < GetSize(args)) { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No module name specified.\n"); - std::string module = args[++argidx]; - VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); - selected_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr; - if (!selected_module) { - log_error("Can't find module '%s'.\n", module.c_str()); - } - continue; - } - if (args[argidx] == "-blacklist" && argidx < GetSize(args)) { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No blacklist specified.\n"); - - std::string line = args[++argidx]; - std::string p; - while (!(p = next_token(line, ",\t\r\n ")).empty()) - blacklists.push_back(p); - continue; - } - if (args[argidx] == "-blfile" && argidx < GetSize(args)) { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No blacklist file specified.\n"); - std::string fn = args[++argidx]; - std::ifstream f(fn); - if (f.fail()) - log_cmd_error("Can't open blacklist file '%s'!\n", fn.c_str()); - - std::string line,p; - while (std::getline(f, line)) { - while (!(p = next_token(line, ",\t\r\n ")).empty()) - blacklists.push_back(p); - } - continue; - } - break; - } - if (argidx < GetSize(args)) - cmd_error(args, argidx, "unknown option/parameter"); - - application->setBlacklists(&blacklists); - application->setSingleModuleMode(selected_module!=nullptr); - - const char *err = application->validate(); - if (err) - cmd_error(args, argidx, err); - - MapIter mi; - VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1); - log("Running formal application '%s'.\n", app.c_str()); - - if (selected_module) { - std::string out; - if (!application->execute(selected_module, out)) - log_error("%s", out.c_str()); - } - else { - VeriModule *module ; - FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, module) { - std::string out; - if (!application->execute(module, out)) { - log_error("%s", out.c_str()); - break; - } - } - } - goto check_error; - } -#endif if (argidx < GetSize(args) && args[argidx] == "-pp") { const char* filename = nullptr; @@ -2921,99 +2926,15 @@ struct VerificPass : public Pass { goto check_error; } -#ifdef YOSYSHQ_VERIFIC_TEMPLATES - if (argidx < GetSize(args) && args[argidx] == "-template") - { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No template type specified.\n"); - - VerificTemplateGenerator vfg; - auto gens = vfg.GetGenerators(); - std::string app = args[++argidx]; - if (gens.find(app) == gens.end()) - log_cmd_error("Template generator '%s' does not exist.\n", app.c_str()); - TemplateGenerator *generator = gens[app]; - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No top module specified.\n"); - generator->setLogger([](std::string msg) { log("%s",msg.c_str()); } ); - - std::string module = args[++argidx]; - VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1); - VeriModule *veri_module = veri_lib ? veri_lib->GetModule(module.c_str(), 1) : nullptr; - if (!veri_module) { - log_error("Can't find module/unit '%s'.\n", module.c_str()); - } - - log("Template '%s' is running for module '%s'.\n", app.c_str(),module.c_str()); - - Map parameters(STRING_HASH); - const char *out_filename = nullptr; - - for (argidx++; argidx < GetSize(args); argidx++) { - std::string error; - if (generator->checkParams(args, argidx, error)) { - if (!error.empty()) - cmd_error(args, argidx, error); - continue; - } - - if (args[argidx] == "-chparam" && argidx < GetSize(args)) { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No param name specified.\n"); - if (!(argidx+2 < GetSize(args))) - cmd_error(args, argidx+2, "No param value specified.\n"); - - const std::string &key = args[++argidx]; - const std::string &value = args[++argidx]; - unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(), - 1 /* force_overwrite */); - if (!new_insertion) - log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str()); - continue; - } - - if (args[argidx] == "-out" && argidx < GetSize(args)) { - if (!(argidx+1 < GetSize(args))) - cmd_error(args, argidx+1, "No output file specified.\n"); - out_filename = args[++argidx].c_str(); - continue; - } - - break; - } - if (argidx < GetSize(args)) - cmd_error(args, argidx, "unknown option/parameter"); - - const char *err = generator->validate(); - if (err) - cmd_error(args, argidx, err); - - std::string val; - if (!generator->generate(veri_module, val, ¶meters)) - log_error("%s", val.c_str()); - - FILE *of = stdout; - if (out_filename) { - of = fopen(out_filename, "w"); - if (of == nullptr) - log_error("Can't open '%s' for writing: %s\n", out_filename, strerror(errno)); - log("Writing output to '%s'\n",out_filename); - } - fprintf(of, "%s\n",val.c_str()); - fflush(of); - if (of!=stdout) - fclose(of); - goto check_error; - } -#endif if (GetSize(args) > argidx && args[argidx] == "-import") { - std::set<Netlist*> nl_todo, nl_done; + std::map<std::string,Netlist*> nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; bool mode_nosva = false, mode_names = false, mode_verific = false; bool mode_autocover = false, mode_fullinit = false; bool flatten = false, extnets = false; string dumpfile; + string ppfile; Map parameters(STRING_HASH); for (argidx++; argidx < GetSize(args); argidx++) { @@ -3082,6 +3003,10 @@ struct VerificPass : public Pass { dumpfile = args[++argidx]; continue; } + if (args[argidx] == "-pp" && argidx+1 < GetSize(args)) { + ppfile = args[++argidx]; + continue; + } break; } @@ -3091,8 +3016,11 @@ struct VerificPass : public Pass { std::set<std::string> top_mod_names; #ifdef YOSYSHQ_VERIFIC_EXTENSIONS - InitialAssertions::Rewrite(work, ¶meters); + VerificExtensions::ElaborateAndRewrite(work, ¶meters); #endif + if (!ppfile.empty()) + veri_file::PrettyPrint(ppfile.c_str(), nullptr, work.c_str()); + if (mode_all) { log("Running hier_tree::ElaborateAll().\n"); @@ -3111,7 +3039,7 @@ struct VerificPass : public Pass { int i; FOREACH_ARRAY_ITEM(netlists, i, nl) - nl_todo.insert(nl); + nl_todo.emplace(nl->CellBaseName(), nl); delete netlists; } else @@ -3163,8 +3091,10 @@ struct VerificPass : public Pass { int i; FOREACH_ARRAY_ITEM(netlists, i, nl) { + if (!top_mod_names.count(nl->CellBaseName())) + continue; nl->AddAtt(new Att(" \\top", NULL)); - nl_todo.insert(nl); + nl_todo.emplace(nl->CellBaseName(), nl); } delete netlists; } @@ -3174,17 +3104,17 @@ struct VerificPass : public Pass { if (flatten) { for (auto nl : nl_todo) - nl->Flatten(); + nl.second->Flatten(); } if (extnets) { VerificExtNets worker; for (auto nl : nl_todo) - worker.run(nl); + worker.run(nl.second); } for (auto nl : nl_todo) - nl->ChangePortBusStructures(1 /* hierarchical */); + nl.second->ChangePortBusStructures(1 /* hierarchical */); if (!dumpfile.empty()) { VeriWrite veri_writer; @@ -3192,23 +3122,32 @@ struct VerificPass : public Pass { } while (!nl_todo.empty()) { - Netlist *nl = *nl_todo.begin(); - if (nl_done.count(nl) == 0) { + auto it = nl_todo.begin(); + Netlist *nl = it->second; + if (nl_done.count(it->first) == 0) { VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names, mode_verific, mode_autocover, mode_fullinit); + nl_done[it->first] = it->second; importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name())); } - nl_todo.erase(nl); - nl_done.insert(nl); + nl_todo.erase(it); } +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + VerificExtensions::Reset(); +#endif + hier_tree::DeleteHierarchicalTree(); veri_file::Reset(); #ifdef VERIFIC_VHDL_SUPPORT vhdl_file::Reset(); #endif Libset::Reset(); + Message::Reset(); + RuntimeFlags::DeleteAllFlags(); + LineFile::DeleteAllLineFiles(); verific_incdirs.clear(); verific_libdirs.clear(); + verific_libexts.clear(); verific_import_pending = false; goto check_error; } @@ -3271,6 +3210,13 @@ struct VerificPass : public Pass { } } } +#ifdef YOSYSHQ_VERIFIC_EXTENSIONS + if (VerificExtensions::Execute(args, argidx, work, + [this](const std::vector<std::string> &args, size_t argidx, std::string msg) + { cmd_error(args, argidx, msg); } )) { + goto check_error; + } +#endif cmd_error(args, argidx, "Missing or unsupported mode parameter.\n"); diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 9d5beb787..695c04f3b 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -44,6 +44,7 @@ struct VerificClocking { SigBit disable_sig = State::S0; bool posedge = true; bool gclk = false; + bool cond_pol = true; VerificClocking() { } VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false); @@ -94,7 +95,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, bool norename = false); + void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::map<std::string,Verific::Netlist*> &nl_todo, bool norename = false); }; void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst); diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 1bbdcf016..12bac2a3d 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1522,10 +1522,13 @@ struct VerificSvaImporter if (inst == nullptr) return false; - if (clocking.cond_net != nullptr) + if (clocking.cond_net != nullptr) { trig = importer->net_map_at(clocking.cond_net); - else + if (!clocking.cond_pol) + trig = module->Not(NEW_ID, trig); + } else { trig = State::S1; + } if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY) { @@ -1587,8 +1590,11 @@ struct VerificSvaImporter SigBit trig = State::S1; - if (clocking.cond_net != nullptr) + if (clocking.cond_net != nullptr) { trig = importer->net_map_at(clocking.cond_net); + if (!clocking.cond_pol) + trig = module->Not(NEW_ID, trig); + } if (inst == nullptr) { diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc index 17f567587..883531e78 100644 --- a/frontends/verilog/preproc.cc +++ b/frontends/verilog/preproc.cc @@ -142,6 +142,16 @@ static std::string next_token(bool pass_newline = false) return_char(ch); } } + else if (ch == '\\') + { + while ((ch = next_char()) != 0) { + if (ch < 33 || ch > 126) { + return_char(ch); + break; + } + token += ch; + } + } else if (ch == '/') { if ((ch = next_char()) != 0) { diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 89c1aa895..958809319 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -128,6 +128,11 @@ static bool isUserType(std::string &s) %x IMPORT_DPI %x BASED_CONST +UNSIGNED_NUMBER [0-9][0-9_]* +FIXED_POINT_NUMBER_DEC [0-9][0-9_]*\.[0-9][0-9_]*([eE][-+]?[0-9_]+)? +FIXED_POINT_NUMBER_NO_DEC [0-9][0-9_]*[eE][-+]?[0-9_]+ +TIME_SCALE_SUFFIX [munpf]?s + %% // Initialise comment_caller to something to avoid a "maybe undefined" // warning from GCC. @@ -297,7 +302,7 @@ static bool isUserType(std::string &s) "union" { SV_KEYWORD(TOK_UNION); } "packed" { SV_KEYWORD(TOK_PACKED); } -[0-9][0-9_]* { +{UNSIGNED_NUMBER} { yylval->string = new std::string(yytext); return TOK_CONSTVAL; } @@ -319,12 +324,12 @@ static bool isUserType(std::string &s) return TOK_BASED_CONSTVAL; } -[0-9][0-9_]*\.[0-9][0-9_]*([eE][-+]?[0-9_]+)? { +{FIXED_POINT_NUMBER_DEC} { yylval->string = new std::string(yytext); return TOK_REALVAL; } -[0-9][0-9_]*[eE][-+]?[0-9_]+ { +{FIXED_POINT_NUMBER_NO_DEC} { yylval->string = new std::string(yytext); return TOK_REALVAL; } @@ -574,6 +579,10 @@ import[ \t\r\n]+\"(DPI|DPI-C)\"[ \t\r\n]+function[ \t\r\n]+ { return TOK_SPECIFY_AND; } +{UNSIGNED_NUMBER}{TIME_SCALE_SUFFIX} { return TOK_TIME_SCALE; } +{FIXED_POINT_NUMBER_DEC}{TIME_SCALE_SUFFIX} { return TOK_TIME_SCALE; } +{FIXED_POINT_NUMBER_NO_DEC}{TIME_SCALE_SUFFIX} { return TOK_TIME_SCALE; } + <INITIAL,BASED_CONST>"/*" { comment_caller=YY_START; BEGIN(COMMENT); } <COMMENT>. /* ignore comment body */ <COMMENT>\n /* ignore comment body */ diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 171e098a5..c533b0c40 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -369,7 +369,7 @@ static void rewriteGenForDeclInit(AstNode *loop) %token TOK_BIT_OR_ASSIGN TOK_BIT_AND_ASSIGN TOK_BIT_XOR_ASSIGN TOK_ADD_ASSIGN %token TOK_SUB_ASSIGN TOK_DIV_ASSIGN TOK_MOD_ASSIGN TOK_MUL_ASSIGN %token TOK_SHL_ASSIGN TOK_SHR_ASSIGN TOK_SSHL_ASSIGN TOK_SSHR_ASSIGN -%token TOK_BIND +%token TOK_BIND TOK_TIME_SCALE %type <ast> range range_or_multirange non_opt_range non_opt_multirange %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list non_io_wire_type io_wire_type @@ -779,6 +779,9 @@ non_opt_delay: '#' TOK_ID { delete $2; } | '#' TOK_CONSTVAL { delete $2; } | '#' TOK_REALVAL { delete $2; } | + // our `expr` doesn't have time_scale, so we need the parenthesized variant + '#' TOK_TIME_SCALE | + '#' '(' TOK_TIME_SCALE ')' | '#' '(' mintypmax_expr ')' | '#' '(' mintypmax_expr ',' mintypmax_expr ')' | '#' '(' mintypmax_expr ',' mintypmax_expr ',' mintypmax_expr ')'; |