Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 34e2fb594d23
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: fa535c0b0041
Choose a head ref

Commits on Sep 30, 2016

  1. Copy the full SHA
    ca54625 View commit details
  2. Copy the full SHA
    ed519f5 View commit details
  3. Added "prep -nokeepdc"

    cliffordwolf committed Sep 30, 2016
    Copy the full SHA
    76352c9 View commit details

Commits on Oct 1, 2016

  1. Copy the full SHA
    2359459 View commit details
  2. Copy the full SHA
    4eb0d6f View commit details

Commits on Oct 2, 2016

  1. Copy the full SHA
    9aec8a1 View commit details
  2. Copy the full SHA
    e586e5e View commit details

Commits on Oct 3, 2016

  1. Copy the full SHA
    99b2093 View commit details
  2. Copy the full SHA
    1114ce9 View commit details
  3. Copy the full SHA
    5f7c5e6 View commit details

Commits on Oct 8, 2016

  1. Copy the full SHA
    5f6a838 View commit details

Commits on Oct 11, 2016

  1. Copy the full SHA
    11130d5 View commit details
  2. Copy the full SHA
    59508c9 View commit details
  3. Copy the full SHA
    4a981a3 View commit details
  4. Copy the full SHA
    8ebba8a View commit details

Commits on Oct 12, 2016

  1. Added "zinit" pass

    cliffordwolf committed Oct 12, 2016
    Copy the full SHA
    ee91350 View commit details

Commits on Oct 13, 2016

  1. Added a new configuration variable GIT_REV_WHERE

    It determines from where we get the gits SHA1 value. By default is HEAD,
    suitable for Clifford, but for Debian we can define it as upstream/master
    set-soft committed Oct 13, 2016
    Copy the full SHA
    77ce813 View commit details
  2. Modified test target name (to test-all)

    As this target depends on external tools, and packagers run "make test",
    I think the name should be less generic.
    set-soft committed Oct 13, 2016
    Copy the full SHA
    f263b17 View commit details
  3. Allow to overwrite ABCEXTERNAL from the environment.

    In this way Debian scripts can define it as berkeley-abc from the shell.
    set-soft committed Oct 13, 2016
    Copy the full SHA
    cc8f29a View commit details
  4. Copy the full SHA
    80749f1 View commit details

Commits on Oct 14, 2016

  1. Copy the full SHA
    788e511 View commit details
  2. Merge pull request YosysHQ#246 from set-soft/abc_external_ovr

    Allow to overwrite ABCEXTERNAL from the environment.
    cliffordwolf authored Oct 14, 2016
    Copy the full SHA
    3c42462 View commit details
  3. Copy the full SHA
    09aeb9a View commit details
  4. Copy the full SHA
    ffbb4e9 View commit details
  5. Copy the full SHA
    53655d1 View commit details
  6. Copy the full SHA
    2ef454c View commit details
  7. Added clk2fflogic

    cliffordwolf committed Oct 14, 2016
    Copy the full SHA
    2733994 View commit details
  8. Added $anyseq cell type

    cliffordwolf committed Oct 14, 2016
    Copy the full SHA
    bdc316d View commit details
  9. Copy the full SHA
    512f93f View commit details
  10. Copy the full SHA
    7fc69b3 View commit details
  11. Avoid using strcasecmp()

    cliffordwolf committed Oct 14, 2016
    Copy the full SHA
    e4c5ee9 View commit details
  12. Copy the full SHA
    fa535c0 View commit details
12 changes: 7 additions & 5 deletions Makefile
Original file line number Diff line number Diff line change
@@ -72,7 +72,7 @@ else
LDLIBS += -lrt
endif

YOSYS_VER := 0.6+$(shell test -e .git && { git log --author=clifford@clifford.at --oneline 5869d26da021.. | wc -l; })
YOSYS_VER := 0.6+$(shell cd $(YOSYS_SRC) && test -e .git && { git log --author=clifford@clifford.at --oneline 5869d26da021.. | wc -l; })
GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
OBJS = kernel/version_$(GIT_REV).o

@@ -82,14 +82,14 @@ OBJS = kernel/version_$(GIT_REV).o
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
ABCREV = 8e08604f8ad3
ABCREV = eb6eca6807cc
ABCPULL = 1
ABCURL ?= https://bitbucket.org/alanmi/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"

# set ABCEXTERNAL = <abc-command> to use an external ABC instance
# Note: The in-tree ABC (yosys-abc) will not be installed when ABCEXTERNAL is set.
ABCEXTERNAL =
ABCEXTERNAL ?=

define newline

@@ -370,10 +370,12 @@ libyosys.so: $(filter-out kernel/driver.o,$(OBJS))
$(Q) mkdir -p $(dir $@)
$(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $<

YOSYS_VER_STR := Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) $(shell \
$(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1) $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)))

kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile
$(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc
$(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) ` \
$(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1` $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)))\"; }" > kernel/version_$(GIT_REV).cc
$(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"$(YOSYS_VER_STR)\"; }" > kernel/version_$(GIT_REV).cc

yosys-config: misc/yosys-config.in
$(P) $(SED) -e 's#@CXXFLAGS@#$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(CXXFLAGS))#;' \
25 changes: 23 additions & 2 deletions README
Original file line number Diff line number Diff line change
@@ -374,6 +374,27 @@ Verilog Attributes and non-standard features
and constant values). The intended use for this is synthesis-time DRC.


Non-standard or SystemVerilog features for formal verification
==============================================================

- Support for "assert", "assume", and "restrict" is enabled when
read_verilog is called with -formal.

- The system task $initstate evaluates to 1 in the initial state and
to 0 otherwise.

- The system task $anyconst evaluates to any constant value.

- The system task $anyseq evaluates to any value, possibly a different
value in each cycle.

- The SystemVerilog tasks $past, $stable, $rose and $fell are supported
in any clocked block.

- The syntax @($global_clock) can be used to create FFs that have no
explicit clock input ($ff cells).


Supported features from SystemVerilog
=====================================

@@ -384,8 +405,8 @@ from SystemVerilog:
form. In module context: "assert property (<expression>);" and within an
always block: "assert(<expression>);". It is transformed to a $assert cell.

- The "assume" statements from SystemVerilog are also supported. The same
limitations as with the "assert" statement apply.
- The "assume" and "restrict" statements from SystemVerilog are also
supported. The same limitations as with the "assert" statement apply.

- The keywords "always_comb", "always_ff" and "always_latch", "logic" and
"bit" are supported.
6 changes: 6 additions & 0 deletions backends/blif/blif.cc
Original file line number Diff line number Diff line change
@@ -315,6 +315,12 @@ struct BlifDumper
continue;
}

if (!config->icells_mode && cell->type == "$_FF_") {
f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
cstr_init(cell->getPort("\\Q")));
continue;
}

if (!config->icells_mode && cell->type == "$_DFF_N_") {
f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
1 change: 1 addition & 0 deletions backends/ilang/ilang_backend.cc
Original file line number Diff line number Diff line change
@@ -228,6 +228,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT
f << stringf("\n");
break;
case RTLIL::STa: f << stringf("always\n"); break;
case RTLIL::STg: f << stringf("global\n"); break;
case RTLIL::STi: f << stringf("init\n"); break;
}

12 changes: 6 additions & 6 deletions backends/smt2/smt2.cc
Original file line number Diff line number Diff line change
@@ -379,7 +379,7 @@ struct Smt2Worker
return;
}

if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
@@ -407,7 +407,7 @@ struct Smt2Worker

if (bvmode)
{
if (cell->type == "$dff")
if (cell->type.in("$ff", "$dff"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
@@ -417,7 +417,7 @@ struct Smt2Worker
return;
}

if (cell->type == "$anyconst")
if (cell->type.in("$anyconst", "$anyseq"))
{
registers.insert(cell);
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
@@ -596,7 +596,7 @@ struct Smt2Worker

pool<SigBit> reg_bits;
for (auto cell : module->cells())
if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
// not using sigmap -- we want the net directly at the dff output
for (auto bit : cell->getPort("\\Q"))
reg_bits.insert(bit);
@@ -674,14 +674,14 @@ struct Smt2Worker

for (auto cell : this_regs)
{
if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
std::string expr_d = get_bool(cell->getPort("\\D"));
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
}

if (cell->type == "$dff")
if (cell->type.in("$ff", "$dff"))
{
std::string expr_d = get_bv(cell->getPort("\\D"));
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
2 changes: 1 addition & 1 deletion backends/smt2/smtbmc.py
Original file line number Diff line number Diff line change
@@ -249,7 +249,7 @@ def get_constr_expr(db, state, final=False, getvalues=False):
if state not in db:
return ([], [], []) if getvalues else "true"

netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*)\](?=[ )]|$)')

def replace_netref(match):
state_sel = match.group(2)
65 changes: 55 additions & 10 deletions backends/smt2/smtio.py
Original file line number Diff line number Diff line change
@@ -54,6 +54,8 @@ def __init__(self, opts=None):
self.logic_uf = True
self.logic_bv = True
self.produce_models = True
self.smt2cache = [list()]
self.p = None

if opts is not None:
self.logic = opts.logic
@@ -63,6 +65,7 @@ def __init__(self, opts=None):
self.dummy_file = opts.dummy_file
self.timeinfo = opts.timeinfo
self.unroll = opts.unroll
self.noincr = opts.noincr
self.info_stmts = opts.info_stmts
self.nocomments = opts.nocomments

@@ -73,32 +76,40 @@ def __init__(self, opts=None):
self.dummy_file = None
self.timeinfo = True
self.unroll = False
self.noincr = False
self.info_stmts = list()
self.nocomments = False

if self.solver == "yices":
popen_vargs = ['yices-smt2', '--incremental']
self.popen_vargs = ['yices-smt2', '--incremental']

if self.solver == "z3":
popen_vargs = ['z3', '-smt2', '-in']
self.popen_vargs = ['z3', '-smt2', '-in']

if self.solver == "cvc4":
popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']

if self.solver == "mathsat":
popen_vargs = ['mathsat']
self.popen_vargs = ['mathsat']

if self.solver == "boolector":
popen_vargs = ['boolector', '--smt2', '-i']
self.popen_vargs = ['boolector', '--smt2', '-i']
self.unroll = True

if self.solver == "abc":
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
self.logic_ax = False
self.unroll = True
self.noincr = True

if self.solver == "dummy":
assert self.dummy_file is not None
self.dummy_fd = open(self.dummy_file, "r")
else:
if self.dummy_file is not None:
self.dummy_fd = open(self.dummy_file, "w")
self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
if not self.noincr:
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)

if self.unroll:
self.logic_uf = False
@@ -258,8 +269,22 @@ def write(self, stmt, unroll=True):
self.debug_file.flush()

if self.solver != "dummy":
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
self.p.stdin.flush()
if self.noincr:
if self.p is not None and not stmt.startswith("(get-"):
self.p.stdin.close()
self.p = None
if stmt == "(push 1)":
self.smt2cache.append(list())
elif stmt == "(pop 1)":
self.smt2cache.pop()
else:
if self.p is not None:
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
self.p.stdin.flush()
self.smt2cache[-1].append(stmt)
else:
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
self.p.stdin.flush()

def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"):
@@ -372,6 +397,15 @@ def check_sat(self):
self.debug_file.flush()

if self.solver != "dummy":
if self.noincr:
if self.p is not None:
self.p.stdin.close()
self.p = None
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
for cache_ctx in self.smt2cache:
for cache_stmt in cache_ctx:
self.p.stdin.write(bytes(cache_stmt + "\n", "ascii"))

self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
self.p.stdin.flush()

@@ -507,6 +541,10 @@ def get_path(self, mod, path):
def net_expr(self, mod, base, path):
if len(path) == 1:
assert mod in self.modinfo
if path[0] == "":
return base
if path[0] in self.modinfo[mod].cells:
return "(|%s_h %s| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].wsize:
return "(|%s_n %s| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].memories:
@@ -567,19 +605,20 @@ def get_net_bin_list(self, mod_name, net_path_list, state_name):
return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]

def wait(self):
if self.solver != "dummy":
if self.p is not None:
self.p.wait()


class SmtOpts:
def __init__(self):
self.shortopts = "s:v"
self.longopts = ["unroll", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "z3"
self.debug_print = False
self.debug_file = None
self.dummy_file = None
self.unroll = False
self.noincr = False
self.timeinfo = True
self.logic = None
self.info_stmts = list()
@@ -592,6 +631,8 @@ def handle(self, o, a):
self.debug_print = True
elif o == "--unroll":
self.unroll = True
elif o == "--noincr":
self.noincr = True
elif o == "--noprogress":
self.timeinfo = True
elif o == "--dump-smt2":
@@ -627,6 +668,10 @@ def helpmsg(self):
--unroll
unroll uninterpreted functions
--noincr
don't use incremental solving, instead restart solver for
each (check-sat). This also avoids (push) and (pop).
--noprogress
disable timer display during solving
3 changes: 2 additions & 1 deletion examples/smtbmc/demo7.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
// Demo for memory initialization

module demo7 (input [2:0] addr);
module demo7;
wire [2:0] addr = $anyseq;
reg [15:0] memory [0:7];

initial begin
19 changes: 13 additions & 6 deletions frontends/ast/genrtlil.cc
Original file line number Diff line number Diff line change
@@ -220,12 +220,19 @@ struct AST_INTERNAL::ProcessGenerator
subst_lvalue_to = new_temp_signal(subst_lvalue_from);
subst_lvalue_map = subst_lvalue_from.to_sigbit_map(subst_lvalue_to);

bool found_global_syncs = false;
bool found_anyedge_syncs = false;
for (auto child : always->children)
if (child->type == AST_EDGE)
found_anyedge_syncs = true;
if (child->type == AST_EDGE) {
if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->str == "\\$global_clock")
found_global_syncs = true;
else
found_anyedge_syncs = true;
}

if (found_anyedge_syncs) {
if (found_global_syncs)
log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
log("Note: Assuming pure combinatorial block at %s:%d in\n", always->filename.c_str(), always->linenum);
log("compliance with IEC 62142(E):2005 / IEEE Std. 1364.1(E):2002. Recommending\n");
log("use of @* instead of @(...) for better match of synthesis and simulation.\n");
@@ -236,7 +243,7 @@ struct AST_INTERNAL::ProcessGenerator
for (auto child : always->children)
if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) {
found_clocked_sync = true;
if (found_anyedge_syncs)
if (found_global_syncs || found_anyedge_syncs)
log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
RTLIL::SyncRule *syncrule = new RTLIL::SyncRule;
syncrule->type = child->type == AST_POSEDGE ? RTLIL::STp : RTLIL::STn;
@@ -248,7 +255,7 @@ struct AST_INTERNAL::ProcessGenerator
}
if (proc->syncs.empty()) {
RTLIL::SyncRule *syncrule = new RTLIL::SyncRule;
syncrule->type = RTLIL::STa;
syncrule->type = found_global_syncs ? RTLIL::STg : RTLIL::STa;
syncrule->signal = RTLIL::SigSpec();
addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true);
proc->syncs.push_back(syncrule);
@@ -755,7 +762,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
break;

case AST_FCALL:
if (str == "\\$anyconst") {
if (str == "\\$anyconst" || str == "\\$anyseq") {
if (GetSize(children) == 1) {
while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { }
if (children[0]->type != AST_CONSTANT)
@@ -1458,7 +1465,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
} break;

case AST_FCALL: {
if (str == "\\$anyconst")
if (str == "\\$anyconst" || str == "\\$anyseq")
{
string myid = stringf("%s$%d", str.c_str() + 1, autoidx++);
int width = width_hint;
4 changes: 2 additions & 2 deletions frontends/ast/simplify.cc
Original file line number Diff line number Diff line change
@@ -1807,8 +1807,8 @@ skip_dynamic_range_lvalue_expansion:;
goto apply_newNode;
}

// $anyconst is mapped in AstNode::genRTLIL()
if (str == "\\$anyconst") {
// $anyconst and $anyseq are mapped in AstNode::genRTLIL()
if (str == "\\$anyconst" || str == "\\$anyseq") {
recursion_counter--;
return false;
}
Loading