diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 201584885..ecc58cf63 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -80,6 +80,7 @@ std::string AST::type2str(AstNodeType type) X(AST_CELLTYPE) X(AST_IDENTIFIER) X(AST_PREFIX) + X(AST_ASSERT) X(AST_FCALL) X(AST_TO_SIGNED) X(AST_TO_UNSIGNED) diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index 22853d0f9..6aaa90e86 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -58,6 +58,7 @@ namespace AST AST_CELLTYPE, AST_IDENTIFIER, AST_PREFIX, + AST_ASSERT, AST_FCALL, AST_TO_SIGNED, diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index e44b2d361..83a5c7506 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -1276,6 +1276,38 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) } break; + // generate $assert cells + case AST_ASSERT: + { + log_assert(children.size() == 2); + + RTLIL::SigSpec check = children[0]->genRTLIL(); + log_assert(check.width == 1); + + RTLIL::SigSpec en = children[1]->genRTLIL(); + log_assert(en.width == 1); + + std::stringstream sstr; + sstr << "$assert$" << filename << ":" << linenum << "$" << (RTLIL::autoidx++); + + RTLIL::Cell *cell = new RTLIL::Cell; + cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum); + cell->name = sstr.str(); + cell->type = "$assert"; + current_module->cells[cell->name] = cell; + + for (auto &attr : attributes) { + if (attr.second->type != AST_CONSTANT) + log_error("Attribute `%s' with non-constant value at %s:%d!\n", + attr.first.c_str(), filename.c_str(), linenum); + cell->attributes[attr.first] = attr.second->asAttrConst(); + } + + cell->connections["\\A"] = check; + cell->connections["\\EN"] = en; + } + break; + // add entries to current_module->connections for assignments (outside of always blocks) case AST_ASSIGN: { diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index bc5dec7b9..c266800e9 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -966,6 +966,66 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, } skip_dynamic_range_lvalue_expansion:; + if (stage > 1 && type == AST_ASSERT && current_block != NULL) + { + std::stringstream sstr; + sstr << "$assert$" << filename << ":" << linenum << "$" << (RTLIL::autoidx++); + std::string id_check = sstr.str() + "_CHECK", id_en = sstr.str() + "_EN"; + + AstNode *wire_check = new AstNode(AST_WIRE); + wire_check->str = id_check; + current_ast_mod->children.push_back(wire_check); + current_scope[wire_check->str] = wire_check; + while (wire_check->simplify(true, false, false, 1, -1, false)) { } + + AstNode *wire_en = new AstNode(AST_WIRE); + wire_en->str = id_en; + current_ast_mod->children.push_back(wire_en); + current_scope[wire_en->str] = wire_en; + while (wire_en->simplify(true, false, false, 1, -1, false)) { } + + std::vector x_bit; + x_bit.push_back(RTLIL::State::Sx); + + AstNode *assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_bits(x_bit, false)); + assign_check->children[0]->str = id_check; + + AstNode *assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(0, false, 1)); + assign_en->children[0]->str = id_en; + + AstNode *default_signals = new AstNode(AST_BLOCK); + default_signals->children.push_back(assign_check); + default_signals->children.push_back(assign_en); + current_top_block->children.insert(current_top_block->children.begin(), default_signals); + + assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_REDUCE_BOOL, children[0]->clone())); + assign_check->children[0]->str = id_check; + + assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1)); + assign_en->children[0]->str = id_en; + + newNode = new AstNode(AST_BLOCK); + newNode->children.push_back(assign_check); + newNode->children.push_back(assign_en); + + AstNode *assertnode = new AstNode(AST_ASSERT); + assertnode->children.push_back(new AstNode(AST_IDENTIFIER)); + assertnode->children.push_back(new AstNode(AST_IDENTIFIER)); + assertnode->children[0]->str = id_check; + assertnode->children[1]->str = id_en; + assertnode->attributes.swap(attributes); + current_ast_mod->children.push_back(assertnode); + + goto apply_newNode; + } + + if (stage > 1 && type == AST_ASSERT && children.size() == 1) + { + children[0] = new AstNode(AST_REDUCE_BOOL, children[0]->clone()); + children.push_back(mkconst_int(1, false, 1)); + did_something = true; + } + // found right-hand side identifier for memory -> replace with memory read port if (stage > 1 && type == AST_IDENTIFIER && id2ast != NULL && id2ast->type == AST_MEMORY && !in_lvalue && children[0]->type == AST_RANGE && children[0]->children.size() == 1) { diff --git a/frontends/verilog/lexer.l b/frontends/verilog/lexer.l index 9e606d90f..81167cf4e 100644 --- a/frontends/verilog/lexer.l +++ b/frontends/verilog/lexer.l @@ -113,6 +113,8 @@ namespace VERILOG_FRONTEND { "generate" { return TOK_GENERATE; } "endgenerate" { return TOK_ENDGENERATE; } +"assert"([ \t\r\n]+"property")? { return TOK_ASSERT; } + "input" { return TOK_INPUT; } "output" { return TOK_OUTPUT; } "inout" { return TOK_INOUT; } diff --git a/frontends/verilog/parser.y b/frontends/verilog/parser.y index 874482d6e..b0c4db8ae 100644 --- a/frontends/verilog/parser.y +++ b/frontends/verilog/parser.y @@ -104,7 +104,7 @@ static void free_attr(std::map *al) %token TOK_GENERATE TOK_ENDGENERATE TOK_GENVAR %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED -%token TOK_POS_INDEXED TOK_NEG_INDEXED +%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT %type wire_type range non_opt_range expr basic_expr concat_list rvalue lvalue lvalue_concat_list %type opt_label tok_prim_wrapper hierarchical_id @@ -366,7 +366,7 @@ module_body: module_body_stmt: task_func_decl | param_decl | localparam_decl | defparam_decl | wire_decl | assign_stmt | cell_stmt | - always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr; + always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert; task_func_decl: TOK_TASK TOK_ID ';' { @@ -748,6 +748,11 @@ opt_label: $$ = NULL; }; +assert: + TOK_ASSERT '(' expr ')' ';' { + ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3)); + }; + simple_behavioral_stmt: lvalue '=' expr { AstNode *node = new AstNode(AST_ASSIGN_EQ, $1, $3); @@ -760,7 +765,7 @@ simple_behavioral_stmt: // this production creates the obligatory if-else shift/reduce conflict behavioral_stmt: - defattr | wire_decl | + defattr | assert | wire_decl | simple_behavioral_stmt ';' | hierarchical_id attr { AstNode *node = new AstNode(AST_TCALL); diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc index 5cfa0f24b..db53e8c68 100644 --- a/frontends/verilog/preproc.cc +++ b/frontends/verilog/preproc.cc @@ -386,7 +386,7 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m std::string name = tok.substr(1); // printf("expand: >>%s<< -> >>%s<<\n", name.c_str(), defines_map[name].c_str()); std::string skipped_spaces = skip_spaces(); - tok = next_token(true); + tok = next_token(false); if (tok == "(" && defines_with_args.count(name) > 0) { int level = 1; std::vector args; diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 2f311c826..9e63e9d1b 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -96,6 +96,7 @@ struct CellTypes cell_types.insert("$pmux"); cell_types.insert("$safe_pmux"); cell_types.insert("$lut"); + cell_types.insert("$assert"); } void setup_internals_mem() diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 661525735..7638d4689 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -595,6 +595,13 @@ namespace { return; } + if (cell->type == "$assert") { + port("\\A", 1); + port("\\EN", 1); + check_expected(); + return; + } + if (cell->type == "$_INV_") { check_gate("AY"); return; } if (cell->type == "$_AND_") { check_gate("ABY"); return; } if (cell->type == "$_OR_") { check_gate("ABY"); return; } diff --git a/kernel/satgen.h b/kernel/satgen.h index a668c73a4..0909e58ef 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -38,6 +38,7 @@ struct SatGen SigMap *sigmap; std::string prefix; SigPool initial_state; + RTLIL::SigSpec asserts_a, asserts_en; bool ignore_div_by_zero; bool model_undef; @@ -96,6 +97,19 @@ struct SatGen return importSigSpecWorker(sig, pf, true, false); } + int importAsserts(int timestep = -1) + { + std::vector check_bits, enable_bits; + if (model_undef) { + check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a, timestep)), importDefSigSpec(asserts_a, timestep)); + enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en, timestep)), importDefSigSpec(asserts_en, timestep)); + } else { + check_bits = importDefSigSpec(asserts_a, timestep); + enable_bits = importDefSigSpec(asserts_en, timestep); + } + return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits))); + } + int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1) { if (timestep_rhs < 0) @@ -765,6 +779,13 @@ struct SatGen return true; } + if (cell->type == "$assert") + { + asserts_a.append((*sigmap)(cell->connections.at("\\A"))); + asserts_en.append((*sigmap)(cell->connections.at("\\EN"))); + return true; + } + // Unsupported internal cell types: $pow $lut // .. and all sequential cells except $dff and $_DFF_[NP]_ return false; diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index b84e1b30e..b848a2b60 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -418,3 +418,7 @@ from the gate level logic network can be mapped to physical flip-flop cells from pass. The combinatorial logic cells can be mapped to physical cells from a Liberty file via ABC \citeweblink{ABC} using the {\tt abc} pass. +\begin{fixme} +Add information about {\tt \$assert} cells. +\end{fixme} + diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index 2921c92d8..051d8dc68 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -47,7 +47,7 @@ static void rmunused_module_cells(RTLIL::Module *module, bool verbose) wire2driver.insert(sig, cell); } } - if (cell->type == "$memwr" || cell->get_bool_attribute("\\keep")) + if (cell->type == "$memwr" || cell->type == "$assert" || cell->get_bool_attribute("\\keep")) queue.insert(cell); unused.insert(cell); } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index fef99dfc0..cf3cd59f5 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -47,6 +47,7 @@ struct SatHelper std::vector> sets, prove, prove_x, sets_init; std::map>> sets_at; std::map> unsets_at; + bool prove_asserts; // undef constraints bool enable_undef, set_init_undef; @@ -284,7 +285,7 @@ struct SatHelper int setup_proof(int timestep = -1) { - assert(prove.size() + prove_x.size() > 0); + assert(prove.size() || prove_x.size() || prove_asserts); RTLIL::SigSpec big_lhs, big_rhs; std::vector prove_bits; @@ -352,6 +353,9 @@ struct SatHelper prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i)))))); } + if (prove_asserts) + prove_bits.push_back(satgen.importAsserts(timestep)); + return ez.expression(ezSAT::OpAnd, prove_bits); } @@ -717,15 +721,21 @@ struct SatPass : public Pass { log("The following additional options can be used to set up a proof. If also -seq\n"); log("is passed, a temporal induction proof is performed.\n"); log("\n"); + log(" -tempinduct\n"); + log(" Perform a temporal induction proof. In a temporalinduction proof it is\n"); + log(" proven that the condition holds forever after the number of time steps\n"); + log(" specified using -seq.\n"); + log("\n"); log(" -prove \n"); - log(" Attempt to proof that is always . In a temporal\n"); - log(" induction proof it is proven that the condition holds forever after\n"); - log(" the number of time steps passed using -seq.\n"); + log(" Attempt to proof that is always .\n"); log("\n"); log(" -prove-x \n"); log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n"); log(" the right hand side. Useful for equivialence checking.\n"); log("\n"); + log(" -prove-asserts\n"); + log(" Prove that all asserts in the design hold.\n"); + log("\n"); log(" -maxsteps \n"); log(" Set a maximum length for the induction.\n"); log("\n"); @@ -748,6 +758,7 @@ struct SatPass : public Pass { int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0; bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false; bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false; + bool tempinduct = false, prove_asserts = false; log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); @@ -817,6 +828,10 @@ struct SatPass : public Pass { enable_undef = true; continue; } + if (args[argidx] == "-tempinduct") { + tempinduct = true; + continue; + } if (args[argidx] == "-prove" && argidx+2 < args.size()) { std::string lhs = args[++argidx]; std::string rhs = args[++argidx]; @@ -830,6 +845,10 @@ struct SatPass : public Pass { enable_undef = true; continue; } + if (args[argidx] == "-prove-asserts") { + prove_asserts = true; + continue; + } if (args[argidx] == "-seq" && argidx+1 < args.size()) { seq_len = atoi(args[++argidx].c_str()); continue; @@ -894,16 +913,22 @@ struct SatPass : public Pass { if (module == NULL) log_cmd_error("Can't perform SAT on an empty selection!\n"); - if (prove.size() + prove_x.size() == 0 && verify) + if (!prove.size() && !prove_x.size() && !prove_asserts && verify) log_cmd_error("Got -verify but nothing to prove!\n"); + if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct) + log_cmd_error("Got -tempinduct but nothing to prove!\n"); + + if (seq_len == 0 && tempinduct) + log_cmd_error("Got -tempinduct but no -seq argument!\n"); + if (set_def_inputs) { for (auto &it : module->wires) if (it.second->port_input) sets_def.push_back(it.second->name); } - if (prove.size() + prove_x.size() > 0 && seq_len > 0) + if (tempinduct) { if (loopcount > 0 || max_undef) log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n"); @@ -914,6 +939,7 @@ struct SatPass : public Pass { basecase.sets = sets; basecase.prove = prove; basecase.prove_x = prove_x; + basecase.prove_asserts = prove_asserts; basecase.sets_at = sets_at; basecase.unsets_at = unsets_at; basecase.shows = shows; @@ -935,6 +961,7 @@ struct SatPass : public Pass { inductstep.sets = sets; inductstep.prove = prove; inductstep.prove_x = prove_x; + inductstep.prove_asserts = prove_asserts; inductstep.shows = shows; inductstep.timeout = timeout; inductstep.sets_def = sets_def; @@ -1021,6 +1048,7 @@ struct SatPass : public Pass { sathelper.sets = sets; sathelper.prove = prove; sathelper.prove_x = prove_x; + sathelper.prove_asserts = prove_asserts; sathelper.sets_at = sets_at; sathelper.unsets_at = unsets_at; sathelper.shows = shows; @@ -1037,11 +1065,14 @@ struct SatPass : public Pass { if (seq_len == 0) { sathelper.setup(); - if (sathelper.prove.size() + sathelper.prove_x.size() > 0) + if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof())); } else { - for (int timestep = 1; timestep <= seq_len; timestep++) + for (int timestep = 1; timestep <= seq_len; timestep++) { sathelper.setup(timestep); + if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) + sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof(timestep))); + } sathelper.setup_init(); } sathelper.generate_model(); @@ -1064,7 +1095,7 @@ struct SatPass : public Pass { sathelper.maximize_undefs(); } - if (prove.size() + prove_x.size() == 0) { + if (!prove.size() && !prove_x.size() && !prove_asserts) { log("SAT solving finished - model found:\n"); } else { log("SAT proof finished - model found: FAIL!\n"); @@ -1090,7 +1121,7 @@ struct SatPass : public Pass { goto timeout; if (rerun_counter) log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter); - else if (prove.size() + prove_x.size() == 0) + else if (!prove.size() && !prove_x.size() && !prove_asserts) log("SAT solving finished - no model found.\n"); else { log("SAT proof finished - no model found: SUCCESS!\n"); diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index 0a56932b7..9751a4744 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -3,6 +3,7 @@ OBJS += passes/techmap/techmap.o OBJS += passes/techmap/simplemap.o OBJS += passes/techmap/dfflibmap.o OBJS += passes/techmap/iopadmap.o +OBJS += passes/techmap/hilomap.o OBJS += passes/techmap/libparse.o GENFILES += passes/techmap/stdcells.inc diff --git a/passes/techmap/hilomap.cc b/passes/techmap/hilomap.cc new file mode 100644 index 000000000..bc5caa38c --- /dev/null +++ b/passes/techmap/hilomap.cc @@ -0,0 +1,129 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/register.h" +#include "kernel/rtlil.h" +#include "kernel/log.h" + +static std::string hicell_celltype, hicell_portname; +static std::string locell_celltype, locell_portname; +static bool singleton_mode; + +static RTLIL::Module *module; +static RTLIL::SigChunk last_hi, last_lo; + +void hilomap_worker(RTLIL::SigSpec &sig) +{ + sig.expand(); + for (auto &c : sig.chunks) { + if (c.wire == NULL && (c.data.bits.at(0) == RTLIL::State::S1) && !hicell_celltype.empty()) { + if (!singleton_mode || last_hi.width == 0) { + last_hi = RTLIL::SigChunk(NEW_WIRE(module, 1)); + RTLIL::Cell *cell = new RTLIL::Cell; + cell->name = NEW_ID; + cell->type = RTLIL::escape_id(hicell_celltype); + cell->connections[RTLIL::escape_id(hicell_portname)] = last_hi; + module->add(cell); + } + c = last_hi; + } + if (c.wire == NULL && (c.data.bits.at(0) == RTLIL::State::S0) && !locell_celltype.empty()) { + if (!singleton_mode || last_lo.width == 0) { + last_lo = RTLIL::SigChunk(NEW_WIRE(module, 1)); + RTLIL::Cell *cell = new RTLIL::Cell; + cell->name = NEW_ID; + cell->type = RTLIL::escape_id(locell_celltype); + cell->connections[RTLIL::escape_id(locell_portname)] = last_lo; + module->add(cell); + } + c = last_lo; + } + } + sig.optimize(); +} + +struct HilomapPass : public Pass { + HilomapPass() : Pass("hilomap", "technology mapping of constant hi- and/or lo-drivers") { } + virtual void help() + { + log("\n"); + log(" hilomap [options] [selection]\n"); + log("\n"); + log("Map module inputs/outputs to PAD cells from a library. This pass\n"); + log("can only map to very simple PAD cells. Use 'techmap' to further map\n"); + log("the resulting cells to more sophisticated PAD cells.\n"); + log("\n"); + log(" -hicell \n"); + log(" Replace constant hi bits with this cell.\n"); + log("\n"); + log(" -locell \n"); + log(" Replace constant lo bits with this cell.\n"); + log("\n"); + log(" -singleton\n"); + log(" Create only one hi/lo cell and connect all constant bits\n"); + log(" to that cell. Per default a separate cell is created for\n"); + log(" each constant bit.\n"); + log("\n"); + } + virtual void execute(std::vector args, RTLIL::Design *design) + { + log_header("Executing HILOPAD pass (mapping to constant drivers).\n"); + + hicell_celltype = std::string(); + hicell_portname = std::string(); + locell_celltype = std::string(); + locell_portname = std::string(); + singleton_mode = false; + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-hicell" && argidx+2 < args.size()) { + hicell_celltype = args[++argidx]; + hicell_portname = args[++argidx]; + continue; + } + if (args[argidx] == "-locell" && argidx+2 < args.size()) { + locell_celltype = args[++argidx]; + locell_portname = args[++argidx]; + continue; + } + if (args[argidx] == "-singleton") { + singleton_mode = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + for (auto &it : design->modules) + { + module = it.second; + + if (!design->selected(module)) + continue; + + last_hi = RTLIL::SigChunk(); + last_lo = RTLIL::SigChunk(); + + module->rewrite_sigspecs(hilomap_worker); + } + } +} HilomapPass; + diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index f3d652f0e..8f354a63d 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -65,10 +65,10 @@ parameter Y_WIDTH = 0; output [Y_WIDTH-1:0] Y; generate - if (!A_SIGNED && 0 < A_WIDTH && A_WIDTH < Y_WIDTH) begin:A + if (!A_SIGNED && 0 < A_WIDTH && A_WIDTH < Y_WIDTH) begin:BLOCK1 assign Y[A_WIDTH-1:0] = A_BUF.val; assign Y[Y_WIDTH-1:A_WIDTH] = 0; - end else begin:B + end else begin:BLOCK2 assign Y = +A_BUF.val; end endgenerate @@ -715,16 +715,33 @@ generate \$lut #( .WIDTH(WIDTH-1), .LUT(LUT ) ) lut0 ( .I(I[WIDTH-2:0]), .O(lut0_out) ); \$lut #( .WIDTH(WIDTH-1), .LUT(LUT >> (2**(WIDTH-1))) ) lut1 ( .I(I[WIDTH-2:0]), .O(lut1_out) ); end + + if (WIDTH > 0) begin:lutlogic + always @* begin + casez ({I[WIDTH-1], lut0_out, lut1_out}) + 3'b?11: O = 1'b1; + 3'b?00: O = 1'b0; + 3'b0??: O = lut0_out; + 3'b1??: O = lut1_out; + default: O = 1'bx; + endcase + end + end endgenerate +endmodule + +// -------------------------------------------------------- + +module \$assert (A, EN); + +input A, EN; + always @* begin - casez ({I[WIDTH-1], lut0_out, lut1_out}) - 3'b?11: O = 1'b1; - 3'b?00: O = 1'b0; - 3'b0??: O = lut0_out; - 3'b1??: O = lut1_out; - default: O = 1'bx; - endcase + if (A !== 1'b1 && EN === 1'b1) begin + $display("Assertation failed!"); + $finish; + end end endmodule @@ -953,8 +970,10 @@ input [ABITS-1:0] ADDR; output [WIDTH-1:0] DATA; initial begin - $display("ERROR: Found non-simulatable instance of $memrd!"); - $finish; + if (MEMID != "") begin + $display("ERROR: Found non-simulatable instance of $memrd!"); + $finish; + end end endmodule @@ -975,8 +994,10 @@ input [ABITS-1:0] ADDR; input [WIDTH-1:0] DATA; initial begin - $display("ERROR: Found non-simulatable instance of $memwr!"); - $finish; + if (MEMID != "") begin + $display("ERROR: Found non-simulatable instance of $memwr!"); + $finish; + end end endmodule @@ -1008,7 +1029,7 @@ input [WR_PORTS*ABITS-1:0] WR_ADDR; input [WR_PORTS*WIDTH-1:0] WR_DATA; reg [WIDTH-1:0] data [SIZE-1:0]; -event update_async_rd; +reg update_async_rd; genvar i; generate @@ -1032,21 +1053,21 @@ generate always @(WR_ADDR or WR_DATA or WR_EN) begin if (WR_EN[i]) begin data[ WR_ADDR[ (i+1)*ABITS-1 : i*ABITS ] - OFFSET ] <= WR_DATA[ (i+1)*WIDTH-1 : i*WIDTH ]; - #1 -> update_async_rd; + update_async_rd <= 1; update_async_rd <= 0; end end end else - if (RD_CLK_POLARITY[i] == 1) begin:rd_posclk + if (WR_CLK_POLARITY[i] == 1) begin:rd_posclk always @(posedge WR_CLK[i]) if (WR_EN[i]) begin data[ WR_ADDR[ (i+1)*ABITS-1 : i*ABITS ] - OFFSET ] <= WR_DATA[ (i+1)*WIDTH-1 : i*WIDTH ]; - #1 -> update_async_rd; + update_async_rd <= 1; update_async_rd <= 0; end end else begin:rd_negclk always @(negedge WR_CLK[i]) if (WR_EN[i]) begin data[ WR_ADDR[ (i+1)*ABITS-1 : i*ABITS ] - OFFSET ] <= WR_DATA[ (i+1)*WIDTH-1 : i*WIDTH ]; - #1 -> update_async_rd; + update_async_rd <= 1; update_async_rd <= 0; end end end