aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
Diffstat (limited to 'frontends')
-rw-r--r--frontends/ast/ast.cc2
-rw-r--r--frontends/ast/ast.h1
-rw-r--r--frontends/ast/genrtlil.cc34
-rw-r--r--frontends/ast/simplify.cc229
-rw-r--r--frontends/blif/blifparse.cc5
-rw-r--r--frontends/json/jsonparse.cc34
-rw-r--r--frontends/verific/README2
-rw-r--r--frontends/verific/verific.cc602
-rw-r--r--frontends/verific/verific.h3
-rw-r--r--frontends/verific/verificsva.cc12
-rw-r--r--frontends/verilog/preproc.cc10
-rw-r--r--frontends/verilog/verilog_lexer.l15
-rw-r--r--frontends/verilog/verilog_parser.y5
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, &parameters))
- 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, &parameters);
+ VerificExtensions::ElaborateAndRewrite(work, &parameters);
#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 ')';