This commit is contained in:
Andrew Zonenberg 2017-01-05 06:05:58 -08:00
commit ac90de73be
5 changed files with 135 additions and 42 deletions

View File

@ -201,10 +201,9 @@ for fn in inconstr:
current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
constr_final_start = 0
elif len(tokens) == 2:
i = int(tokens[1])
assert i < 0
current_states = set(["final-%d" % i for i in range(-i, num_steps+1)])
constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i)
arg = abs(int(tokens[1]))
current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
else:
assert False
continue
@ -232,9 +231,8 @@ for fn in inconstr:
if len(tokens) == 1:
current_states = set(range(0, num_steps+1))
elif len(tokens) == 2:
i = int(tokens[1])
assert i < 0
current_states = set(range(-i, num_steps+1))
arg = abs(int(tokens[1]))
current_states = set(range(arg, num_steps+1))
else:
assert False
continue

View File

@ -16,7 +16,7 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import sys, subprocess, re
import sys, subprocess, re, os
from copy import deepcopy
from select import select
from time import time
@ -73,7 +73,7 @@ class SmtIo:
self.debug_print = False
self.debug_file = None
self.dummy_file = None
self.timeinfo = True
self.timeinfo = os.name != "nt"
self.unroll = False
self.noincr = False
self.info_stmts = list()
@ -618,7 +618,7 @@ class SmtOpts:
self.dummy_file = None
self.unroll = False
self.noincr = False
self.timeinfo = True
self.timeinfo = os.name != "nt"
self.logic = None
self.info_stmts = list()
self.nocomments = False
@ -633,7 +633,7 @@ class SmtOpts:
elif o == "--noincr":
self.noincr = True
elif o == "--noprogress":
self.timeinfo = True
self.timeinfo = False
elif o == "--dump-smt2":
self.debug_file = open(a, "w")
elif o == "--logic":
@ -673,6 +673,7 @@ class SmtOpts:
--noprogress
disable timer display during solving
(this option is set implicitly on Windows)
--dump-smt2 <filename>
write smt2 statements to file

View File

@ -1083,6 +1083,15 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
did_something = true;
}
// check for local objects in unnamed block
if (type == AST_BLOCK && str.empty())
{
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)
log_error("Local declaration in unnamed block at %s:%d is an unsupported SystemVerilog feature!\n",
children[i]->filename.c_str(), children[i]->linenum);
}
// transform block with name
if (type == AST_BLOCK && !str.empty())
{
@ -1091,7 +1100,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
std::vector<AstNode*> new_children;
for (size_t i = 0; i < children.size(); i++)
if (children[i]->type == AST_WIRE || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM) {
if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM) {
children[i]->simplify(false, false, false, stage, -1, false, false);
current_ast_mod->children.push_back(children[i]);
current_scope[children[i]->str] = children[i];
@ -1864,7 +1873,8 @@ skip_dynamic_range_lvalue_expansion:;
if (str == "\\$ln" || str == "\\$log10" || str == "\\$exp" || str == "\\$sqrt" || str == "\\$pow" ||
str == "\\$floor" || str == "\\$ceil" || str == "\\$sin" || str == "\\$cos" || str == "\\$tan" ||
str == "\\$asin" || str == "\\$acos" || str == "\\$atan" || str == "\\$atan2" || str == "\\$hypot" ||
str == "\\$sinh" || str == "\\$cosh" || str == "\\$tanh" || str == "\\$asinh" || str == "\\$acosh" || str == "\\$atanh")
str == "\\$sinh" || str == "\\$cosh" || str == "\\$tanh" || str == "\\$asinh" || str == "\\$acosh" || str == "\\$atanh" ||
str == "\\$rtoi" || str == "\\$itor")
{
bool func_with_two_arguments = str == "\\$pow" || str == "\\$atan2" || str == "\\$hypot";
double x = 0, y = 0;
@ -1901,29 +1911,34 @@ skip_dynamic_range_lvalue_expansion:;
y = children[1]->asReal(child_sign_hint);
}
newNode = new AstNode(AST_REALVALUE);
if (str == "\\$ln") newNode->realvalue = ::log(x);
else if (str == "\\$log10") newNode->realvalue = ::log10(x);
else if (str == "\\$exp") newNode->realvalue = ::exp(x);
else if (str == "\\$sqrt") newNode->realvalue = ::sqrt(x);
else if (str == "\\$pow") newNode->realvalue = ::pow(x, y);
else if (str == "\\$floor") newNode->realvalue = ::floor(x);
else if (str == "\\$ceil") newNode->realvalue = ::ceil(x);
else if (str == "\\$sin") newNode->realvalue = ::sin(x);
else if (str == "\\$cos") newNode->realvalue = ::cos(x);
else if (str == "\\$tan") newNode->realvalue = ::tan(x);
else if (str == "\\$asin") newNode->realvalue = ::asin(x);
else if (str == "\\$acos") newNode->realvalue = ::acos(x);
else if (str == "\\$atan") newNode->realvalue = ::atan(x);
else if (str == "\\$atan2") newNode->realvalue = ::atan2(x, y);
else if (str == "\\$hypot") newNode->realvalue = ::hypot(x, y);
else if (str == "\\$sinh") newNode->realvalue = ::sinh(x);
else if (str == "\\$cosh") newNode->realvalue = ::cosh(x);
else if (str == "\\$tanh") newNode->realvalue = ::tanh(x);
else if (str == "\\$asinh") newNode->realvalue = ::asinh(x);
else if (str == "\\$acosh") newNode->realvalue = ::acosh(x);
else if (str == "\\$atanh") newNode->realvalue = ::atanh(x);
else log_abort();
if (str == "\\$rtoi") {
newNode = AstNode::mkconst_int(x, true);
} else {
newNode = new AstNode(AST_REALVALUE);
if (str == "\\$ln") newNode->realvalue = ::log(x);
else if (str == "\\$log10") newNode->realvalue = ::log10(x);
else if (str == "\\$exp") newNode->realvalue = ::exp(x);
else if (str == "\\$sqrt") newNode->realvalue = ::sqrt(x);
else if (str == "\\$pow") newNode->realvalue = ::pow(x, y);
else if (str == "\\$floor") newNode->realvalue = ::floor(x);
else if (str == "\\$ceil") newNode->realvalue = ::ceil(x);
else if (str == "\\$sin") newNode->realvalue = ::sin(x);
else if (str == "\\$cos") newNode->realvalue = ::cos(x);
else if (str == "\\$tan") newNode->realvalue = ::tan(x);
else if (str == "\\$asin") newNode->realvalue = ::asin(x);
else if (str == "\\$acos") newNode->realvalue = ::acos(x);
else if (str == "\\$atan") newNode->realvalue = ::atan(x);
else if (str == "\\$atan2") newNode->realvalue = ::atan2(x, y);
else if (str == "\\$hypot") newNode->realvalue = ::hypot(x, y);
else if (str == "\\$sinh") newNode->realvalue = ::sinh(x);
else if (str == "\\$cosh") newNode->realvalue = ::cosh(x);
else if (str == "\\$tanh") newNode->realvalue = ::tanh(x);
else if (str == "\\$asinh") newNode->realvalue = ::asinh(x);
else if (str == "\\$acosh") newNode->realvalue = ::acosh(x);
else if (str == "\\$atanh") newNode->realvalue = ::atanh(x);
else if (str == "\\$itor") newNode->realvalue = x;
else log_abort();
}
goto apply_newNode;
}
@ -2158,7 +2173,7 @@ skip_dynamic_range_lvalue_expansion:;
}
for (auto child : decl->children)
if (child->type == AST_WIRE || child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
if (child->type == AST_WIRE || child->type == AST_MEMORY || child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
{
AstNode *wire = nullptr;
@ -2218,7 +2233,7 @@ skip_dynamic_range_lvalue_expansion:;
}
for (auto child : decl->children)
if (child->type != AST_WIRE && child->type != AST_PARAMETER && child->type != AST_LOCALPARAM)
if (child->type != AST_WIRE && child->type != AST_MEMORY && child->type != AST_PARAMETER && child->type != AST_LOCALPARAM)
{
AstNode *stmt = child->clone();
stmt->replace_ids(prefix, replace_rules);

View File

@ -44,6 +44,9 @@ struct CheckPass : public Pass {
log("When called with -noinit then this command also checks for wires which have\n");
log("the 'init' attribute set.\n");
log("\n");
log("When called with -initdrv then this command also checks for wires which have\n");
log("the 'init' attribute set and aren't driven by a FF cell type.\n");
log("\n");
log("When called with -assert then the command will produce an error if any\n");
log("problems are found in the current design.\n");
log("\n");
@ -52,6 +55,7 @@ struct CheckPass : public Pass {
{
int counter = 0;
bool noinit = false;
bool initdrv = false;
bool assert_mode = false;
size_t argidx;
@ -60,6 +64,10 @@ struct CheckPass : public Pass {
noinit = true;
continue;
}
if (args[argidx] == "-initdrv") {
initdrv = true;
continue;
}
if (args[argidx] == "-assert") {
assert_mode = true;
continue;
@ -70,6 +78,49 @@ struct CheckPass : public Pass {
log_header(design, "Executing CHECK pass (checking for obvious problems).\n");
pool<IdString> fftypes;
fftypes.insert("$sr");
fftypes.insert("$ff");
fftypes.insert("$dff");
fftypes.insert("$dffe");
fftypes.insert("$dffsr");
fftypes.insert("$adff");
fftypes.insert("$dlatch");
fftypes.insert("$dlatchsr");
fftypes.insert("$_DFFE_NN_");
fftypes.insert("$_DFFE_NP_");
fftypes.insert("$_DFFE_PN_");
fftypes.insert("$_DFFE_PP_");
fftypes.insert("$_DFFSR_NNN_");
fftypes.insert("$_DFFSR_NNP_");
fftypes.insert("$_DFFSR_NPN_");
fftypes.insert("$_DFFSR_NPP_");
fftypes.insert("$_DFFSR_PNN_");
fftypes.insert("$_DFFSR_PNP_");
fftypes.insert("$_DFFSR_PPN_");
fftypes.insert("$_DFFSR_PPP_");
fftypes.insert("$_DFF_NN0_");
fftypes.insert("$_DFF_NN1_");
fftypes.insert("$_DFF_NP0_");
fftypes.insert("$_DFF_NP1_");
fftypes.insert("$_DFF_N_");
fftypes.insert("$_DFF_PN0_");
fftypes.insert("$_DFF_PN1_");
fftypes.insert("$_DFF_PP0_");
fftypes.insert("$_DFF_PP1_");
fftypes.insert("$_DFF_P_");
fftypes.insert("$_DLATCHSR_NNN_");
fftypes.insert("$_DLATCHSR_NNP_");
fftypes.insert("$_DLATCHSR_NPN_");
fftypes.insert("$_DLATCHSR_NPP_");
fftypes.insert("$_DLATCHSR_PNN_");
fftypes.insert("$_DLATCHSR_PNP_");
fftypes.insert("$_DLATCHSR_PPN_");
fftypes.insert("$_DLATCHSR_PPP_");
fftypes.insert("$_DLATCH_N_");
fftypes.insert("$_DLATCH_P_");
fftypes.insert("$_FF_");
for (auto module : design->selected_whole_modules_warn())
{
if (module->has_processes_warn())
@ -109,6 +160,8 @@ struct CheckPass : public Pass {
if (bit.wire) wire_drivers_count[bit]++;
}
pool<SigBit> init_bits;
for (auto wire : module->wires()) {
if (wire->port_input) {
SigSpec sig = sigmap(wire);
@ -121,9 +174,15 @@ struct CheckPass : public Pass {
if (wire->port_input && !wire->port_output)
for (auto bit : sigmap(wire))
if (bit.wire) wire_drivers_count[bit]++;
if (noinit && wire->attributes.count("\\init")) {
log_warning("Wire %s.%s has an unprocessed 'init' attribute.\n", log_id(module), log_id(wire));
counter++;
if (wire->attributes.count("\\init")) {
Const initval = wire->attributes.at("\\init");
for (int i = 0; i < GetSize(initval) && i < GetSize(wire); i++)
if (initval[i] == State::S0 || initval[i] == State::S1)
init_bits.insert(sigmap(SigBit(wire, i)));
if (noinit) {
log_warning("Wire %s.%s has an unprocessed 'init' attribute.\n", log_id(module), log_id(wire));
counter++;
}
}
}
@ -150,6 +209,26 @@ struct CheckPass : public Pass {
log_warning("%s", message.c_str());
counter++;
}
if (initdrv)
{
for (auto cell : module->cells())
{
if (fftypes.count(cell->type) == 0)
continue;
for (auto bit : sigmap(cell->getPort("\\Q")))
init_bits.erase(bit);
}
SigSpec init_sig(init_bits);
init_sig.sort_and_unify();
for (auto chunk : init_sig.chunks()) {
log_warning("Wire %s.%s has 'init' attribute and is not driven by an FF cell.\n", log_id(module), log_signal(chunk));
counter++;
}
}
}
log("found and reported %d problems.\n", counter);

View File

@ -2,7 +2,7 @@
module array_test001(a, b, c, y);
input a;
input [31:0] b, c;
input [31:0] y;
output [31:0] y;
aoi12 p [31:0] (a, b, c, y);
endmodule