From 3f0bb441f8a3014bf6b3a656b673fc07663bda76 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 4 Feb 2019 16:46:24 -0800 Subject: Add tests --- tests/aig/and.aag | 5 +++++ tests/aig/buffer.aag | 3 +++ tests/aig/cnt1.aag | 3 +++ tests/aig/cnt1e.aag | 8 ++++++++ tests/aig/empty.aag | 1 + tests/aig/false.aag | 2 ++ tests/aig/halfadder.aag | 14 ++++++++++++++ tests/aig/inverter.aag | 3 +++ tests/aig/notcnt1.aag | 4 ++++ tests/aig/notcnt1e.aag | 8 ++++++++ tests/aig/or.aag | 5 +++++ tests/aig/run-test.sh | 20 ++++++++++++++++++++ tests/aig/toggle-re.aag | 14 ++++++++++++++ tests/aig/toggle.aag | 4 ++++ tests/aig/true.aag | 2 ++ tests/tools/autotest.sh | 21 +++++++++++++-------- 16 files changed, 109 insertions(+), 8 deletions(-) create mode 100644 tests/aig/and.aag create mode 100644 tests/aig/buffer.aag create mode 100644 tests/aig/cnt1.aag create mode 100644 tests/aig/cnt1e.aag create mode 100644 tests/aig/empty.aag create mode 100644 tests/aig/false.aag create mode 100644 tests/aig/halfadder.aag create mode 100644 tests/aig/inverter.aag create mode 100644 tests/aig/notcnt1.aag create mode 100644 tests/aig/notcnt1e.aag create mode 100644 tests/aig/or.aag create mode 100755 tests/aig/run-test.sh create mode 100644 tests/aig/toggle-re.aag create mode 100644 tests/aig/toggle.aag create mode 100644 tests/aig/true.aag diff --git a/tests/aig/and.aag b/tests/aig/and.aag new file mode 100644 index 000000000..d1ef2c5a5 --- /dev/null +++ b/tests/aig/and.aag @@ -0,0 +1,5 @@ +aag 3 2 0 1 1 +2 +4 +6 +6 2 4 diff --git a/tests/aig/buffer.aag b/tests/aig/buffer.aag new file mode 100644 index 000000000..94a6fb1ed --- /dev/null +++ b/tests/aig/buffer.aag @@ -0,0 +1,3 @@ +aag 1 1 0 1 0 +2 +2 diff --git a/tests/aig/cnt1.aag b/tests/aig/cnt1.aag new file mode 100644 index 000000000..ce4f28fcb --- /dev/null +++ b/tests/aig/cnt1.aag @@ -0,0 +1,3 @@ +aag 1 0 1 0 0 1 +2 3 +2 diff --git a/tests/aig/cnt1e.aag b/tests/aig/cnt1e.aag new file mode 100644 index 000000000..6db3f0ffd --- /dev/null +++ b/tests/aig/cnt1e.aag @@ -0,0 +1,8 @@ +aag 5 1 1 0 3 1 +2 +4 10 +4 +6 5 3 +8 4 2 +10 9 7 +b0 AIGER_NEVER diff --git a/tests/aig/empty.aag b/tests/aig/empty.aag new file mode 100644 index 000000000..40c0f00cb --- /dev/null +++ b/tests/aig/empty.aag @@ -0,0 +1 @@ +aag 0 0 0 0 0 diff --git a/tests/aig/false.aag b/tests/aig/false.aag new file mode 100644 index 000000000..421e64a91 --- /dev/null +++ b/tests/aig/false.aag @@ -0,0 +1,2 @@ +aag 0 0 0 1 0 +0 diff --git a/tests/aig/halfadder.aag b/tests/aig/halfadder.aag new file mode 100644 index 000000000..5bf54d38d --- /dev/null +++ b/tests/aig/halfadder.aag @@ -0,0 +1,14 @@ +aag 7 2 0 2 3 +2 +4 +6 +12 +6 13 15 +12 2 4 +14 3 5 +i0 x +i1 y +o0 s +o1 c +c +half adder diff --git a/tests/aig/inverter.aag b/tests/aig/inverter.aag new file mode 100644 index 000000000..ff7c28542 --- /dev/null +++ b/tests/aig/inverter.aag @@ -0,0 +1,3 @@ +aag 1 1 0 1 0 +2 +3 diff --git a/tests/aig/notcnt1.aag b/tests/aig/notcnt1.aag new file mode 100644 index 000000000..e92815f23 --- /dev/null +++ b/tests/aig/notcnt1.aag @@ -0,0 +1,4 @@ +aag 1 0 1 0 0 1 +2 3 +3 +b0 AIGER_NEVER diff --git a/tests/aig/notcnt1e.aag b/tests/aig/notcnt1e.aag new file mode 100644 index 000000000..141c864f7 --- /dev/null +++ b/tests/aig/notcnt1e.aag @@ -0,0 +1,8 @@ +aag 5 1 1 0 3 1 +2 +4 10 +5 +6 5 3 +8 4 2 +10 9 7 +b0 AIGER_NEVER diff --git a/tests/aig/or.aag b/tests/aig/or.aag new file mode 100644 index 000000000..f780e339f --- /dev/null +++ b/tests/aig/or.aag @@ -0,0 +1,5 @@ +aag 3 2 0 1 1 +2 +4 +7 +6 3 5 diff --git a/tests/aig/run-test.sh b/tests/aig/run-test.sh new file mode 100755 index 000000000..308578f01 --- /dev/null +++ b/tests/aig/run-test.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +OPTIND=1 +seed="" # default to no seed specified +while getopts "S:" opt +do + case "$opt" in + S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space + seed="SEED=$arg" ;; + esac +done +shift "$((OPTIND-1))" + +# check for Icarus Verilog +if ! which iverilog > /dev/null ; then + echo "$0: Error: Icarus Verilog 'iverilog' not found." + exit 1 +fi + +exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger" diff --git a/tests/aig/toggle-re.aag b/tests/aig/toggle-re.aag new file mode 100644 index 000000000..b662bb386 --- /dev/null +++ b/tests/aig/toggle-re.aag @@ -0,0 +1,14 @@ +aag 7 2 1 2 4 +2 +4 +6 8 +6 +7 +8 4 10 +10 13 15 +12 2 6 +14 3 7 +i0 enable +i1 reset +o0 Q +o1 !Q diff --git a/tests/aig/toggle.aag b/tests/aig/toggle.aag new file mode 100644 index 000000000..09651012d --- /dev/null +++ b/tests/aig/toggle.aag @@ -0,0 +1,4 @@ +aag 1 0 1 2 0 +2 3 +2 +3 diff --git a/tests/aig/true.aag b/tests/aig/true.aag new file mode 100644 index 000000000..366893648 --- /dev/null +++ b/tests/aig/true.aag @@ -0,0 +1,2 @@ +aag 0 0 0 1 0 +1 diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index d6216244f..c01ce5611 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -86,8 +86,9 @@ shift $((OPTIND - 1)) for fn do - bn=${fn%.v} - if [ "$bn" == "$fn" ]; then + bn=${fn%.*} + ext=${fn##*.} + if [[ "$ext" != "v" ]] && [[ "$ext" != "aag" ]]; then echo "Invalid argument: $fn" >&2 exit 1 fi @@ -109,10 +110,14 @@ do fn=$(basename $fn) bn=$(basename $bn) - egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.v + if [[ "$ext" == "v" ]]; then + egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext} + else + cp ../$fn ${bn}_ref.${ext} + fi if [ ! -f ../${bn}_tb.v ]; then - "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v + "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.${ext} else cp ../${bn}_tb.v ${bn}_tb.v fi @@ -138,16 +143,16 @@ do fi if [ -n "$scriptfiles" ]; then - test_passes -f "$frontend $include_opts" ${bn}_ref.v $scriptfiles + test_passes -f "$frontend $include_opts" ${bn}_ref.${ext} $scriptfiles elif [ -n "$scriptopt" ]; then - test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.v + test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.${ext} elif [ "$frontend" = "verific" ]; then test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -all; opt; memory;;" elif [ "$frontend" = "verific_gates" ]; then test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -gates -all; opt; memory;;" else - test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.v - test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.v + test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.${ext} + test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.${ext} fi touch ../${bn}.log } -- cgit v1.2.3 From cc0b723484d27424a65336662b7e8c19e21589c2 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 6 Feb 2019 12:19:48 -0800 Subject: WIP --- frontends/aiger/Makefile.inc | 3 + frontends/aiger/aigerparse.cc | 213 ++++++++++++++++++++++++++++++++++++++++++ frontends/aiger/aigerparse.h | 31 ++++++ 3 files changed, 247 insertions(+) create mode 100644 frontends/aiger/Makefile.inc create mode 100644 frontends/aiger/aigerparse.cc create mode 100644 frontends/aiger/aigerparse.h diff --git a/frontends/aiger/Makefile.inc b/frontends/aiger/Makefile.inc new file mode 100644 index 000000000..bc1112452 --- /dev/null +++ b/frontends/aiger/Makefile.inc @@ -0,0 +1,3 @@ + +OBJS += frontends/aiger/aigerparse.o + diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc new file mode 100644 index 000000000..c7a9aecb9 --- /dev/null +++ b/frontends/aiger/aigerparse.cc @@ -0,0 +1,213 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * Eddie Hung + * + * 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. + * + */ + +// [[CITE]] The AIGER And-Inverter Graph (AIG) Format Version 20071012 +// Armin Biere. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1, October 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria. +// http://fmv.jku.at/papers/Biere-FMV-TR-07-1.pdf + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" +#include "aigerparse.h" + +YOSYS_NAMESPACE_BEGIN + +#define log_debug log + +void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) +{ + std::string header; + f >> header; + if (header != "aag") { + log_error("Unsupported AIGER file!\n"); + return; + } + + int M, I, L, O, A; + int B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 + if (!(f >> M >> I >> L >> O >> A)) { + log_error("Invalid AIGER header\n"); + return; + } + for (auto &i : std::array,4>{B, C, J, F}) { + if (f.peek() != ' ') break; + if (!(f >> i)) { + log_error("Invalid AIGER header\n"); + return; + } + } + + std::string line; + std::getline(f, line); // Ignore up to start of next ine, as standard + // says anything that follows could be used for + // optional sections + + log_debug("M=%d I=%d L=%d O=%d A=%d B=%d C=%d J=%d F=%d\n", M, I, L, O, A, B, C, J, F); + + int line_count = 1; + std::stringstream ss; + + auto module = new RTLIL::Module; + module->name = RTLIL::escape_id("aig"); // TODO: Name? + if (design->module(module->name)) + log_error("Duplicate definition of module %s in line %d!\n", log_id(module->name), line_count); + design->add(module); + + auto createWireIfNotExists = [module](int literal) { + const int variable = literal >> 1; + const bool invert = literal & 1; + RTLIL::IdString wire_name(stringf("\\n%d%s", variable, invert ? "_inv" : "")); // FIXME: is "_inv" the right suffix? + RTLIL::Wire *wire = module->wire(wire_name); + if (wire) return wire; + log_debug("Creating %s\n", wire_name.c_str()); + wire = module->addWire(wire_name); + if (!invert) return wire; + RTLIL::IdString wire_inv_name(stringf("\\n%d", variable)); + RTLIL::Wire *wire_inv = module->wire(wire_inv_name); + if (wire_inv) { + if (module->cell(wire_inv_name)) return wire; + } + else { + log_debug("Creating %s\n", wire_inv_name.c_str()); + wire_inv = module->addWire(wire_inv_name); + } + + log_debug("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str()); + RTLIL::Cell *inv = module->addCell(stringf("\\n%d_not", variable), "$_NOT_"); // FIXME: is "_not" the right suffix? + inv->setPort("\\A", wire_inv); + inv->setPort("\\Y", wire); + + return wire; + }; + + int l1, l2, l3; + + // Parse inputs + for (int i = 0; i < I; ++i, ++line_count) { + if (!(f >> l1)) { + log_error("Line %d cannot be interpreted as an input!\n", line_count); + return; + } + log_debug("%d is an input\n", l1); + log_assert(!(l1 & 1)); // TODO: Inputs can't be inverted? + RTLIL::Wire *wire = createWireIfNotExists(l1); + wire->port_input = true; + } + + // Parse latches + for (int i = 0; i < L; ++i, ++line_count) { + if (!(f >> l1 >> l2)) { + log_error("Line %d cannot be interpreted as a latch!\n", line_count); + return; + } + log_debug("%d %d is a latch\n", l1, l2); + log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted? + RTLIL::Wire *q_wire = createWireIfNotExists(l1); + RTLIL::Wire *d_wire = createWireIfNotExists(l2); + RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); + RTLIL::Wire *clk_wire = module->wire(clk_id); + if (!clk_wire) { + log_debug("Creating %s\n", clk_id.c_str()); + clk_wire = module->addWire(clk_id); + clk_wire->port_input = true; + } + + module->addDff(NEW_ID, clk_wire, d_wire, q_wire); + // AIGER latches are assumed to be initialized to zero + q_wire->attributes["\\init"] = RTLIL::Const(0); + } + + // Parse outputs + for (int i = 0; i < O; ++i, ++line_count) { + if (!(f >> l1)) { + log_error("Line %d cannot be interpreted as an output!\n", line_count); + return; + } + + log_debug("%d is an output\n", l1); + RTLIL::Wire *wire = createWireIfNotExists(l1); + wire->port_output = true; + } + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse bad state properties + for (int i = 0; i < B; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse invariant constraints + for (int i = 0; i < C; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse justice properties + for (int i = 0; i < J; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse fairness constraints + for (int i = 0; i < F; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // Parse AND + for (int i = 0; i < A; ++i, ++line_count) { + if (!(f >> l1 >> l2 >> l3)) { + log_error("Line %d cannot be interpreted as an AND!\n", line_count); + return; + } + + log_debug("%d %d %d is an AND\n", l1, l2, l3); + log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted? + RTLIL::Wire *o_wire = createWireIfNotExists(l1); + RTLIL::Wire *i1_wire = createWireIfNotExists(l2); + RTLIL::Wire *i2_wire = createWireIfNotExists(l3); + + RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); + and_cell->setPort("\\A", i1_wire); + and_cell->setPort("\\B", i2_wire); + and_cell->setPort("\\Y", o_wire); + } + + module->fixup_ports(); +} + +struct AigerFrontend : public Frontend { + AigerFrontend() : Frontend("aiger", "read AIGER file") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" read_aiger [options] [filename]\n"); + log("\n"); + log("Load modules from an AIGER file into the current design.\n"); + log("\n"); + } + void execute(std::istream *&f, std::string filename, std::vector args, RTLIL::Design *design) YS_OVERRIDE + { + log_header(design, "Executing AIGER frontend.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + std::string arg = args[argidx]; + break; + } + extra_args(f, filename, args, argidx); + + parse_aiger(design, *f); + } +} AigerFrontend; + +YOSYS_NAMESPACE_END diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h new file mode 100644 index 000000000..6a250aa67 --- /dev/null +++ b/frontends/aiger/aigerparse.h @@ -0,0 +1,31 @@ +/* + * 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. + * + */ + +#ifndef ABC_AIGERPARSE +#define ABC_AIGERPARSE + +#include "kernel/yosys.h" + +YOSYS_NAMESPACE_BEGIN + +extern void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name="clk"); + +YOSYS_NAMESPACE_END + +#endif -- cgit v1.2.3 From fdd55d064b16f9334c86bb15b1c32cfb45294802 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 6 Feb 2019 12:20:36 -0800 Subject: Rename ASCII tests --- tests/aig/and.aag | 5 ----- tests/aig/buffer.aag | 3 --- tests/aig/cnt1.aag | 3 --- tests/aig/cnt1e.aag | 8 -------- tests/aig/empty.aag | 1 - tests/aig/false.aag | 2 -- tests/aig/halfadder.aag | 14 -------------- tests/aig/inverter.aag | 3 --- tests/aig/notcnt1.aag | 4 ---- tests/aig/notcnt1e.aag | 8 -------- tests/aig/or.aag | 5 ----- tests/aig/run-test.sh | 20 -------------------- tests/aig/toggle-re.aag | 14 -------------- tests/aig/toggle.aag | 4 ---- tests/aig/true.aag | 2 -- tests/aiger/and.aag | 5 +++++ tests/aiger/buffer.aag | 3 +++ tests/aiger/cnt1.aag | 3 +++ tests/aiger/cnt1e.aag | 8 ++++++++ tests/aiger/empty.aag | 1 + tests/aiger/false.aag | 2 ++ tests/aiger/halfadder.aag | 14 ++++++++++++++ tests/aiger/inverter.aag | 3 +++ tests/aiger/notcnt1.aag | 4 ++++ tests/aiger/notcnt1e.aag | 8 ++++++++ tests/aiger/or.aag | 5 +++++ tests/aiger/run-test.sh | 20 ++++++++++++++++++++ tests/aiger/toggle-re.aag | 14 ++++++++++++++ tests/aiger/toggle.aag | 4 ++++ tests/aiger/true.aag | 2 ++ 30 files changed, 96 insertions(+), 96 deletions(-) delete mode 100644 tests/aig/and.aag delete mode 100644 tests/aig/buffer.aag delete mode 100644 tests/aig/cnt1.aag delete mode 100644 tests/aig/cnt1e.aag delete mode 100644 tests/aig/empty.aag delete mode 100644 tests/aig/false.aag delete mode 100644 tests/aig/halfadder.aag delete mode 100644 tests/aig/inverter.aag delete mode 100644 tests/aig/notcnt1.aag delete mode 100644 tests/aig/notcnt1e.aag delete mode 100644 tests/aig/or.aag delete mode 100755 tests/aig/run-test.sh delete mode 100644 tests/aig/toggle-re.aag delete mode 100644 tests/aig/toggle.aag delete mode 100644 tests/aig/true.aag create mode 100644 tests/aiger/and.aag create mode 100644 tests/aiger/buffer.aag create mode 100644 tests/aiger/cnt1.aag create mode 100644 tests/aiger/cnt1e.aag create mode 100644 tests/aiger/empty.aag create mode 100644 tests/aiger/false.aag create mode 100644 tests/aiger/halfadder.aag create mode 100644 tests/aiger/inverter.aag create mode 100644 tests/aiger/notcnt1.aag create mode 100644 tests/aiger/notcnt1e.aag create mode 100644 tests/aiger/or.aag create mode 100755 tests/aiger/run-test.sh create mode 100644 tests/aiger/toggle-re.aag create mode 100644 tests/aiger/toggle.aag create mode 100644 tests/aiger/true.aag diff --git a/tests/aig/and.aag b/tests/aig/and.aag deleted file mode 100644 index d1ef2c5a5..000000000 --- a/tests/aig/and.aag +++ /dev/null @@ -1,5 +0,0 @@ -aag 3 2 0 1 1 -2 -4 -6 -6 2 4 diff --git a/tests/aig/buffer.aag b/tests/aig/buffer.aag deleted file mode 100644 index 94a6fb1ed..000000000 --- a/tests/aig/buffer.aag +++ /dev/null @@ -1,3 +0,0 @@ -aag 1 1 0 1 0 -2 -2 diff --git a/tests/aig/cnt1.aag b/tests/aig/cnt1.aag deleted file mode 100644 index ce4f28fcb..000000000 --- a/tests/aig/cnt1.aag +++ /dev/null @@ -1,3 +0,0 @@ -aag 1 0 1 0 0 1 -2 3 -2 diff --git a/tests/aig/cnt1e.aag b/tests/aig/cnt1e.aag deleted file mode 100644 index 6db3f0ffd..000000000 --- a/tests/aig/cnt1e.aag +++ /dev/null @@ -1,8 +0,0 @@ -aag 5 1 1 0 3 1 -2 -4 10 -4 -6 5 3 -8 4 2 -10 9 7 -b0 AIGER_NEVER diff --git a/tests/aig/empty.aag b/tests/aig/empty.aag deleted file mode 100644 index 40c0f00cb..000000000 --- a/tests/aig/empty.aag +++ /dev/null @@ -1 +0,0 @@ -aag 0 0 0 0 0 diff --git a/tests/aig/false.aag b/tests/aig/false.aag deleted file mode 100644 index 421e64a91..000000000 --- a/tests/aig/false.aag +++ /dev/null @@ -1,2 +0,0 @@ -aag 0 0 0 1 0 -0 diff --git a/tests/aig/halfadder.aag b/tests/aig/halfadder.aag deleted file mode 100644 index 5bf54d38d..000000000 --- a/tests/aig/halfadder.aag +++ /dev/null @@ -1,14 +0,0 @@ -aag 7 2 0 2 3 -2 -4 -6 -12 -6 13 15 -12 2 4 -14 3 5 -i0 x -i1 y -o0 s -o1 c -c -half adder diff --git a/tests/aig/inverter.aag b/tests/aig/inverter.aag deleted file mode 100644 index ff7c28542..000000000 --- a/tests/aig/inverter.aag +++ /dev/null @@ -1,3 +0,0 @@ -aag 1 1 0 1 0 -2 -3 diff --git a/tests/aig/notcnt1.aag b/tests/aig/notcnt1.aag deleted file mode 100644 index e92815f23..000000000 --- a/tests/aig/notcnt1.aag +++ /dev/null @@ -1,4 +0,0 @@ -aag 1 0 1 0 0 1 -2 3 -3 -b0 AIGER_NEVER diff --git a/tests/aig/notcnt1e.aag b/tests/aig/notcnt1e.aag deleted file mode 100644 index 141c864f7..000000000 --- a/tests/aig/notcnt1e.aag +++ /dev/null @@ -1,8 +0,0 @@ -aag 5 1 1 0 3 1 -2 -4 10 -5 -6 5 3 -8 4 2 -10 9 7 -b0 AIGER_NEVER diff --git a/tests/aig/or.aag b/tests/aig/or.aag deleted file mode 100644 index f780e339f..000000000 --- a/tests/aig/or.aag +++ /dev/null @@ -1,5 +0,0 @@ -aag 3 2 0 1 1 -2 -4 -7 -6 3 5 diff --git a/tests/aig/run-test.sh b/tests/aig/run-test.sh deleted file mode 100755 index 308578f01..000000000 --- a/tests/aig/run-test.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/bin/bash - -OPTIND=1 -seed="" # default to no seed specified -while getopts "S:" opt -do - case "$opt" in - S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space - seed="SEED=$arg" ;; - esac -done -shift "$((OPTIND-1))" - -# check for Icarus Verilog -if ! which iverilog > /dev/null ; then - echo "$0: Error: Icarus Verilog 'iverilog' not found." - exit 1 -fi - -exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger" diff --git a/tests/aig/toggle-re.aag b/tests/aig/toggle-re.aag deleted file mode 100644 index b662bb386..000000000 --- a/tests/aig/toggle-re.aag +++ /dev/null @@ -1,14 +0,0 @@ -aag 7 2 1 2 4 -2 -4 -6 8 -6 -7 -8 4 10 -10 13 15 -12 2 6 -14 3 7 -i0 enable -i1 reset -o0 Q -o1 !Q diff --git a/tests/aig/toggle.aag b/tests/aig/toggle.aag deleted file mode 100644 index 09651012d..000000000 --- a/tests/aig/toggle.aag +++ /dev/null @@ -1,4 +0,0 @@ -aag 1 0 1 2 0 -2 3 -2 -3 diff --git a/tests/aig/true.aag b/tests/aig/true.aag deleted file mode 100644 index 366893648..000000000 --- a/tests/aig/true.aag +++ /dev/null @@ -1,2 +0,0 @@ -aag 0 0 0 1 0 -1 diff --git a/tests/aiger/and.aag b/tests/aiger/and.aag new file mode 100644 index 000000000..d1ef2c5a5 --- /dev/null +++ b/tests/aiger/and.aag @@ -0,0 +1,5 @@ +aag 3 2 0 1 1 +2 +4 +6 +6 2 4 diff --git a/tests/aiger/buffer.aag b/tests/aiger/buffer.aag new file mode 100644 index 000000000..94a6fb1ed --- /dev/null +++ b/tests/aiger/buffer.aag @@ -0,0 +1,3 @@ +aag 1 1 0 1 0 +2 +2 diff --git a/tests/aiger/cnt1.aag b/tests/aiger/cnt1.aag new file mode 100644 index 000000000..ce4f28fcb --- /dev/null +++ b/tests/aiger/cnt1.aag @@ -0,0 +1,3 @@ +aag 1 0 1 0 0 1 +2 3 +2 diff --git a/tests/aiger/cnt1e.aag b/tests/aiger/cnt1e.aag new file mode 100644 index 000000000..6db3f0ffd --- /dev/null +++ b/tests/aiger/cnt1e.aag @@ -0,0 +1,8 @@ +aag 5 1 1 0 3 1 +2 +4 10 +4 +6 5 3 +8 4 2 +10 9 7 +b0 AIGER_NEVER diff --git a/tests/aiger/empty.aag b/tests/aiger/empty.aag new file mode 100644 index 000000000..40c0f00cb --- /dev/null +++ b/tests/aiger/empty.aag @@ -0,0 +1 @@ +aag 0 0 0 0 0 diff --git a/tests/aiger/false.aag b/tests/aiger/false.aag new file mode 100644 index 000000000..421e64a91 --- /dev/null +++ b/tests/aiger/false.aag @@ -0,0 +1,2 @@ +aag 0 0 0 1 0 +0 diff --git a/tests/aiger/halfadder.aag b/tests/aiger/halfadder.aag new file mode 100644 index 000000000..5bf54d38d --- /dev/null +++ b/tests/aiger/halfadder.aag @@ -0,0 +1,14 @@ +aag 7 2 0 2 3 +2 +4 +6 +12 +6 13 15 +12 2 4 +14 3 5 +i0 x +i1 y +o0 s +o1 c +c +half adder diff --git a/tests/aiger/inverter.aag b/tests/aiger/inverter.aag new file mode 100644 index 000000000..ff7c28542 --- /dev/null +++ b/tests/aiger/inverter.aag @@ -0,0 +1,3 @@ +aag 1 1 0 1 0 +2 +3 diff --git a/tests/aiger/notcnt1.aag b/tests/aiger/notcnt1.aag new file mode 100644 index 000000000..e92815f23 --- /dev/null +++ b/tests/aiger/notcnt1.aag @@ -0,0 +1,4 @@ +aag 1 0 1 0 0 1 +2 3 +3 +b0 AIGER_NEVER diff --git a/tests/aiger/notcnt1e.aag b/tests/aiger/notcnt1e.aag new file mode 100644 index 000000000..141c864f7 --- /dev/null +++ b/tests/aiger/notcnt1e.aag @@ -0,0 +1,8 @@ +aag 5 1 1 0 3 1 +2 +4 10 +5 +6 5 3 +8 4 2 +10 9 7 +b0 AIGER_NEVER diff --git a/tests/aiger/or.aag b/tests/aiger/or.aag new file mode 100644 index 000000000..f780e339f --- /dev/null +++ b/tests/aiger/or.aag @@ -0,0 +1,5 @@ +aag 3 2 0 1 1 +2 +4 +7 +6 3 5 diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh new file mode 100755 index 000000000..308578f01 --- /dev/null +++ b/tests/aiger/run-test.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +OPTIND=1 +seed="" # default to no seed specified +while getopts "S:" opt +do + case "$opt" in + S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space + seed="SEED=$arg" ;; + esac +done +shift "$((OPTIND-1))" + +# check for Icarus Verilog +if ! which iverilog > /dev/null ; then + echo "$0: Error: Icarus Verilog 'iverilog' not found." + exit 1 +fi + +exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger" diff --git a/tests/aiger/toggle-re.aag b/tests/aiger/toggle-re.aag new file mode 100644 index 000000000..b662bb386 --- /dev/null +++ b/tests/aiger/toggle-re.aag @@ -0,0 +1,14 @@ +aag 7 2 1 2 4 +2 +4 +6 8 +6 +7 +8 4 10 +10 13 15 +12 2 6 +14 3 7 +i0 enable +i1 reset +o0 Q +o1 !Q diff --git a/tests/aiger/toggle.aag b/tests/aiger/toggle.aag new file mode 100644 index 000000000..09651012d --- /dev/null +++ b/tests/aiger/toggle.aag @@ -0,0 +1,4 @@ +aag 1 0 1 2 0 +2 3 +2 +3 diff --git a/tests/aiger/true.aag b/tests/aiger/true.aag new file mode 100644 index 000000000..366893648 --- /dev/null +++ b/tests/aiger/true.aag @@ -0,0 +1,2 @@ +aag 0 0 0 1 0 +1 -- cgit v1.2.3 From 3f87cf86ccefe6e66f768fbf19c34db97cf7246d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 6 Feb 2019 14:30:19 -0800 Subject: Revert most of autotest.sh; for non *.v use Yosys to translate --- tests/tools/autotest.sh | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index c01ce5611..3bce003e1 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -113,16 +113,18 @@ do if [[ "$ext" == "v" ]]; then egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext} else - cp ../$fn ${bn}_ref.${ext} + "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "verilog" -o ${bn}_ref.v ../${fn} + frontend="verilog" fi if [ ! -f ../${bn}_tb.v ]; then - "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.${ext} + "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v else cp ../${bn}_tb.v ${bn}_tb.v fi if $genvcd; then sed -i 's,// \$dump,$dump,g' ${bn}_tb.v; fi - compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.v $libs + compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.v $libs \ + "$toolsdir"/../../techlibs/common/simlib.v if $genvcd; then mv testbench.vcd ${bn}_ref.vcd; fi test_count=0 @@ -143,16 +145,16 @@ do fi if [ -n "$scriptfiles" ]; then - test_passes -f "$frontend $include_opts" ${bn}_ref.${ext} $scriptfiles + test_passes -f "$frontend $include_opts" ${bn}_ref.v $scriptfiles elif [ -n "$scriptopt" ]; then - test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.${ext} + test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.v elif [ "$frontend" = "verific" ]; then test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -all; opt; memory;;" elif [ "$frontend" = "verific_gates" ]; then test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -gates -all; opt; memory;;" else - test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.${ext} - test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.${ext} + test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.v + test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.v fi touch ../${bn}.log } -- cgit v1.2.3 From 40db2f2eb61287071f59f3e15bd1cd1bf2838d1d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 6 Feb 2019 14:58:47 -0800 Subject: Refactor --- frontends/aiger/aigerparse.cc | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index c7a9aecb9..7f9feee4a 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -30,15 +30,22 @@ YOSYS_NAMESPACE_BEGIN #define log_debug log +static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name); + void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) { std::string header; f >> header; - if (header != "aag") { + if (header == "aag") + return parse_aiger_ascii(design, f, clk_name); + else { log_error("Unsupported AIGER file!\n"); return; } +} +static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name) +{ int M, I, L, O, A; int B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 if (!(f >> M >> I >> L >> O >> A)) { -- cgit v1.2.3 From 791f93181df091877e0b233fa21ee5fa34b24b27 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 07:31:04 -0800 Subject: Stub for binary AIGER --- frontends/aiger/aigerparse.cc | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 7f9feee4a..a33110ed0 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -31,6 +31,7 @@ YOSYS_NAMESPACE_BEGIN #define log_debug log static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name); +static void parse_aiger_binary(RTLIL::Design *design, std::istream &f, std::string clk_name); void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) { @@ -38,10 +39,10 @@ void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) f >> header; if (header == "aag") return parse_aiger_ascii(design, f, clk_name); - else { + else if (header == "aig") + return parse_aiger_binary(design, f, clk_name); + else log_error("Unsupported AIGER file!\n"); - return; - } } static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name) @@ -191,6 +192,10 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin module->fixup_ports(); } +static void parse_aiger_binary(RTLIL::Design *design, std::istream &f, std::string clk_name) +{ +} + struct AigerFrontend : public Frontend { AigerFrontend() : Frontend("aiger", "read AIGER file") { } void help() YS_OVERRIDE -- cgit v1.2.3 From 6dbeda1807b285ff079c15067e2f649180524c08 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:03:40 -0800 Subject: Add support for symbol tables --- frontends/aiger/aigerparse.cc | 50 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index a33110ed0..7a53bb808 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -107,6 +107,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin int l1, l2, l3; // Parse inputs + std::vector inputs; for (int i = 0; i < I; ++i, ++line_count) { if (!(f >> l1)) { log_error("Line %d cannot be interpreted as an input!\n", line_count); @@ -116,9 +117,11 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_assert(!(l1 & 1)); // TODO: Inputs can't be inverted? RTLIL::Wire *wire = createWireIfNotExists(l1); wire->port_input = true; + inputs.push_back(wire); } // Parse latches + std::vector latches; for (int i = 0; i < L; ++i, ++line_count) { if (!(f >> l1 >> l2)) { log_error("Line %d cannot be interpreted as a latch!\n", line_count); @@ -139,9 +142,11 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin module->addDff(NEW_ID, clk_wire, d_wire, q_wire); // AIGER latches are assumed to be initialized to zero q_wire->attributes["\\init"] = RTLIL::Const(0); + latches.push_back(q_wire); } // Parse outputs + std::vector outputs; for (int i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) { log_error("Line %d cannot be interpreted as an output!\n", line_count); @@ -151,9 +156,10 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_debug("%d is an output\n", l1); RTLIL::Wire *wire = createWireIfNotExists(l1); wire->port_output = true; + outputs.push_back(wire); } std::getline(f, line); // Ignore up to start of next line - + // TODO: Parse bad state properties for (int i = 0; i < B; ++i, ++line_count) std::getline(f, line); // Ignore up to start of next line @@ -188,6 +194,48 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin and_cell->setPort("\\B", i2_wire); and_cell->setPort("\\Y", o_wire); } + std::getline(f, line); // Ignore up to start of next line + + std::string s; + for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) { + if (c == 'i' || c == 'o') { + f.ignore(1); + if (!(f >> l1 >> s)) { + log_error("Line %d cannot be interpreted as a symbol entry!\n", line_count); + return; + } + + if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) { + log_error("Line %d has invalid symbol position!\n", line_count); + return; + } + + RTLIL::Wire* wire; + if (c == 'i') wire = inputs[l1]; + else if (c == 'l') wire = latches[l1]; + else if (c == 'o') wire = outputs[l1]; + else log_abort(); + + module->rename(wire, stringf("\\%s", s.c_str())); + } + else if (c == 'l') { + } + else if (c == 'b' || c == 'j' || c == 'f') { + // TODO + } + else if (c == 'c') { + f.ignore(1); + if (f.peek() == '\n') + break; + // Else constraint (TODO) + break; + } + else { + log_error("Line %d: cannot interpret first character '%c'!\n", line_count, c); + return; + } + std::getline(f, line); // Ignore up to start of next line + } module->fixup_ports(); } -- cgit v1.2.3 From 5a593ff41c44329e9a103d8c9f7a7351b1848043 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:04:48 -0800 Subject: Remove return after log_error --- frontends/aiger/aigerparse.cc | 36 +++++++++--------------------------- 1 file changed, 9 insertions(+), 27 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 7a53bb808..950432578 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -49,16 +49,12 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin { int M, I, L, O, A; int B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 - if (!(f >> M >> I >> L >> O >> A)) { + if (!(f >> M >> I >> L >> O >> A)) log_error("Invalid AIGER header\n"); - return; - } for (auto &i : std::array,4>{B, C, J, F}) { if (f.peek() != ' ') break; - if (!(f >> i)) { + if (!(f >> i)) log_error("Invalid AIGER header\n"); - return; - } } std::string line; @@ -109,10 +105,8 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse inputs std::vector inputs; for (int i = 0; i < I; ++i, ++line_count) { - if (!(f >> l1)) { + if (!(f >> l1)) log_error("Line %d cannot be interpreted as an input!\n", line_count); - return; - } log_debug("%d is an input\n", l1); log_assert(!(l1 & 1)); // TODO: Inputs can't be inverted? RTLIL::Wire *wire = createWireIfNotExists(l1); @@ -123,10 +117,8 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse latches std::vector latches; for (int i = 0; i < L; ++i, ++line_count) { - if (!(f >> l1 >> l2)) { + if (!(f >> l1 >> l2)) log_error("Line %d cannot be interpreted as a latch!\n", line_count); - return; - } log_debug("%d %d is a latch\n", l1, l2); log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted? RTLIL::Wire *q_wire = createWireIfNotExists(l1); @@ -148,10 +140,8 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse outputs std::vector outputs; for (int i = 0; i < O; ++i, ++line_count) { - if (!(f >> l1)) { + if (!(f >> l1)) log_error("Line %d cannot be interpreted as an output!\n", line_count); - return; - } log_debug("%d is an output\n", l1); RTLIL::Wire *wire = createWireIfNotExists(l1); @@ -178,10 +168,8 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse AND for (int i = 0; i < A; ++i, ++line_count) { - if (!(f >> l1 >> l2 >> l3)) { + if (!(f >> l1 >> l2 >> l3)) log_error("Line %d cannot be interpreted as an AND!\n", line_count); - return; - } log_debug("%d %d %d is an AND\n", l1, l2, l3); log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted? @@ -200,15 +188,11 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) { if (c == 'i' || c == 'o') { f.ignore(1); - if (!(f >> l1 >> s)) { + if (!(f >> l1 >> s)) log_error("Line %d cannot be interpreted as a symbol entry!\n", line_count); - return; - } - if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) { + if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) log_error("Line %d has invalid symbol position!\n", line_count); - return; - } RTLIL::Wire* wire; if (c == 'i') wire = inputs[l1]; @@ -230,10 +214,8 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Else constraint (TODO) break; } - else { + else log_error("Line %d: cannot interpret first character '%c'!\n", line_count, c); - return; - } std::getline(f, line); // Ignore up to start of next line } -- cgit v1.2.3 From 02f603ac1a43f3f98048c146b1950c776f73c070 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:05:27 -0800 Subject: Handle latch symbols too --- frontends/aiger/aigerparse.cc | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 950432578..a2b2f611e 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -186,7 +186,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin std::string s; for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) { - if (c == 'i' || c == 'o') { + if (c == 'i' || c == 'l' || c == 'o') { f.ignore(1); if (!(f >> l1 >> s)) log_error("Line %d cannot be interpreted as a symbol entry!\n", line_count); @@ -202,8 +202,6 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin module->rename(wire, stringf("\\%s", s.c_str())); } - else if (c == 'l') { - } else if (c == 'b' || c == 'j' || c == 'f') { // TODO } -- cgit v1.2.3 From fafa972238e91f6d25bfa307a4ead4035477df18 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:08:49 -0800 Subject: Create clk outside of latch loop --- frontends/aiger/aigerparse.cc | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index a2b2f611e..abff6d8d9 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -116,6 +116,15 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse latches std::vector latches; + RTLIL::Wire *clk_wire = nullptr; + if (L > 0) { + RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); + clk_wire = module->wire(clk_id); + log_assert(!clk_wire); + log_debug("Creating %s\n", clk_id.c_str()); + clk_wire = module->addWire(clk_id); + clk_wire->port_input = true; + } for (int i = 0; i < L; ++i, ++line_count) { if (!(f >> l1 >> l2)) log_error("Line %d cannot be interpreted as a latch!\n", line_count); @@ -123,13 +132,6 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted? RTLIL::Wire *q_wire = createWireIfNotExists(l1); RTLIL::Wire *d_wire = createWireIfNotExists(l2); - RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); - RTLIL::Wire *clk_wire = module->wire(clk_id); - if (!clk_wire) { - log_debug("Creating %s\n", clk_id.c_str()); - clk_wire = module->addWire(clk_id); - clk_wire->port_input = true; - } module->addDff(NEW_ID, clk_wire, d_wire, q_wire); // AIGER latches are assumed to be initialized to zero -- cgit v1.2.3 From 652e414392b8e9e8c7dde74e6f2c2369d8d65a20 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:09:30 -0800 Subject: Change literal vars from int to unsigned --- frontends/aiger/aigerparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index abff6d8d9..0414d3db3 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -100,7 +100,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin return wire; }; - int l1, l2, l3; + unsigned l1, l2, l3; // Parse inputs std::vector inputs; -- cgit v1.2.3 From 5e24251a61b8798e597ac49bdc8aff2f378f625d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:37:18 -0800 Subject: Handle reset logic in latches --- frontends/aiger/aigerparse.cc | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 0414d3db3..c3cc6b321 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -134,8 +134,23 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin RTLIL::Wire *d_wire = createWireIfNotExists(l2); module->addDff(NEW_ID, clk_wire, d_wire, q_wire); - // AIGER latches are assumed to be initialized to zero - q_wire->attributes["\\init"] = RTLIL::Const(0); + + if (f.peek() == ' ') { + if (!(f >> l3)) + log_error("Line %d cannot be interpreted as a latch!\n", line_count); + + if (l3 == 0 || l3 == 1) + q_wire->attributes["\\init"] = RTLIL::Const(0); + else if (l3 == l1) { + //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx); + } + else + log_error("Line %d has invalid reset literal for latch!\n", line_count); + } + else { + // AIGER latches are assumed to be initialized to zero + q_wire->attributes["\\init"] = RTLIL::Const(0); + } latches.push_back(q_wire); } -- cgit v1.2.3 From 36c56bf4127edc1ed0f8fbbd62bd70a859263570 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 08:37:44 -0800 Subject: Add comment --- frontends/aiger/aigerparse.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index c3cc6b321..56e4f3b2c 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -135,6 +135,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin module->addDff(NEW_ID, clk_wire, d_wire, q_wire); + // Reset logic is optional in AIGER 1.9 if (f.peek() == ' ') { if (!(f >> l3)) log_error("Line %d cannot be interpreted as a latch!\n", line_count); -- cgit v1.2.3 From 09d758f0a31e3b4290bfcd3d9864733e84c83628 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 10:54:31 -0800 Subject: Refactor to parse_aiger_header() --- frontends/aiger/aigerparse.cc | 58 ++++++++++++++++++++++++------------------- 1 file changed, 32 insertions(+), 26 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 56e4f3b2c..4c15e34d2 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -45,13 +45,11 @@ void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) log_error("Unsupported AIGER file!\n"); } -static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name) +static void parse_aiger_header(std::istream &f, unsigned &M, unsigned &I, unsigned &L, unsigned &O, unsigned &A, unsigned &B, unsigned &C, unsigned &J, unsigned &F) { - int M, I, L, O, A; - int B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 if (!(f >> M >> I >> L >> O >> A)) log_error("Invalid AIGER header\n"); - for (auto &i : std::array,4>{B, C, J, F}) { + for (auto &i : std::array,4>{B, C, J, F}) { if (f.peek() != ' ') break; if (!(f >> i)) log_error("Invalid AIGER header\n"); @@ -62,19 +60,27 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // says anything that follows could be used for // optional sections - log_debug("M=%d I=%d L=%d O=%d A=%d B=%d C=%d J=%d F=%d\n", M, I, L, O, A, B, C, J, F); + log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M, I, L, O, A, B, C, J, F); +} + +static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name) +{ + unsigned M, I, L, O, A; + unsigned B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 + parse_aiger_header(f, M, I, L, O, A, B, C, J, F); - int line_count = 1; + unsigned line_count = 1; + std::string line; std::stringstream ss; auto module = new RTLIL::Module; module->name = RTLIL::escape_id("aig"); // TODO: Name? if (design->module(module->name)) - log_error("Duplicate definition of module %s in line %d!\n", log_id(module->name), line_count); + log_error("Duplicate definition of module %s in line %u!\n", log_id(module->name), line_count); design->add(module); - auto createWireIfNotExists = [module](int literal) { - const int variable = literal >> 1; + auto createWireIfNotExists = [module](unsigned literal) { + const unsigned variable = literal >> 1; const bool invert = literal & 1; RTLIL::IdString wire_name(stringf("\\n%d%s", variable, invert ? "_inv" : "")); // FIXME: is "_inv" the right suffix? RTLIL::Wire *wire = module->wire(wire_name); @@ -104,9 +110,9 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse inputs std::vector inputs; - for (int i = 0; i < I; ++i, ++line_count) { + for (unsigned i = 0; i < I; ++i, ++line_count) { if (!(f >> l1)) - log_error("Line %d cannot be interpreted as an input!\n", line_count); + log_error("Line %u cannot be interpreted as an input!\n", line_count); log_debug("%d is an input\n", l1); log_assert(!(l1 & 1)); // TODO: Inputs can't be inverted? RTLIL::Wire *wire = createWireIfNotExists(l1); @@ -125,9 +131,9 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin clk_wire = module->addWire(clk_id); clk_wire->port_input = true; } - for (int i = 0; i < L; ++i, ++line_count) { + for (unsigned i = 0; i < L; ++i, ++line_count) { if (!(f >> l1 >> l2)) - log_error("Line %d cannot be interpreted as a latch!\n", line_count); + log_error("Line %u cannot be interpreted as a latch!\n", line_count); log_debug("%d %d is a latch\n", l1, l2); log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted? RTLIL::Wire *q_wire = createWireIfNotExists(l1); @@ -138,7 +144,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Reset logic is optional in AIGER 1.9 if (f.peek() == ' ') { if (!(f >> l3)) - log_error("Line %d cannot be interpreted as a latch!\n", line_count); + log_error("Line %u cannot be interpreted as a latch!\n", line_count); if (l3 == 0 || l3 == 1) q_wire->attributes["\\init"] = RTLIL::Const(0); @@ -146,7 +152,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx); } else - log_error("Line %d has invalid reset literal for latch!\n", line_count); + log_error("Line %u has invalid reset literal for latch!\n", line_count); } else { // AIGER latches are assumed to be initialized to zero @@ -157,9 +163,9 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin // Parse outputs std::vector outputs; - for (int i = 0; i < O; ++i, ++line_count) { + for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) - log_error("Line %d cannot be interpreted as an output!\n", line_count); + log_error("Line %u cannot be interpreted as an output!\n", line_count); log_debug("%d is an output\n", l1); RTLIL::Wire *wire = createWireIfNotExists(l1); @@ -169,25 +175,25 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin std::getline(f, line); // Ignore up to start of next line // TODO: Parse bad state properties - for (int i = 0; i < B; ++i, ++line_count) + for (unsigned i = 0; i < B; ++i, ++line_count) std::getline(f, line); // Ignore up to start of next line // TODO: Parse invariant constraints - for (int i = 0; i < C; ++i, ++line_count) + for (unsigned i = 0; i < C; ++i, ++line_count) std::getline(f, line); // Ignore up to start of next line // TODO: Parse justice properties - for (int i = 0; i < J; ++i, ++line_count) + for (unsigned i = 0; i < J; ++i, ++line_count) std::getline(f, line); // Ignore up to start of next line // TODO: Parse fairness constraints - for (int i = 0; i < F; ++i, ++line_count) + for (unsigned i = 0; i < F; ++i, ++line_count) std::getline(f, line); // Ignore up to start of next line // Parse AND - for (int i = 0; i < A; ++i, ++line_count) { + for (unsigned i = 0; i < A; ++i, ++line_count) { if (!(f >> l1 >> l2 >> l3)) - log_error("Line %d cannot be interpreted as an AND!\n", line_count); + log_error("Line %u cannot be interpreted as an AND!\n", line_count); log_debug("%d %d %d is an AND\n", l1, l2, l3); log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted? @@ -207,10 +213,10 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin if (c == 'i' || c == 'l' || c == 'o') { f.ignore(1); if (!(f >> l1 >> s)) - log_error("Line %d cannot be interpreted as a symbol entry!\n", line_count); + log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count); if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) - log_error("Line %d has invalid symbol position!\n", line_count); + log_error("Line %u has invalid symbol position!\n", line_count); RTLIL::Wire* wire; if (c == 'i') wire = inputs[l1]; @@ -231,7 +237,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin break; } else - log_error("Line %d: cannot interpret first character '%c'!\n", line_count, c); + log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c); std::getline(f, line); // Ignore up to start of next line } -- cgit v1.2.3 From 4e6c5e46725bb99e0c919a5f82ce5290da2ce2f9 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 11:41:25 -0800 Subject: Add binary AIGs converted from AAG --- tests/aiger/and.aig | 3 +++ tests/aiger/buffer.aig | 2 ++ tests/aiger/cnt1.aig | 3 +++ tests/aiger/cnt1e.aig | 4 ++++ tests/aiger/empty.aig | 1 + tests/aiger/false.aig | 2 ++ tests/aiger/halfadder.aig | 9 +++++++++ tests/aiger/inverter.aig | 2 ++ tests/aiger/notcnt1.aig | 4 ++++ tests/aiger/notcnt1e.aig | 4 ++++ tests/aiger/or.aig | 3 +++ tests/aiger/toggle-re.aig | 8 ++++++++ tests/aiger/toggle.aig | 4 ++++ tests/aiger/true.aig | 2 ++ 14 files changed, 51 insertions(+) create mode 100644 tests/aiger/and.aig create mode 100644 tests/aiger/buffer.aig create mode 100644 tests/aiger/cnt1.aig create mode 100644 tests/aiger/cnt1e.aig create mode 100644 tests/aiger/empty.aig create mode 100644 tests/aiger/false.aig create mode 100644 tests/aiger/halfadder.aig create mode 100644 tests/aiger/inverter.aig create mode 100644 tests/aiger/notcnt1.aig create mode 100644 tests/aiger/notcnt1e.aig create mode 100644 tests/aiger/or.aig create mode 100644 tests/aiger/toggle-re.aig create mode 100644 tests/aiger/toggle.aig create mode 100644 tests/aiger/true.aig diff --git a/tests/aiger/and.aig b/tests/aiger/and.aig new file mode 100644 index 000000000..da0fa0719 --- /dev/null +++ b/tests/aiger/and.aig @@ -0,0 +1,3 @@ +aig 3 2 0 1 1 +6 + \ No newline at end of file diff --git a/tests/aiger/buffer.aig b/tests/aiger/buffer.aig new file mode 100644 index 000000000..0c715fdeb --- /dev/null +++ b/tests/aiger/buffer.aig @@ -0,0 +1,2 @@ +aig 1 1 0 1 0 +2 diff --git a/tests/aiger/cnt1.aig b/tests/aiger/cnt1.aig new file mode 100644 index 000000000..8d0ba13b1 --- /dev/null +++ b/tests/aiger/cnt1.aig @@ -0,0 +1,3 @@ +aig 1 0 1 0 0 1 +3 +2 diff --git a/tests/aiger/cnt1e.aig b/tests/aiger/cnt1e.aig new file mode 100644 index 000000000..d8d159f11 --- /dev/null +++ b/tests/aiger/cnt1e.aig @@ -0,0 +1,4 @@ +aig 5 1 1 0 3 1 +10 +4 +b0 AIGER_NEVER diff --git a/tests/aiger/empty.aig b/tests/aiger/empty.aig new file mode 100644 index 000000000..a28373cd3 --- /dev/null +++ b/tests/aiger/empty.aig @@ -0,0 +1 @@ +aig 0 0 0 0 0 diff --git a/tests/aiger/false.aig b/tests/aiger/false.aig new file mode 100644 index 000000000..ad7d039fa --- /dev/null +++ b/tests/aiger/false.aig @@ -0,0 +1,2 @@ +aig 0 0 0 1 0 +0 diff --git a/tests/aiger/halfadder.aig b/tests/aiger/halfadder.aig new file mode 100644 index 000000000..83727ee63 --- /dev/null +++ b/tests/aiger/halfadder.aig @@ -0,0 +1,9 @@ +aig 5 2 0 2 3 +10 +6 +i0 x +i1 y +o0 s +o1 c +c +half adder diff --git a/tests/aiger/inverter.aig b/tests/aiger/inverter.aig new file mode 100644 index 000000000..525d82392 --- /dev/null +++ b/tests/aiger/inverter.aig @@ -0,0 +1,2 @@ +aig 1 1 0 1 0 +3 diff --git a/tests/aiger/notcnt1.aig b/tests/aiger/notcnt1.aig new file mode 100644 index 000000000..f8a667f1f --- /dev/null +++ b/tests/aiger/notcnt1.aig @@ -0,0 +1,4 @@ +aig 1 0 1 0 0 1 +3 +3 +b0 AIGER_NEVER diff --git a/tests/aiger/notcnt1e.aig b/tests/aiger/notcnt1e.aig new file mode 100644 index 000000000..7c85a7290 --- /dev/null +++ b/tests/aiger/notcnt1e.aig @@ -0,0 +1,4 @@ +aig 5 1 1 0 3 1 +10 +5 +b0 AIGER_NEVER diff --git a/tests/aiger/or.aig b/tests/aiger/or.aig new file mode 100644 index 000000000..75c9e4480 --- /dev/null +++ b/tests/aiger/or.aig @@ -0,0 +1,3 @@ +aig 3 2 0 1 1 +7 + \ No newline at end of file diff --git a/tests/aiger/toggle-re.aig b/tests/aiger/toggle-re.aig new file mode 100644 index 000000000..9d6730f21 --- /dev/null +++ b/tests/aiger/toggle-re.aig @@ -0,0 +1,8 @@ +aig 7 2 1 2 4 +14 +6 +7 +i0 enable +i1 reset +o0 Q +o1 !Q diff --git a/tests/aiger/toggle.aig b/tests/aiger/toggle.aig new file mode 100644 index 000000000..b69e21aaf --- /dev/null +++ b/tests/aiger/toggle.aig @@ -0,0 +1,4 @@ +aig 1 0 1 2 0 +3 +2 +3 diff --git a/tests/aiger/true.aig b/tests/aiger/true.aig new file mode 100644 index 000000000..10086f389 --- /dev/null +++ b/tests/aiger/true.aig @@ -0,0 +1,2 @@ +aig 0 0 0 1 0 +1 -- cgit v1.2.3 From 2a8cc36578be9a9d1645e435c3a79eb7d1abc7b2 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 11:45:16 -0800 Subject: Parse binary AIG files --- frontends/aiger/aigerparse.cc | 213 ++++++++++++++++++++++++++++++++---------- 1 file changed, 164 insertions(+), 49 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 4c15e34d2..4bc3918be 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -30,19 +30,55 @@ YOSYS_NAMESPACE_BEGIN #define log_debug log -static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name); -static void parse_aiger_binary(RTLIL::Design *design, std::istream &f, std::string clk_name); +static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::string clk_name); +static void parse_aiger_binary(RTLIL::Module *module, std::istream &f, std::string clk_name); void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) { + auto module = new RTLIL::Module; + module->name = RTLIL::escape_id("aig"); // TODO: Name? + if (design->module(module->name)) + log_error("Duplicate definition of module %s!\n", log_id(module->name)); + std::string header; f >> header; if (header == "aag") - return parse_aiger_ascii(design, f, clk_name); + parse_aiger_ascii(module, f, clk_name); else if (header == "aig") - return parse_aiger_binary(design, f, clk_name); + parse_aiger_binary(module, f, clk_name); else log_error("Unsupported AIGER file!\n"); + + module->fixup_ports(); + design->add(module); +} + +static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned literal) +{ + const unsigned variable = literal >> 1; + const bool invert = literal & 1; + RTLIL::IdString wire_name(stringf("\\n%d%s", variable, invert ? "_inv" : "")); // FIXME: is "_inv" the right suffix? + RTLIL::Wire *wire = module->wire(wire_name); + if (wire) return wire; + log_debug("Creating %s\n", wire_name.c_str()); + wire = module->addWire(wire_name); + if (!invert) return wire; + RTLIL::IdString wire_inv_name(stringf("\\n%d", variable)); + RTLIL::Wire *wire_inv = module->wire(wire_inv_name); + if (wire_inv) { + if (module->cell(wire_inv_name)) return wire; + } + else { + log_debug("Creating %s\n", wire_inv_name.c_str()); + wire_inv = module->addWire(wire_inv_name); + } + + log_debug("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str()); + RTLIL::Cell *inv = module->addCell(stringf("\\n%d_not", variable), "$_NOT_"); // FIXME: is "_not" the right suffix? + inv->setPort("\\A", wire_inv); + inv->setPort("\\Y", wire); + + return wire; } static void parse_aiger_header(std::istream &f, unsigned &M, unsigned &I, unsigned &L, unsigned &O, unsigned &A, unsigned &B, unsigned &C, unsigned &J, unsigned &F) @@ -56,14 +92,14 @@ static void parse_aiger_header(std::istream &f, unsigned &M, unsigned &I, unsign } std::string line; - std::getline(f, line); // Ignore up to start of next ine, as standard + std::getline(f, line); // Ignore up to start of next line, as standard // says anything that follows could be used for // optional sections log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M, I, L, O, A, B, C, J, F); } -static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::string clk_name) +static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::string clk_name) { unsigned M, I, L, O, A; unsigned B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 @@ -73,39 +109,6 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin std::string line; std::stringstream ss; - auto module = new RTLIL::Module; - module->name = RTLIL::escape_id("aig"); // TODO: Name? - if (design->module(module->name)) - log_error("Duplicate definition of module %s in line %u!\n", log_id(module->name), line_count); - design->add(module); - - auto createWireIfNotExists = [module](unsigned literal) { - const unsigned variable = literal >> 1; - const bool invert = literal & 1; - RTLIL::IdString wire_name(stringf("\\n%d%s", variable, invert ? "_inv" : "")); // FIXME: is "_inv" the right suffix? - RTLIL::Wire *wire = module->wire(wire_name); - if (wire) return wire; - log_debug("Creating %s\n", wire_name.c_str()); - wire = module->addWire(wire_name); - if (!invert) return wire; - RTLIL::IdString wire_inv_name(stringf("\\n%d", variable)); - RTLIL::Wire *wire_inv = module->wire(wire_inv_name); - if (wire_inv) { - if (module->cell(wire_inv_name)) return wire; - } - else { - log_debug("Creating %s\n", wire_inv_name.c_str()); - wire_inv = module->addWire(wire_inv_name); - } - - log_debug("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str()); - RTLIL::Cell *inv = module->addCell(stringf("\\n%d_not", variable), "$_NOT_"); // FIXME: is "_not" the right suffix? - inv->setPort("\\A", wire_inv); - inv->setPort("\\Y", wire); - - return wire; - }; - unsigned l1, l2, l3; // Parse inputs @@ -115,7 +118,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_error("Line %u cannot be interpreted as an input!\n", line_count); log_debug("%d is an input\n", l1); log_assert(!(l1 & 1)); // TODO: Inputs can't be inverted? - RTLIL::Wire *wire = createWireIfNotExists(l1); + RTLIL::Wire *wire = createWireIfNotExists(module, l1); wire->port_input = true; inputs.push_back(wire); } @@ -136,8 +139,8 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_error("Line %u cannot be interpreted as a latch!\n", line_count); log_debug("%d %d is a latch\n", l1, l2); log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted? - RTLIL::Wire *q_wire = createWireIfNotExists(l1); - RTLIL::Wire *d_wire = createWireIfNotExists(l2); + RTLIL::Wire *q_wire = createWireIfNotExists(module, l1); + RTLIL::Wire *d_wire = createWireIfNotExists(module, l2); module->addDff(NEW_ID, clk_wire, d_wire, q_wire); @@ -147,7 +150,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_error("Line %u cannot be interpreted as a latch!\n", line_count); if (l3 == 0 || l3 == 1) - q_wire->attributes["\\init"] = RTLIL::Const(0); + q_wire->attributes["\\init"] = RTLIL::Const(l3); else if (l3 == l1) { //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx); } @@ -168,7 +171,7 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_error("Line %u cannot be interpreted as an output!\n", line_count); log_debug("%d is an output\n", l1); - RTLIL::Wire *wire = createWireIfNotExists(l1); + RTLIL::Wire *wire = createWireIfNotExists(module, l1); wire->port_output = true; outputs.push_back(wire); } @@ -197,9 +200,9 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_debug("%d %d %d is an AND\n", l1, l2, l3); log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted? - RTLIL::Wire *o_wire = createWireIfNotExists(l1); - RTLIL::Wire *i1_wire = createWireIfNotExists(l2); - RTLIL::Wire *i2_wire = createWireIfNotExists(l3); + RTLIL::Wire *o_wire = createWireIfNotExists(module, l1); + RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2); + RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); and_cell->setPort("\\A", i1_wire); @@ -240,12 +243,124 @@ static void parse_aiger_ascii(RTLIL::Design *design, std::istream &f, std::strin log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c); std::getline(f, line); // Ignore up to start of next line } +} - module->fixup_ports(); +static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) +{ + unsigned x = 0, i = 0; + unsigned char ch; + while ((ch = f.get()) & 0x80) + x |= (ch & 0x7f) << (7 * i++); + return ref - (x | (ch << (7 * i))); } -static void parse_aiger_binary(RTLIL::Design *design, std::istream &f, std::string clk_name) +static void parse_aiger_binary(RTLIL::Module *module, std::istream &f, std::string clk_name) { + unsigned M, I, L, O, A; + unsigned B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 + parse_aiger_header(f, M, I, L, O, A, B, C, J, F); + + unsigned line_count = 1; + unsigned l1, l2, l3; + std::string line; + + // Parse inputs + std::vector inputs; + for (unsigned i = 1; i <= I; ++i) { + RTLIL::Wire *wire = createWireIfNotExists(module, i << 1); + wire->port_input = true; + inputs.push_back(wire); + } + + // Parse latches + std::vector latches; + RTLIL::Wire *clk_wire = nullptr; + if (L > 0) { + RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); + clk_wire = module->wire(clk_id); + log_assert(!clk_wire); + log_debug("Creating %s\n", clk_id.c_str()); + clk_wire = module->addWire(clk_id); + clk_wire->port_input = true; + } + l1 = (I+1) * 2; + for (unsigned i = 0; i < L; ++i, ++line_count, l1 += 2) { + if (!(f >> l2)) + log_error("Line %u cannot be interpreted as a latch!\n", line_count); + log_debug("%d %d is a latch\n", l1, l2); + RTLIL::Wire *q_wire = createWireIfNotExists(module, l1); + RTLIL::Wire *d_wire = createWireIfNotExists(module, l2); + + module->addDff(NEW_ID, clk_wire, d_wire, q_wire); + + // Reset logic is optional in AIGER 1.9 + if (f.peek() == ' ') { + if (!(f >> l3)) + log_error("Line %u cannot be interpreted as a latch!\n", line_count); + + if (l3 == 0 || l3 == 1) + q_wire->attributes["\\init"] = RTLIL::Const(l3); + else if (l3 == l1) { + //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx); + } + else + log_error("Line %u has invalid reset literal for latch!\n", line_count); + } + else { + // AIGER latches are assumed to be initialized to zero + q_wire->attributes["\\init"] = RTLIL::Const(0); + } + latches.push_back(q_wire); + } + + // Parse outputs + std::vector outputs; + for (unsigned i = 0; i < O; ++i, ++line_count) { + if (!(f >> l1)) + log_error("Line %u cannot be interpreted as an output!\n", line_count); + + log_debug("%d is an output\n", l1); + RTLIL::Wire *wire = createWireIfNotExists(module, l1); + wire->port_output = true; + outputs.push_back(wire); + } + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse bad state properties + for (unsigned i = 0; i < B; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse invariant constraints + for (unsigned i = 0; i < C; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse justice properties + for (unsigned i = 0; i < J; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // TODO: Parse fairness constraints + for (unsigned i = 0; i < F; ++i, ++line_count) + std::getline(f, line); // Ignore up to start of next line + + // Parse AND + l1 = (I+L+1) << 1; + for (unsigned i = 0; i < A; ++i, ++line_count, l1 += 2) { + l2 = parse_next_delta_literal(f, l1); + l3 = parse_next_delta_literal(f, l2); + + log_debug("%d %d %d is an AND\n", l1, l2, l3); + log_assert(!(l1 & 1)); // TODO: Output of ANDs can't be inverted? + RTLIL::Wire *o_wire = createWireIfNotExists(module, l1); + RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2); + RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); + + RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); + and_cell->setPort("\\A", i1_wire); + and_cell->setPort("\\B", i2_wire); + and_cell->setPort("\\Y", o_wire); + } + std::getline(f, line); // Ignore up to start of next line + } struct AigerFrontend : public Frontend { -- cgit v1.2.3 From f1befe1b44ada400e979f43e1b35ebe022ff8fe8 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 12:04:26 -0800 Subject: Refactor into AigerReader class --- frontends/aiger/aigerparse.cc | 150 ++++++++++++++++++++---------------------- frontends/aiger/aigerparse.h | 21 +++++- 2 files changed, 92 insertions(+), 79 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 4bc3918be..365bf1b69 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -30,24 +30,84 @@ YOSYS_NAMESPACE_BEGIN #define log_debug log -static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::string clk_name); -static void parse_aiger_binary(RTLIL::Module *module, std::istream &f, std::string clk_name); - -void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name) +AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, std::string clk_name) + : design(design), f(f), clk_name(clk_name) { - auto module = new RTLIL::Module; + module = new RTLIL::Module; module->name = RTLIL::escape_id("aig"); // TODO: Name? if (design->module(module->name)) log_error("Duplicate definition of module %s!\n", log_id(module->name)); +} +void AigerReader::parse_aiger() +{ std::string header; f >> header; + if (header != "aag" && header != "aig") + log_error("Unsupported AIGER file!\n"); + + // Parse rest of header + if (!(f >> M >> I >> L >> O >> A)) + log_error("Invalid AIGER header\n"); + + // Optional values + B = C = J = F = 0; + for (auto &i : std::array,4>{B, C, J, F}) { + if (f.peek() != ' ') break; + if (!(f >> i)) + log_error("Invalid AIGER header\n"); + } + + std::string line; + std::getline(f, line); // Ignore up to start of next line, as standard + // says anything that follows could be used for + // optional sections + + log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M, I, L, O, A, B, C, J, F); + + line_count = 1; + if (header == "aag") - parse_aiger_ascii(module, f, clk_name); + parse_aiger_ascii(); else if (header == "aig") - parse_aiger_binary(module, f, clk_name); + parse_aiger_binary(); else - log_error("Unsupported AIGER file!\n"); + log_abort(); + + // Parse footer (symbol table, comments, etc.) + unsigned l1; + std::string s; + for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) { + if (c == 'i' || c == 'l' || c == 'o') { + f.ignore(1); + if (!(f >> l1 >> s)) + log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count); + + if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) + log_error("Line %u has invalid symbol position!\n", line_count); + + RTLIL::Wire* wire; + if (c == 'i') wire = inputs[l1]; + else if (c == 'l') wire = latches[l1]; + else if (c == 'o') wire = outputs[l1]; + else log_abort(); + + module->rename(wire, stringf("\\%s", s.c_str())); + } + else if (c == 'b' || c == 'j' || c == 'f') { + // TODO + } + else if (c == 'c') { + f.ignore(1); + if (f.peek() == '\n') + break; + // Else constraint (TODO) + break; + } + else + log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c); + std::getline(f, line); // Ignore up to start of next line + } module->fixup_ports(); design->add(module); @@ -81,38 +141,14 @@ static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned litera return wire; } -static void parse_aiger_header(std::istream &f, unsigned &M, unsigned &I, unsigned &L, unsigned &O, unsigned &A, unsigned &B, unsigned &C, unsigned &J, unsigned &F) +void AigerReader::parse_aiger_ascii() { - if (!(f >> M >> I >> L >> O >> A)) - log_error("Invalid AIGER header\n"); - for (auto &i : std::array,4>{B, C, J, F}) { - if (f.peek() != ' ') break; - if (!(f >> i)) - log_error("Invalid AIGER header\n"); - } - - std::string line; - std::getline(f, line); // Ignore up to start of next line, as standard - // says anything that follows could be used for - // optional sections - - log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M, I, L, O, A, B, C, J, F); -} - -static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::string clk_name) -{ - unsigned M, I, L, O, A; - unsigned B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 - parse_aiger_header(f, M, I, L, O, A, B, C, J, F); - - unsigned line_count = 1; std::string line; std::stringstream ss; unsigned l1, l2, l3; // Parse inputs - std::vector inputs; for (unsigned i = 0; i < I; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an input!\n", line_count); @@ -124,7 +160,6 @@ static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::strin } // Parse latches - std::vector latches; RTLIL::Wire *clk_wire = nullptr; if (L > 0) { RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); @@ -165,7 +200,6 @@ static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::strin } // Parse outputs - std::vector outputs; for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an output!\n", line_count); @@ -210,39 +244,6 @@ static void parse_aiger_ascii(RTLIL::Module *module, std::istream &f, std::strin and_cell->setPort("\\Y", o_wire); } std::getline(f, line); // Ignore up to start of next line - - std::string s; - for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) { - if (c == 'i' || c == 'l' || c == 'o') { - f.ignore(1); - if (!(f >> l1 >> s)) - log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count); - - if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size())) - log_error("Line %u has invalid symbol position!\n", line_count); - - RTLIL::Wire* wire; - if (c == 'i') wire = inputs[l1]; - else if (c == 'l') wire = latches[l1]; - else if (c == 'o') wire = outputs[l1]; - else log_abort(); - - module->rename(wire, stringf("\\%s", s.c_str())); - } - else if (c == 'b' || c == 'j' || c == 'f') { - // TODO - } - else if (c == 'c') { - f.ignore(1); - if (f.peek() == '\n') - break; - // Else constraint (TODO) - break; - } - else - log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c); - std::getline(f, line); // Ignore up to start of next line - } } static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) @@ -254,18 +255,12 @@ static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) return ref - (x | (ch << (7 * i))); } -static void parse_aiger_binary(RTLIL::Module *module, std::istream &f, std::string clk_name) +void AigerReader::parse_aiger_binary() { - unsigned M, I, L, O, A; - unsigned B=0, C=0, J=0, F=0; // Optional in AIGER 1.9 - parse_aiger_header(f, M, I, L, O, A, B, C, J, F); - - unsigned line_count = 1; unsigned l1, l2, l3; std::string line; // Parse inputs - std::vector inputs; for (unsigned i = 1; i <= I; ++i) { RTLIL::Wire *wire = createWireIfNotExists(module, i << 1); wire->port_input = true; @@ -273,7 +268,6 @@ static void parse_aiger_binary(RTLIL::Module *module, std::istream &f, std::stri } // Parse latches - std::vector latches; RTLIL::Wire *clk_wire = nullptr; if (L > 0) { RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); @@ -314,7 +308,6 @@ static void parse_aiger_binary(RTLIL::Module *module, std::istream &f, std::stri } // Parse outputs - std::vector outputs; for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an output!\n", line_count); @@ -385,7 +378,8 @@ struct AigerFrontend : public Frontend { } extra_args(f, filename, args, argidx); - parse_aiger(design, *f); + AigerReader reader(design, *f); + reader.parse_aiger(); } } AigerFrontend; diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h index 6a250aa67..3e8ef09fc 100644 --- a/frontends/aiger/aigerparse.h +++ b/frontends/aiger/aigerparse.h @@ -24,7 +24,26 @@ YOSYS_NAMESPACE_BEGIN -extern void parse_aiger(RTLIL::Design *design, std::istream &f, std::string clk_name="clk"); +struct AigerReader +{ + RTLIL::Design *design; + std::istream &f; + std::string clk_name; + RTLIL::Module *module; + + unsigned M, I, L, O, A; + unsigned B, C, J, F; // Optional in AIGER 1.9 + unsigned line_count; + + std::vector inputs; + std::vector latches; + std::vector outputs; + + AigerReader(RTLIL::Design *design, std::istream &f, std::string clk_name="clk"); + void parse_aiger(); + void parse_aiger_ascii(); + void parse_aiger_binary(); +}; YOSYS_NAMESPACE_END -- cgit v1.2.3 From fb8ad440a32da850e32765ec29119cacb3f3c27c Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 12:40:43 -0800 Subject: Allow module name to be determined by argument too --- frontends/aiger/aigerparse.cc | 54 +++++++++++++++++++++++++++++++++---------- frontends/aiger/aigerparse.h | 4 ++-- 2 files changed, 44 insertions(+), 14 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 365bf1b69..6ebb524bd 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -30,11 +30,11 @@ YOSYS_NAMESPACE_BEGIN #define log_debug log -AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, std::string clk_name) +AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name) : design(design), f(f), clk_name(clk_name) { module = new RTLIL::Module; - module->name = RTLIL::escape_id("aig"); // TODO: Name? + module->name = module_name; if (design->module(module->name)) log_error("Duplicate definition of module %s!\n", log_id(module->name)); } @@ -162,11 +162,10 @@ void AigerReader::parse_aiger_ascii() // Parse latches RTLIL::Wire *clk_wire = nullptr; if (L > 0) { - RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); - clk_wire = module->wire(clk_id); + clk_wire = module->wire(clk_name); log_assert(!clk_wire); - log_debug("Creating %s\n", clk_id.c_str()); - clk_wire = module->addWire(clk_id); + log_debug("Creating %s\n", clk_name.c_str()); + clk_wire = module->addWire(clk_name); clk_wire->port_input = true; } for (unsigned i = 0; i < L; ++i, ++line_count) { @@ -270,11 +269,10 @@ void AigerReader::parse_aiger_binary() // Parse latches RTLIL::Wire *clk_wire = nullptr; if (L > 0) { - RTLIL::IdString clk_id = RTLIL::escape_id(clk_name.c_str()); - clk_wire = module->wire(clk_id); + clk_wire = module->wire(clk_name); log_assert(!clk_wire); - log_debug("Creating %s\n", clk_id.c_str()); - clk_wire = module->addWire(clk_id); + log_debug("Creating %s\n", clk_name.c_str()); + clk_wire = module->addWire(clk_name); clk_wire->port_input = true; } l1 = (I+1) * 2; @@ -364,21 +362,53 @@ struct AigerFrontend : public Frontend { log("\n"); log(" read_aiger [options] [filename]\n"); log("\n"); - log("Load modules from an AIGER file into the current design.\n"); + log("Load module from an AIGER file into the current design.\n"); + log("\n"); + log(" -clk_name \n"); + log(" AIGER latches to be transformed into posedge DFFs clocked by wire of"); + log(" this name (default: clk)\n"); + log("\n"); + log(" -module_name \n"); + log(" Name of module to be created (default: )" +#ifdef _WIN32 + "top" // FIXME +#else + "" +#endif + ")\n"); log("\n"); } void execute(std::istream *&f, std::string filename, std::vector args, RTLIL::Design *design) YS_OVERRIDE { log_header(design, "Executing AIGER frontend.\n"); + RTLIL::IdString clk_name = "\\clk"; + RTLIL::IdString module_name; + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; + if (arg == "-clk_name" && argidx+1 < args.size()) { + clk_name = RTLIL::escape_id(args[++argidx]); + continue; + } + if (arg == "-module_name" && argidx+1 < args.size()) { + module_name = RTLIL::escape_id(args[++argidx]); + continue; + } break; } extra_args(f, filename, args, argidx); - AigerReader reader(design, *f); + if (module_name.empty()) { +#ifdef _WIN32 + module_name = "top"; // FIXME: basename equivalent on Win32? +#else + module_name = RTLIL::escape_id(basename(filename.c_str())); +#endif + } + + AigerReader reader(design, *f, module_name, clk_name); reader.parse_aiger(); } } AigerFrontend; diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h index 3e8ef09fc..39a77bd93 100644 --- a/frontends/aiger/aigerparse.h +++ b/frontends/aiger/aigerparse.h @@ -28,7 +28,7 @@ struct AigerReader { RTLIL::Design *design; std::istream &f; - std::string clk_name; + RTLIL::IdString clk_name; RTLIL::Module *module; unsigned M, I, L, O, A; @@ -39,7 +39,7 @@ struct AigerReader std::vector latches; std::vector outputs; - AigerReader(RTLIL::Design *design, std::istream &f, std::string clk_name="clk"); + AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name); void parse_aiger(); void parse_aiger_ascii(); void parse_aiger_binary(); -- cgit v1.2.3 From 391ec75b07cc8c10818884f19329d719847957d3 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 12:41:39 -0800 Subject: Add missing "[options]" to read_blif help --- frontends/blif/blifparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 9116b257f..a6a07863f 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -584,7 +584,7 @@ struct BlifFrontend : public Frontend { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" read_blif [filename]\n"); + log(" read_blif [options] [filename]\n"); log("\n"); log("Load modules from a BLIF file into the current design.\n"); log("\n"); -- cgit v1.2.3 From 587872236ecd1ca2f2a466bccc8d41618feb0dfb Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 12:41:59 -0800 Subject: Support and differentiate between ASCII and binary AIG testing --- tests/aiger/run-test.sh | 6 +++++- tests/tools/autotest.sh | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh index 308578f01..e0a34f023 100755 --- a/tests/aiger/run-test.sh +++ b/tests/aiger/run-test.sh @@ -17,4 +17,8 @@ if ! which iverilog > /dev/null ; then exit 1 fi -exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger" +echo "===== AAG ======" +${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger" + +echo "===== AIG ======" +exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aig EXTRA_FLAGS="-f aiger" diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index 3e1325b33..0ffa062e3 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -90,7 +90,7 @@ for fn do bn=${fn%.*} ext=${fn##*.} - if [[ "$ext" != "v" ]] && [[ "$ext" != "aag" ]]; then + if [[ "$ext" != "v" ]] && [[ "$ext" != "aag" ]] && [[ "$ext" != "aig" ]]; then echo "Invalid argument: $fn" >&2 exit 1 fi -- cgit v1.2.3 From aa66d8f12f89b457a4a23c04de706a36ee8fc114 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 12:49:55 -0800 Subject: -module_name arg to go before -clk_name --- frontends/aiger/aigerparse.cc | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 6ebb524bd..5c982fb59 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -363,13 +363,13 @@ struct AigerFrontend : public Frontend { log(" read_aiger [options] [filename]\n"); log("\n"); log("Load module from an AIGER file into the current design.\n"); + log("\n"); + log(" -module_name \n"); + log(" Name of module to be created (default: )" log("\n"); log(" -clk_name \n"); log(" AIGER latches to be transformed into posedge DFFs clocked by wire of"); log(" this name (default: clk)\n"); - log("\n"); - log(" -module_name \n"); - log(" Name of module to be created (default: )" #ifdef _WIN32 "top" // FIXME #else @@ -388,14 +388,14 @@ struct AigerFrontend : public Frontend { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; - if (arg == "-clk_name" && argidx+1 < args.size()) { - clk_name = RTLIL::escape_id(args[++argidx]); - continue; - } if (arg == "-module_name" && argidx+1 < args.size()) { module_name = RTLIL::escape_id(args[++argidx]); continue; } + if (arg == "-clk_name" && argidx+1 < args.size()) { + clk_name = RTLIL::escape_id(args[++argidx]); + continue; + } break; } extra_args(f, filename, args, argidx); -- cgit v1.2.3 From afc3c4b6139db528b58062f544fb0b098ab212b0 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 13:17:02 -0800 Subject: Fix tabulation --- frontends/aiger/aigerparse.cc | 56 +++++++++++++++++++++---------------------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 5c982fb59..154581179 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -237,10 +237,10 @@ void AigerReader::parse_aiger_ascii() RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2); RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); - RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); - and_cell->setPort("\\A", i1_wire); - and_cell->setPort("\\B", i2_wire); - and_cell->setPort("\\Y", o_wire); + RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); + and_cell->setPort("\\A", i1_wire); + and_cell->setPort("\\B", i2_wire); + and_cell->setPort("\\Y", o_wire); } std::getline(f, line); // Ignore up to start of next line } @@ -345,42 +345,42 @@ void AigerReader::parse_aiger_binary() RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2); RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); - RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); - and_cell->setPort("\\A", i1_wire); - and_cell->setPort("\\B", i2_wire); - and_cell->setPort("\\Y", o_wire); + RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); + and_cell->setPort("\\A", i1_wire); + and_cell->setPort("\\B", i2_wire); + and_cell->setPort("\\Y", o_wire); } std::getline(f, line); // Ignore up to start of next line } struct AigerFrontend : public Frontend { - AigerFrontend() : Frontend("aiger", "read AIGER file") { } - void help() YS_OVERRIDE - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" read_aiger [options] [filename]\n"); - log("\n"); - log("Load module from an AIGER file into the current design.\n"); + AigerFrontend() : Frontend("aiger", "read AIGER file") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" -module_name \n"); - log(" Name of module to be created (default: )" - log("\n"); - log(" -clk_name \n"); - log(" AIGER latches to be transformed into posedge DFFs clocked by wire of"); - log(" this name (default: clk)\n"); + log(" read_aiger [options] [filename]\n"); + log("\n"); + log("Load module from an AIGER file into the current design.\n"); + log("\n"); + log(" -module_name \n"); + log(" Name of module to be created (default: )" #ifdef _WIN32 "top" // FIXME #else "" #endif ")\n"); - log("\n"); - } - void execute(std::istream *&f, std::string filename, std::vector args, RTLIL::Design *design) YS_OVERRIDE - { - log_header(design, "Executing AIGER frontend.\n"); + log("\n"); + log(" -clk_name \n"); + log(" AIGER latches to be transformed into posedge DFFs clocked by wire of"); + log(" this name (default: clk)\n"); + log("\n"); + } + void execute(std::istream *&f, std::string filename, std::vector args, RTLIL::Design *design) YS_OVERRIDE + { + log_header(design, "Executing AIGER frontend.\n"); RTLIL::IdString clk_name = "\\clk"; RTLIL::IdString module_name; @@ -410,7 +410,7 @@ struct AigerFrontend : public Frontend { AigerReader reader(design, *f, module_name, clk_name); reader.parse_aiger(); - } + } } AigerFrontend; YOSYS_NAMESPACE_END -- cgit v1.2.3 From 8886fa5506b227229398e5ac884203e799bce22c Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 8 Feb 2019 13:17:53 -0800 Subject: addDff -> addDffGate as per @daveshah1 --- frontends/aiger/aigerparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 154581179..c45de8531 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -176,7 +176,7 @@ void AigerReader::parse_aiger_ascii() RTLIL::Wire *q_wire = createWireIfNotExists(module, l1); RTLIL::Wire *d_wire = createWireIfNotExists(module, l2); - module->addDff(NEW_ID, clk_wire, d_wire, q_wire); + module->addDffGate(NEW_ID, clk_wire, d_wire, q_wire); // Reset logic is optional in AIGER 1.9 if (f.peek() == ' ') { -- cgit v1.2.3 From bb4164481d8b6eeec6bbc6f5b36f1286ada51eb5 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 11 Feb 2019 11:51:44 -0800 Subject: Do not ignore newline after AND in binary AIG --- frontends/aiger/aigerparse.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index c45de8531..ed91b6990 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -242,7 +242,6 @@ void AigerReader::parse_aiger_ascii() and_cell->setPort("\\B", i2_wire); and_cell->setPort("\\Y", o_wire); } - std::getline(f, line); // Ignore up to start of next line } static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) -- cgit v1.2.3 From 727ba52504c65be1fcda9b03f6c2e1498e10061d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 11 Feb 2019 13:24:21 -0800 Subject: No increment line_count for binary ANDs --- frontends/aiger/aigerparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index ed91b6990..096e269b2 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -227,7 +227,7 @@ void AigerReader::parse_aiger_ascii() std::getline(f, line); // Ignore up to start of next line // Parse AND - for (unsigned i = 0; i < A; ++i, ++line_count) { + for (unsigned i = 0; i < A; ++i) { if (!(f >> l1 >> l2 >> l3)) log_error("Line %u cannot be interpreted as an AND!\n", line_count); -- cgit v1.2.3 From 04c580fde7a0d1d50c2d93bb6661b3f17a7d61a9 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 11 Feb 2019 13:28:00 -0800 Subject: Do not break for constraints --- frontends/aiger/aigerparse.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 096e269b2..1e13e1124 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -102,7 +102,6 @@ void AigerReader::parse_aiger() if (f.peek() == '\n') break; // Else constraint (TODO) - break; } else log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c); -- cgit v1.2.3 From a2ae39381124ccfec348293c7c7926597c26a5b8 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 12 Feb 2019 09:21:15 -0800 Subject: Use module->add{Not,And}Gate() functions --- frontends/aiger/aigerparse.cc | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index c45de8531..888a4afe6 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -134,9 +134,7 @@ static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned litera } log_debug("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str()); - RTLIL::Cell *inv = module->addCell(stringf("\\n%d_not", variable), "$_NOT_"); // FIXME: is "_not" the right suffix? - inv->setPort("\\A", wire_inv); - inv->setPort("\\Y", wire); + module->addNotGate(stringf("\\n%d_not", variable), wire_inv, wire); // FIXME: is "_not" the right suffix? return wire; } @@ -236,11 +234,7 @@ void AigerReader::parse_aiger_ascii() RTLIL::Wire *o_wire = createWireIfNotExists(module, l1); RTLIL::Wire *i1_wire = createWireIfNotExists(module, l2); RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); - - RTLIL::Cell *and_cell = module->addCell(NEW_ID, "$_AND_"); - and_cell->setPort("\\A", i1_wire); - and_cell->setPort("\\B", i2_wire); - and_cell->setPort("\\Y", o_wire); + module->addAndGate(NEW_ID, i1_wire, i2_wire, o_wire); } std::getline(f, line); // Ignore up to start of next line } -- cgit v1.2.3 From c23e3f07517d4818d9ab1b532250353492cf50c2 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 12 Feb 2019 09:24:13 -0800 Subject: Missing headers for Xcode? --- passes/techmap/abc.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index d2d15a4a9..b215b1ea4 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -52,6 +52,8 @@ #include #include #include +#include +#include #ifndef _WIN32 # include -- cgit v1.2.3 From 430a7548bca6046c812f713877253f8c3d81d805 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sun, 17 Feb 2019 11:50:55 -0800 Subject: One more merge conflict --- tests/tools/autotest.sh | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index 2722cba19..b5abc3570 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -134,18 +134,13 @@ do fn=$(basename $fn) bn=$(basename $bn) -<<<<<<< HEAD + rm -f ${bn}_ref.fir if [[ "$ext" == "v" ]]; then egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext} else "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "verilog" -o ${bn}_ref.v ../${fn} frontend="verilog" fi -======= - rm -f ${bn}_ref.fir - - egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.v ->>>>>>> e45f62b0c56717a23099425f078d1e56212aa632 if [ ! -f ../${bn}_tb.v ]; then "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v -- cgit v1.2.3 From 9268a271fb8b22b089927d63f0b36d620e19704c Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sun, 17 Feb 2019 12:07:14 -0800 Subject: read_aiger to ignore line after ands for ascii, not binary --- frontends/aiger/aigerparse.cc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 7df28fe87..a1a0a08a0 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -235,6 +235,7 @@ void AigerReader::parse_aiger_ascii() RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); module->addAndGate(NEW_ID, i1_wire, i2_wire, o_wire); } + std::getline(f, line); // Ignore up to start of next line } static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) @@ -342,8 +343,6 @@ void AigerReader::parse_aiger_binary() and_cell->setPort("\\B", i2_wire); and_cell->setPort("\\Y", o_wire); } - std::getline(f, line); // Ignore up to start of next line - } struct AigerFrontend : public Frontend { -- cgit v1.2.3 From de1dc7947b3d4bfc4e611740a906915a0c2490b0 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sun, 17 Feb 2019 20:59:15 -0800 Subject: Revert "Missing headers for Xcode?" This reverts commit c23e3f07517d4818d9ab1b532250353492cf50c2. --- passes/techmap/abc.cc | 2 -- 1 file changed, 2 deletions(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index b215b1ea4..d2d15a4a9 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -52,8 +52,6 @@ #include #include #include -#include -#include #ifndef _WIN32 # include -- cgit v1.2.3 From 8e1dbfac3af64339f021ed674bdd98e71cd7fb90 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sun, 17 Feb 2019 20:59:53 -0800 Subject: Missing OSX headers? --- frontends/aiger/aigerparse.cc | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index a1a0a08a0..778b8b070 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -22,6 +22,11 @@ // Armin Biere. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1, October 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria. // http://fmv.jku.at/papers/Biere-FMV-TR-07-1.pdf +#ifdef __linux__ +#include +#endif +#include + #include "kernel/yosys.h" #include "kernel/sigtools.h" #include "aigerparse.h" -- cgit v1.2.3 From 843e7fc8a70b7510ae8dfbad2c9f66d2d64d0e64 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 19 Feb 2019 09:02:37 -0800 Subject: Fix for using POSIX basename --- frontends/aiger/aigerparse.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 778b8b070..cf7950c85 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -22,7 +22,7 @@ // Armin Biere. The AIGER And-Inverter Graph (AIG) Format Version 20071012. Technical Report 07/1, October 2011, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria. // http://fmv.jku.at/papers/Biere-FMV-TR-07-1.pdf -#ifdef __linux__ +#ifndef _WIN32 #include #endif #include @@ -400,7 +400,9 @@ struct AigerFrontend : public Frontend { #ifdef _WIN32 module_name = "top"; // FIXME: basename equivalent on Win32? #else - module_name = RTLIL::escape_id(basename(filename.c_str())); + char* bn = strdup(filename.c_str()); + module_name = RTLIL::escape_id(bn); + free(bn); #endif } -- cgit v1.2.3 From d365682a21147b6a06d9548a6f4b99d347931441 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 19 Feb 2019 15:25:47 -0800 Subject: Add aiger tests to make tests --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index d83a71256..4324b2eec 100644 --- a/Makefile +++ b/Makefile @@ -580,6 +580,7 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/sat && bash run-test.sh +cd tests/svinterfaces && bash run-test.sh $(SEEDOPT) +cd tests/opt && bash run-test.sh + +cd tests/aiger && bash run-test.sh @echo "" @echo " Passed \"make test\"." @echo "" -- cgit v1.2.3 From ff15cf9b1f8208d8c6e22beb9aebedc8bdae213f Mon Sep 17 00:00:00 2001 From: "William D. Jones" Date: Tue, 12 Mar 2019 17:55:47 -0400 Subject: Install launcher executable when running yosys-smtbmc on Windows. Signed-off-by: William D. Jones --- .gitignore | 2 + backends/smt2/Makefile.inc | 18 ++- misc/launcher.c | 358 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 377 insertions(+), 1 deletion(-) create mode 100644 misc/launcher.c diff --git a/.gitignore b/.gitignore index 48ce458c7..e24f7975a 100644 --- a/.gitignore +++ b/.gitignore @@ -24,6 +24,8 @@ /yosys-abc.exe /yosys-config /yosys-smtbmc +/yosys-smtbmc.exe +/yosys-smtbmc-script.py /yosys-filterlib /yosys-filterlib.exe /kernel/version_*.cc diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc index dce82f01a..92941d4cf 100644 --- a/backends/smt2/Makefile.inc +++ b/backends/smt2/Makefile.inc @@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o ifneq ($(CONFIG),mxe) ifneq ($(CONFIG),emcc) + +# MSYS targets support yosys-smtbmc, but require a launcher script +ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64)) +TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py +# Needed to find the Python interpreter for yosys-smtbmc scripts. +# Override if necessary, it is only used for msys2 targets. +PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3) + +yosys-smtbmc-script.py: backends/smt2/smtbmc.py + $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \ + -e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@ + +yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py + $(P) gcc -DGUI=0 -O -s -o $@ $< +# Other targets +else TARGETS += yosys-smtbmc yosys-smtbmc: backends/smt2/smtbmc.py $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new $(Q) chmod +x $@.new $(Q) mv $@.new $@ +endif $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py)) endif endif - diff --git a/misc/launcher.c b/misc/launcher.c new file mode 100644 index 000000000..157d68cf3 --- /dev/null +++ b/misc/launcher.c @@ -0,0 +1,358 @@ +/* This file comes from the PyPA Setuptools repository, commit 16e452a: +https://github.com/pypa/setuptools +Modifications include this comment and inline inclusion of the LICENSE text. */ + +/* Copyright (C) 2016 Jason R Coombs + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies +of the Software, and to permit persons to whom the Software is furnished to do +so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. */ + +/* Setuptools Script Launcher for Windows + + This is a stub executable for Windows that functions somewhat like + Effbot's "exemaker", in that it runs a script with the same name but + a .py extension, using information from a #! line. It differs in that + it spawns the actual Python executable, rather than attempting to + hook into the Python DLL. This means that the script will run with + sys.executable set to the Python executable, where exemaker ends up with + sys.executable pointing to itself. (Which means it won't work if you try + to run another Python process using sys.executable.) + + To build/rebuild with mingw32, do this in the setuptools project directory: + + gcc -DGUI=0 -mno-cygwin -O -s -o setuptools/cli.exe launcher.c + gcc -DGUI=1 -mwindows -mno-cygwin -O -s -o setuptools/gui.exe launcher.c + + To build for Windows RT, install both Visual Studio Express for Windows 8 + and for Windows Desktop (both freeware), create "win32" application using + "Windows Desktop" version, create new "ARM" target via + "Configuration Manager" menu and modify ".vcxproj" file by adding + "true" tag + as child of "PropertyGroup" tags that has "Debug|ARM" and "Release|ARM" + properties. + + It links to msvcrt.dll, but this shouldn't be a problem since it doesn't + actually run Python in the same process. Note that using 'exec' instead + of 'spawn' doesn't work, because on Windows this leads to the Python + executable running in the *background*, attached to the same console + window, meaning you get a command prompt back *before* Python even finishes + starting. So, we have to use spawnv() and wait for Python to exit before + continuing. :( +*/ + +#include +#include +#include +#include +#include +#include + +int child_pid=0; + +int fail(char *format, char *data) { + /* Print error message to stderr and return 2 */ + fprintf(stderr, format, data); + return 2; +} + +char *quoted(char *data) { + int i, ln = strlen(data), nb; + + /* We allocate twice as much space as needed to deal with worse-case + of having to escape everything. */ + char *result = calloc(ln*2+3, sizeof(char)); + char *presult = result; + + *presult++ = '"'; + for (nb=0, i=0; i < ln; i++) + { + if (data[i] == '\\') + nb += 1; + else if (data[i] == '"') + { + for (; nb > 0; nb--) + *presult++ = '\\'; + *presult++ = '\\'; + } + else + nb = 0; + *presult++ = data[i]; + } + + for (; nb > 0; nb--) /* Deal w trailing slashes */ + *presult++ = '\\'; + + *presult++ = '"'; + *presult++ = 0; + return result; +} + + + + + + + + + + +char *loadable_exe(char *exename) { + /* HINSTANCE hPython; DLL handle for python executable */ + char *result; + + /* hPython = LoadLibraryEx(exename, NULL, LOAD_WITH_ALTERED_SEARCH_PATH); + if (!hPython) return NULL; */ + + /* Return the absolute filename for spawnv */ + result = calloc(MAX_PATH, sizeof(char)); + strncpy(result, exename, MAX_PATH); + /*if (result) GetModuleFileNameA(hPython, result, MAX_PATH); + + FreeLibrary(hPython); */ + return result; +} + + +char *find_exe(char *exename, char *script) { + char drive[_MAX_DRIVE], dir[_MAX_DIR], fname[_MAX_FNAME], ext[_MAX_EXT]; + char path[_MAX_PATH], c, *result; + + /* convert slashes to backslashes for uniform search below */ + result = exename; + while (c = *result++) if (c=='/') result[-1] = '\\'; + + _splitpath(exename, drive, dir, fname, ext); + if (drive[0] || dir[0]=='\\') { + return loadable_exe(exename); /* absolute path, use directly */ + } + /* Use the script's parent directory, which should be the Python home + (This should only be used for bdist_wininst-installed scripts, because + easy_install-ed scripts use the absolute path to python[w].exe + */ + _splitpath(script, drive, dir, fname, ext); + result = dir + strlen(dir) -1; + if (*result == '\\') result--; + while (*result != '\\' && result>=dir) *result-- = 0; + _makepath(path, drive, dir, exename, NULL); + return loadable_exe(path); +} + + +char **parse_argv(char *cmdline, int *argc) +{ + /* Parse a command line in-place using MS C rules */ + + char **result = calloc(strlen(cmdline), sizeof(char *)); + char *output = cmdline; + char c; + int nb = 0; + int iq = 0; + *argc = 0; + + result[0] = output; + while (isspace(*cmdline)) cmdline++; /* skip leading spaces */ + + do { + c = *cmdline++; + if (!c || (isspace(c) && !iq)) { + while (nb) {*output++ = '\\'; nb--; } + *output++ = 0; + result[++*argc] = output; + if (!c) return result; + while (isspace(*cmdline)) cmdline++; /* skip leading spaces */ + if (!*cmdline) return result; /* avoid empty arg if trailing ws */ + continue; + } + if (c == '\\') + ++nb; /* count \'s */ + else { + if (c == '"') { + if (!(nb & 1)) { iq = !iq; c = 0; } /* skip " unless odd # of \ */ + nb = nb >> 1; /* cut \'s in half */ + } + while (nb) {*output++ = '\\'; nb--; } + if (c) *output++ = c; + } + } while (1); +} + +void pass_control_to_child(DWORD control_type) { + /* + * distribute-issue207 + * passes the control event to child process (Python) + */ + if (!child_pid) { + return; + } + GenerateConsoleCtrlEvent(child_pid,0); +} + +BOOL control_handler(DWORD control_type) { + /* + * distribute-issue207 + * control event handler callback function + */ + switch (control_type) { + case CTRL_C_EVENT: + pass_control_to_child(0); + break; + } + return TRUE; +} + +int create_and_wait_for_subprocess(char* command) { + /* + * distribute-issue207 + * launches child process (Python) + */ + DWORD return_value = 0; + LPSTR commandline = command; + STARTUPINFOA s_info; + PROCESS_INFORMATION p_info; + ZeroMemory(&p_info, sizeof(p_info)); + ZeroMemory(&s_info, sizeof(s_info)); + s_info.cb = sizeof(STARTUPINFO); + // set-up control handler callback funciotn + SetConsoleCtrlHandler((PHANDLER_ROUTINE) control_handler, TRUE); + if (!CreateProcessA(NULL, commandline, NULL, NULL, TRUE, 0, NULL, NULL, &s_info, &p_info)) { + fprintf(stderr, "failed to create process.\n"); + return 0; + } + child_pid = p_info.dwProcessId; + // wait for Python to exit + WaitForSingleObject(p_info.hProcess, INFINITE); + if (!GetExitCodeProcess(p_info.hProcess, &return_value)) { + fprintf(stderr, "failed to get exit code from process.\n"); + return 0; + } + return return_value; +} + +char* join_executable_and_args(char *executable, char **args, int argc) +{ + /* + * distribute-issue207 + * CreateProcess needs a long string of the executable and command-line arguments, + * so we need to convert it from the args that was built + */ + int len,counter; + char* cmdline; + + len=strlen(executable)+2; + for (counter=1; counterscript && *end != '.') + *end-- = '\0'; + *end-- = '\0'; + strcat(script, (GUI ? "-script.pyw" : "-script.py")); + + /* figure out the target python executable */ + + scriptf = open(script, O_RDONLY); + if (scriptf == -1) { + return fail("Cannot open %s\n", script); + } + end = python + read(scriptf, python, sizeof(python)); + close(scriptf); + + ptr = python-1; + while(++ptr < end && *ptr && *ptr!='\n' && *ptr!='\r') {;} + + *ptr-- = '\0'; + + if (strncmp(python, "#!", 2)) { + /* default to python.exe if no #! header */ + strcpy(python, "#!python.exe"); + } + + parsedargs = parse_argv(python+2, &parsedargc); + + /* Using spawnv() can fail strangely if you e.g. find the Cygwin + Python, so we'll make sure Windows can find and load it */ + + ptr = find_exe(parsedargs[0], script); + if (!ptr) { + return fail("Cannot find Python executable %s\n", parsedargs[0]); + } + + /* printf("Python executable: %s\n", ptr); */ + + /* Argument array needs to be + parsedargc + argc, plus 1 for null sentinel */ + + newargs = (char **)calloc(parsedargc + argc + 1, sizeof(char *)); + newargsp = newargs; + + *newargsp++ = quoted(ptr); + for (i = 1; i Date: Thu, 14 Mar 2019 17:50:20 +0100 Subject: Fix a syntax bug in ilang backend related to process case statements Signed-off-by: Clifford Wolf --- backends/ilang/ilang_backend.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc index 4c58ea087..dc39e5e08 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/ilang/ilang_backend.cc @@ -204,7 +204,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const f << stringf("%s case ", indent.c_str()); for (size_t i = 0; i < (*it)->compare.size(); i++) { if (i > 0) - f << stringf(", "); + f << stringf(" , "); dump_sigspec(f, (*it)->compare[i]); } f << stringf("\n"); -- cgit v1.2.3 From 17caaa3fa898e39d1dbcfd8b92750a9d713a24af Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 17:51:21 +0100 Subject: Improve handling of "full_case" attributes Signed-off-by: Clifford Wolf --- frontends/ast/genrtlil.cc | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index d7da6fb40..b3a2a84be 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -525,7 +525,16 @@ struct AST_INTERNAL::ProcessGenerator } if (last_generated_case != NULL && ast->get_bool_attribute("\\full_case") && default_case == NULL) { + #if 0 + // this is a valid transformation, but as optimization it is premature. + // better: add a default case that assigns 'x' to everything, and let later + // optimizations take care of the rest last_generated_case->compare.clear(); + #else + default_case = new RTLIL::CaseRule; + addChunkActions(default_case->actions, this_case_eq_ltemp, SigSpec(State::Sx, GetSize(this_case_eq_rvalue))); + sw->cases.push_back(default_case); + #endif } else { if (default_case == NULL) { default_case = new RTLIL::CaseRule; -- cgit v1.2.3 From f806b95ed6a2f2c1a0e5c8884676fd384e510143 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 20:35:15 +0100 Subject: Improve handling of and-with-1 and or-with-0 in opt_expr, fixes #327 Signed-off-by: Clifford Wolf --- passes/opt/opt_expr.cc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc index 26a3ca7bc..a05db2a4f 100644 --- a/passes/opt/opt_expr.cc +++ b/passes/opt/opt_expr.cc @@ -155,6 +155,13 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ new_b.append_bit(it.first.second); } + if (cell->type.in("$and", "$or") && i == GRP_CONST_A) { + log(" Direct Connection: %s (%s with %s)\n", log_signal(new_b), log_id(cell->type), log_signal(new_a)); + module->connect(new_y, new_b); + module->connect(new_conn); + continue; + } + RTLIL::Cell *c = module->addCell(NEW_ID, cell->type); c->setPort("\\A", new_a); -- cgit v1.2.3 From ea8ee2414053101bae26cfc2a537d42daf57f5e0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 12 Mar 2019 17:01:59 +0100 Subject: Add basic "mutate -list N" framework Signed-off-by: Clifford Wolf --- passes/sat/Makefile.inc | 1 + passes/sat/mutate.cc | 229 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 230 insertions(+) create mode 100644 passes/sat/mutate.cc diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index 6cb1ea644..e91df1eb0 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -9,4 +9,5 @@ OBJS += passes/sat/assertpmux.o OBJS += passes/sat/clk2fflogic.o OBJS += passes/sat/async2sync.o OBJS += passes/sat/supercover.o +OBJS += passes/sat/mutate.o diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc new file mode 100644 index 000000000..5fd89b7d0 --- /dev/null +++ b/passes/sat/mutate.cc @@ -0,0 +1,229 @@ +/* + * 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/yosys.h" +#include "kernel/sigtools.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct mutate_t { + std::string mode, src; + IdString modname, cellname, celltype, cellport; + SigBit outsigbit; + int portbit = -1; +}; + +struct mutate_opts_t { + std::string mode; + IdString module, cell, port; + int bit = -1; +}; + +void database_add(std::vector &database, const mutate_opts_t &opts, const mutate_t &entry) +{ + if (!opts.module.empty() && opts.module != entry.modname) + return; + + if (!opts.cell.empty() && opts.cell != entry.cellname) + return; + + if (!opts.port.empty() && opts.port != entry.cellport) + return; + + if (opts.bit >= 0 && opts.bit != entry.portbit) + return; + + database.push_back(entry); +} + +void database_reduce(std::vector &database, const mutate_opts_t &opts, int N) +{ +} + +struct MutatePass : public Pass { + MutatePass() : Pass("mutate", "generate or apply design mutations") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" mutate -list N [options] [selection]\n"); + log("\n"); + log("Create a list of N mutations using an even sampling.\n"); + log("\n"); + log(" -o filename\n"); + log(" Write list to this file instead of console output\n"); + log("\n"); + log("\n"); + log(" mutate -mode MODE [options]\n"); + log("\n"); + log("Apply the given mutation.\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE + { + mutate_opts_t opts; + string filename; + int N = -1; + + log_header(design, "Executing MUTATE pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-list" && argidx+1 < args.size()) { + N = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-o" && argidx+1 < args.size()) { + filename = args[++argidx]; + continue; + } + if (args[argidx] == "-mode" && argidx+1 < args.size()) { + opts.mode = args[++argidx]; + continue; + } + if (args[argidx] == "-module" && argidx+1 < args.size()) { + opts.module = RTLIL::escape_id(args[++argidx]); + continue; + } + if (args[argidx] == "-cell" && argidx+1 < args.size()) { + opts.cell = RTLIL::escape_id(args[++argidx]); + continue; + } + if (args[argidx] == "-port" && argidx+1 < args.size()) { + opts.port = RTLIL::escape_id(args[++argidx]); + continue; + } + if (args[argidx] == "-bit" && argidx+1 < args.size()) { + opts.bit = atoi(args[++argidx].c_str()); + continue; + } + break; + } + extra_args(args, argidx, design); + + if (N >= 0) + { + std::vector database; + + for (auto module : design->selected_modules()) + { + if (!opts.module.empty() && module->name != opts.module) + continue; + + SigMap sigmap(module); + + for (auto wire : module->selected_wires()) + { + for (SigBit bit : SigSpec(wire)) + { + SigBit sigbit = sigmap(bit); + + if (bit.wire == nullptr || sigbit.wire == nullptr) + continue; + + if (!bit.wire->port_id != !sigbit.wire->port_id) { + if (bit.wire->port_id) + sigmap.add(bit); + continue; + } + + if (!bit.wire->name[0] != !sigbit.wire->name[0]) { + if (bit.wire->name[0] == '\\') + sigmap.add(bit); + continue; + } + } + } + + for (auto cell : module->selected_cells()) + { + if (!opts.cell.empty() && cell->name != opts.cell) + continue; + + for (auto &conn : cell->connections()) + { + for (int i = 0; i < GetSize(conn.second); i++) { + mutate_t entry; + entry.mode = "inv"; + entry.src = cell->get_src_attribute(); + entry.modname = module->name; + entry.cellname = cell->name; + entry.celltype = cell->type; + entry.cellport = conn.first; + entry.portbit = i; + + if (cell->output(conn.first)) { + SigBit bit = sigmap(conn.second[i]); + if (bit.wire && bit.wire->name[0] == '\\') + entry.outsigbit = bit; + } + + database_add(database, opts, entry); + } + } + } + } + + log("Raw database size: %d\n", GetSize(database)); + if (N != 0) { + database_reduce(database, opts, N); + log("Reduced database size: %d\n", GetSize(database)); + } + + std::ofstream fout; + + if (!filename.empty()) { + fout.open(filename, std::ios::out | std::ios::trunc); + if (!fout.is_open()) + log_error("Could not open file \"%s\" with write access.\n", filename.c_str()); + } + + for (auto &entry : database) { + string str = stringf("mutate -mode %s", entry.mode.c_str()); + if (!entry.modname.empty()) + str += stringf(" -module %s", log_id(entry.modname)); + if (!entry.cellname.empty()) + str += stringf(" -cell %s", log_id(entry.cellname)); + if (!entry.cellport.empty()) + str += stringf(" -port %s", log_id(entry.cellport)); + if (entry.portbit >= 0) + str += stringf(" -bit %d", entry.portbit); + if (entry.outsigbit.wire || !entry.src.empty()) { + str += " #"; + if (!entry.src.empty()) + str += stringf(" %s", entry.src.c_str()); + if (entry.outsigbit.wire) + str += stringf(" %s", log_signal(entry.outsigbit)); + } + if (filename.empty()) + log("%s\n", str.c_str()); + else + fout << str << std::endl; + } + + return; + } + + log_cmd_error("Invalid mode: %s\n", opts.mode.c_str()); + } +} MutatePass; + +PRIVATE_NAMESPACE_END -- cgit v1.2.3 From 8e6b69d7bba21dd3fa01064ee698dcd409b5dcc8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 13 Mar 2019 16:09:47 +0100 Subject: Add "mutate -mode inv", various other mutate improvements Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 312 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 213 insertions(+), 99 deletions(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 5fd89b7d0..04aebd897 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -34,10 +34,16 @@ struct mutate_opts_t { std::string mode; IdString module, cell, port; int bit = -1; + + IdString ctrl_name; + int ctrl_width, ctrl_value; }; void database_add(std::vector &database, const mutate_opts_t &opts, const mutate_t &entry) { + if (!opts.mode.empty() && opts.mode != entry.mode) + return; + if (!opts.module.empty() && opts.module != entry.modname) return; @@ -57,6 +63,183 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, { } +void mutate_list(Design *design, const mutate_opts_t &opts, const string &filename, int N) +{ + std::vector database; + + for (auto module : design->selected_modules()) + { + if (!opts.module.empty() && module->name != opts.module) + continue; + + SigMap sigmap(module); + + for (auto wire : module->selected_wires()) + { + for (SigBit bit : SigSpec(wire)) + { + SigBit sigbit = sigmap(bit); + + if (bit.wire == nullptr || sigbit.wire == nullptr) + continue; + + if (!bit.wire->port_id != !sigbit.wire->port_id) { + if (bit.wire->port_id) + sigmap.add(bit); + continue; + } + + if (!bit.wire->name[0] != !sigbit.wire->name[0]) { + if (bit.wire->name[0] == '\\') + sigmap.add(bit); + continue; + } + } + } + + for (auto cell : module->selected_cells()) + { + if (!opts.cell.empty() && cell->name != opts.cell) + continue; + + for (auto &conn : cell->connections()) + { + for (int i = 0; i < GetSize(conn.second); i++) { + mutate_t entry; + entry.mode = "inv"; + entry.src = cell->get_src_attribute(); + entry.modname = module->name; + entry.cellname = cell->name; + entry.celltype = cell->type; + entry.cellport = conn.first; + entry.portbit = i; + + if (cell->output(conn.first)) { + SigBit bit = sigmap(conn.second[i]); + if (bit.wire && bit.wire->name[0] == '\\') + entry.outsigbit = bit; + } + + database_add(database, opts, entry); + } + } + } + } + + log("Raw database size: %d\n", GetSize(database)); + if (N != 0) { + database_reduce(database, opts, N); + log("Reduced database size: %d\n", GetSize(database)); + } + + std::ofstream fout; + + if (!filename.empty()) { + fout.open(filename, std::ios::out | std::ios::trunc); + if (!fout.is_open()) + log_error("Could not open file \"%s\" with write access.\n", filename.c_str()); + } + + for (auto &entry : database) { + string str = stringf("mutate -mode %s", entry.mode.c_str()); + if (!entry.modname.empty()) + str += stringf(" -module %s", log_id(entry.modname)); + if (!entry.cellname.empty()) + str += stringf(" -cell %s", log_id(entry.cellname)); + if (!entry.cellport.empty()) + str += stringf(" -port %s", log_id(entry.cellport)); + if (entry.portbit >= 0) + str += stringf(" -bit %d", entry.portbit); + if (entry.outsigbit.wire || !entry.src.empty()) { + str += " #"; + if (!entry.src.empty()) + str += stringf(" %s", entry.src.c_str()); + if (entry.outsigbit.wire) + str += stringf(" %s", log_signal(entry.outsigbit)); + } + if (filename.empty()) + log("%s\n", str.c_str()); + else + fout << str << std::endl; + } +} + +SigSpec mutate_ctrl_sig(Module *module, IdString name, int width) +{ + Wire *ctrl_wire = module->wire(name); + + if (ctrl_wire == nullptr) + { + log("Adding ctrl port %s to module %s.\n", log_id(name), log_id(module)); + + ctrl_wire = module->addWire(name, width); + ctrl_wire->port_input = true; + module->fixup_ports(); + + for (auto mod : module->design->modules()) + for (auto cell : mod->cells()) + { + if (cell->type != module->name) + continue; + + SigSpec ctrl = mutate_ctrl_sig(mod, name, width); + + log("Connecting ctrl port to cell %s in module %s.\n", log_id(cell), log_id(mod)); + cell->setPort(name, ctrl); + } + } + + log_assert(GetSize(ctrl_wire) == width); + return ctrl_wire; +} + +SigBit mutate_ctrl(Module *module, const mutate_opts_t &opts) +{ + if (opts.ctrl_name.empty()) + return State::S1; + + SigSpec sig = mutate_ctrl_sig(module, opts.ctrl_name, opts.ctrl_width); + return module->Eq(NEW_ID, sig, Const(opts.ctrl_value, GetSize(sig))); +} + +SigSpec mutate_ctrl_mux(Module *module, const mutate_opts_t &opts, SigSpec unchanged_sig, SigSpec changed_sig) +{ + SigBit ctrl_bit = mutate_ctrl(module, opts); + if (ctrl_bit == State::S0) + return unchanged_sig; + if (ctrl_bit == State::S1) + return changed_sig; + return module->Mux(NEW_ID, unchanged_sig, changed_sig, ctrl_bit); +} + +void mutate_inv(Design *design, const mutate_opts_t &opts) +{ + Module *module = design->module(opts.module); + Cell *cell = module->cell(opts.cell); + + SigBit bit = cell->getPort(opts.port)[opts.bit]; + SigBit inbit, outbit; + + if (cell->input(opts.port)) + { + log("Add input inverter at %s.%s.%s[%d].\n", log_id(module), log_id(cell), log_id(opts.port), opts.bit); + SigBit outbit = module->Not(NEW_ID, bit); + bit = mutate_ctrl_mux(module, opts, bit, outbit); + } + else + { + log("Add output inverter at %s.%s.%s[%d].\n", log_id(module), log_id(cell), log_id(opts.port), opts.bit); + SigBit inbit = module->addWire(NEW_ID); + SigBit outbit = module->Not(NEW_ID, inbit); + module->connect(bit, mutate_ctrl_mux(module, opts, inbit, outbit)); + bit = inbit; + } + + SigSpec s = cell->getPort(opts.port); + s[opts.bit] = bit; + cell->setPort(opts.port, s); +} + struct MutatePass : public Pass { MutatePass() : Pass("mutate", "generate or apply design mutations") { } void help() YS_OVERRIDE @@ -70,11 +253,29 @@ struct MutatePass : public Pass { log(" -o filename\n"); log(" Write list to this file instead of console output\n"); log("\n"); + log(" -mode name\n"); + log(" -module name\n"); + log(" -cell name\n"); + log(" -port name\n"); + log(" -bit int\n"); + log(" Filter list of mutation candidates to those matching\n"); + log(" the given parameters.\n"); + log("\n"); log("\n"); log(" mutate -mode MODE [options]\n"); log("\n"); log("Apply the given mutation.\n"); log("\n"); + log(" -ctrl name width value\n"); + log(" Add a control signal with the given name and width. The mutation is\n"); + log(" activated if the control signal equals the given value.\n"); + log("\n"); + log(" -module name\n"); + log(" -cell name\n"); + log(" -port name\n"); + log(" -bit int\n"); + log(" Mutation parameters, as generated by 'mutate -list N'.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { @@ -99,6 +300,12 @@ struct MutatePass : public Pass { opts.mode = args[++argidx]; continue; } + if (args[argidx] == "-ctrl" && argidx+3 < args.size()) { + opts.ctrl_name = RTLIL::escape_id(args[++argidx]); + opts.ctrl_width = atoi(args[++argidx].c_str()); + opts.ctrl_value = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-module" && argidx+1 < args.size()) { opts.module = RTLIL::escape_id(args[++argidx]); continue; @@ -119,106 +326,13 @@ struct MutatePass : public Pass { } extra_args(args, argidx, design); - if (N >= 0) - { - std::vector database; - - for (auto module : design->selected_modules()) - { - if (!opts.module.empty() && module->name != opts.module) - continue; - - SigMap sigmap(module); - - for (auto wire : module->selected_wires()) - { - for (SigBit bit : SigSpec(wire)) - { - SigBit sigbit = sigmap(bit); - - if (bit.wire == nullptr || sigbit.wire == nullptr) - continue; - - if (!bit.wire->port_id != !sigbit.wire->port_id) { - if (bit.wire->port_id) - sigmap.add(bit); - continue; - } - - if (!bit.wire->name[0] != !sigbit.wire->name[0]) { - if (bit.wire->name[0] == '\\') - sigmap.add(bit); - continue; - } - } - } - - for (auto cell : module->selected_cells()) - { - if (!opts.cell.empty() && cell->name != opts.cell) - continue; - - for (auto &conn : cell->connections()) - { - for (int i = 0; i < GetSize(conn.second); i++) { - mutate_t entry; - entry.mode = "inv"; - entry.src = cell->get_src_attribute(); - entry.modname = module->name; - entry.cellname = cell->name; - entry.celltype = cell->type; - entry.cellport = conn.first; - entry.portbit = i; - - if (cell->output(conn.first)) { - SigBit bit = sigmap(conn.second[i]); - if (bit.wire && bit.wire->name[0] == '\\') - entry.outsigbit = bit; - } - - database_add(database, opts, entry); - } - } - } - } - - log("Raw database size: %d\n", GetSize(database)); - if (N != 0) { - database_reduce(database, opts, N); - log("Reduced database size: %d\n", GetSize(database)); - } - - std::ofstream fout; - - if (!filename.empty()) { - fout.open(filename, std::ios::out | std::ios::trunc); - if (!fout.is_open()) - log_error("Could not open file \"%s\" with write access.\n", filename.c_str()); - } - - for (auto &entry : database) { - string str = stringf("mutate -mode %s", entry.mode.c_str()); - if (!entry.modname.empty()) - str += stringf(" -module %s", log_id(entry.modname)); - if (!entry.cellname.empty()) - str += stringf(" -cell %s", log_id(entry.cellname)); - if (!entry.cellport.empty()) - str += stringf(" -port %s", log_id(entry.cellport)); - if (entry.portbit >= 0) - str += stringf(" -bit %d", entry.portbit); - if (entry.outsigbit.wire || !entry.src.empty()) { - str += " #"; - if (!entry.src.empty()) - str += stringf(" %s", entry.src.c_str()); - if (entry.outsigbit.wire) - str += stringf(" %s", log_signal(entry.outsigbit)); - } - if (filename.empty()) - log("%s\n", str.c_str()); - else - fout << str << std::endl; - } + if (N >= 0) { + mutate_list(design, opts, filename, N); + return; + } + if (opts.mode == "inv") { + mutate_inv(design, opts); return; } -- cgit v1.2.3 From 76c9c350e7d0dfc11b609d98bdcd1ea0d845cb06 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 13 Mar 2019 17:36:06 +0100 Subject: Add hashlib "::element(int n)" methods Signed-off-by: Clifford Wolf --- kernel/hashlib.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/kernel/hashlib.h b/kernel/hashlib.h index df534ec1b..e7cb312ed 100644 --- a/kernel/hashlib.h +++ b/kernel/hashlib.h @@ -557,9 +557,11 @@ public: void clear() { hashtable.clear(); entries.clear(); } iterator begin() { return iterator(this, int(entries.size())-1); } + iterator element(int n) { return iterator(this, int(entries.size())-1-n); } iterator end() { return iterator(nullptr, -1); } const_iterator begin() const { return const_iterator(this, int(entries.size())-1); } + const_iterator element(int n) const { return const_iterator(this, int(entries.size())-1-n); } const_iterator end() const { return const_iterator(nullptr, -1); } }; @@ -881,9 +883,11 @@ public: void clear() { hashtable.clear(); entries.clear(); } iterator begin() { return iterator(this, int(entries.size())-1); } + iterator element(int n) { return iterator(this, int(entries.size())-1-n); } iterator end() { return iterator(nullptr, -1); } const_iterator begin() const { return const_iterator(this, int(entries.size())-1); } + const_iterator element(int n) const { return const_iterator(this, int(entries.size())-1-n); } const_iterator end() const { return const_iterator(nullptr, -1); } }; @@ -952,6 +956,7 @@ public: void clear() { database.clear(); } const_iterator begin() const { return database.begin(); } + const_iterator element(int n) const { return database.element(n); } const_iterator end() const { return database.end(); } }; @@ -1051,6 +1056,7 @@ public: void clear() { database.clear(); parents.clear(); } const_iterator begin() const { return database.begin(); } + const_iterator element(int n) const { return database.element(n); } const_iterator end() const { return database.end(); } }; -- cgit v1.2.3 From 6ad5d036c58766b2bd0a705c7adfcbf9af4a7d16 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 13 Mar 2019 17:36:37 +0100 Subject: Add "mutate" command DB reduce functionality Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 193 +++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 181 insertions(+), 12 deletions(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 04aebd897..3ecb955f0 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -25,16 +25,19 @@ PRIVATE_NAMESPACE_BEGIN struct mutate_t { std::string mode, src; - IdString modname, cellname, celltype, cellport; + Module *module; + Cell *cell; + IdString cellport; SigBit outsigbit; int portbit = -1; + bool used = false; }; struct mutate_opts_t { + int seed = 0; std::string mode; IdString module, cell, port; int bit = -1; - IdString ctrl_name; int ctrl_width, ctrl_value; }; @@ -44,10 +47,10 @@ void database_add(std::vector &database, const mutate_opts_t &opts, co if (!opts.mode.empty() && opts.mode != entry.mode) return; - if (!opts.module.empty() && opts.module != entry.modname) + if (!opts.module.empty() && opts.module != entry.module->name) return; - if (!opts.cell.empty() && opts.cell != entry.cellname) + if (!opts.cell.empty() && opts.cell != entry.cell->name) return; if (!opts.port.empty() && opts.port != entry.cellport) @@ -59,8 +62,159 @@ void database_add(std::vector &database, const mutate_opts_t &opts, co database.push_back(entry); } +struct xs128_t +{ + uint32_t x = 123456789; + uint32_t y = 0, z = 0, w = 0; + + xs128_t(int seed = 0) : w(seed) { + next(); + next(); + next(); + } + + void next() { + uint32_t t = x ^ (x << 11); + x = y, y = z, z = w; + w ^= (w >> 19) ^ t ^ (t >> 8); + } + + int operator()() { + next(); + return w & 0x3fffffff; + } + + int operator()(int n) { + if (n < 2) + return 0; + while (1) { + int k = (*this)(), p = k % n; + if ((k - p + n) <= 0x40000000) + return p; + } + } +}; + +struct mutate_leaf_queue_t +{ + pool db; + + mutate_t *pick(xs128_t &rng) { + while (!db.empty()) { + int i = rng(GetSize(db)); + auto it = db.element(i); + mutate_t *m = *it; + db.erase(it); + if (m->used == false) { + m->used = true; + return m; + } + } + return nullptr; + } + + void add(mutate_t *m) { + db.insert(m); + } +}; + +template +struct mutate_inner_queue_t +{ + dict db; + + mutate_t *pick(xs128_t &rng) { + while (!db.empty()) { + int i = rng(GetSize(db)); + auto it = db.element(i); + mutate_t *m = it->second.pick(rng); + if (m != nullptr) + return m; + db.erase(it); + } + return nullptr; + } + + template + void add(mutate_t *m, K key, Args... args) { + db[key].add(m, args...); + } +}; + void database_reduce(std::vector &database, const mutate_opts_t &opts, int N) { + if (N >= GetSize(database)) + return; + + mutate_inner_queue_t primary_queue_wire; + mutate_inner_queue_t primary_queue_bit; + mutate_inner_queue_t primary_queue_cell; + mutate_inner_queue_t primary_queue_src; + + mutate_inner_queue_t> primary_queue_module_wire; + mutate_inner_queue_t> primary_queue_module_bit; + mutate_inner_queue_t> primary_queue_module_cell; + mutate_inner_queue_t> primary_queue_module_src; + + for (auto &m : database) + { + if (m.outsigbit.wire) { + primary_queue_wire.add(&m, m.outsigbit.wire); + primary_queue_bit.add(&m, m.outsigbit); + primary_queue_module_wire.add(&m, m.module, m.outsigbit.wire); + primary_queue_module_bit.add(&m, m.module, m.outsigbit); + } + + primary_queue_cell.add(&m, m.cell); + primary_queue_module_cell.add(&m, m.module, m.cell); + + if (!m.src.empty()) { + primary_queue_src.add(&m, m.src); + primary_queue_module_src.add(&m, m.module, m.src); + } + } + + int weight_pq_w = 100; + int weight_pq_b = 100; + int weight_pq_c = 100; + int weight_pq_s = 100; + + int weight_pq_mw = 100; + int weight_pq_mb = 100; + int weight_pq_mc = 100; + int weight_pq_ms = 100; + + int total_weight = weight_pq_w + weight_pq_b + weight_pq_c + weight_pq_s; + total_weight += weight_pq_mw + weight_pq_mb + weight_pq_mc + weight_pq_ms; + + std::vector new_database; + xs128_t rng(opts.seed); + + while (GetSize(new_database) < N) + { + int k = rng(total_weight); + +#define X(__wght, __queue) \ + k -= __wght; \ + if (k < 0) { \ + mutate_t *m = __queue.pick(rng); \ + if (m != nullptr) \ + new_database.push_back(*m); \ + continue; \ + } + + X(weight_pq_w, primary_queue_wire) + X(weight_pq_b, primary_queue_bit) + X(weight_pq_c, primary_queue_cell) + X(weight_pq_s, primary_queue_src) + + X(weight_pq_mw, primary_queue_module_wire) + X(weight_pq_mb, primary_queue_module_bit) + X(weight_pq_mc, primary_queue_module_cell) + X(weight_pq_ms, primary_queue_module_src) + } + + std::swap(new_database, database); } void mutate_list(Design *design, const mutate_opts_t &opts, const string &filename, int N) @@ -108,9 +262,8 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena mutate_t entry; entry.mode = "inv"; entry.src = cell->get_src_attribute(); - entry.modname = module->name; - entry.cellname = cell->name; - entry.celltype = cell->type; + entry.module = module; + entry.cell = cell; entry.cellport = conn.first; entry.portbit = i; @@ -140,12 +293,17 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena log_error("Could not open file \"%s\" with write access.\n", filename.c_str()); } + int ctrl_value = opts.ctrl_value; + for (auto &entry : database) { - string str = stringf("mutate -mode %s", entry.mode.c_str()); - if (!entry.modname.empty()) - str += stringf(" -module %s", log_id(entry.modname)); - if (!entry.cellname.empty()) - str += stringf(" -cell %s", log_id(entry.cellname)); + string str = "mutate"; + if (!opts.ctrl_name.empty()) + str += stringf(" -ctrl %s %d %d", log_id(opts.ctrl_name), opts.ctrl_width, ctrl_value++); + str += stringf(" -mode %s", entry.mode.c_str()); + if (entry.module) + str += stringf(" -module %s", log_id(entry.module)); + if (entry.cell) + str += stringf(" -cell %s", log_id(entry.cell)); if (!entry.cellport.empty()) str += stringf(" -port %s", log_id(entry.cellport)); if (entry.portbit >= 0) @@ -253,6 +411,13 @@ struct MutatePass : public Pass { log(" -o filename\n"); log(" Write list to this file instead of console output\n"); log("\n"); + log(" -seed N\n"); + log(" RNG seed for selecting mutations\n"); + log("\n"); + log(" -ctrl name width value\n"); + log(" Add -ctrl options to the output. Use 'value' for first mutation, then\n"); + log(" simply count up from there.\n"); + log("\n"); log(" -mode name\n"); log(" -module name\n"); log(" -cell name\n"); @@ -296,6 +461,10 @@ struct MutatePass : public Pass { filename = args[++argidx]; continue; } + if (args[argidx] == "-seed" && argidx+1 < args.size()) { + opts.seed = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-mode" && argidx+1 < args.size()) { opts.mode = args[++argidx]; continue; -- cgit v1.2.3 From bacca5753775bfabed955a9772a5d86d85007c58 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 13 Mar 2019 19:27:17 +0100 Subject: Fix smtbmc.py handling of zero appended steps Signed-off-by: Clifford Wolf --- backends/smt2/smtbmc.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 94a5e2da0..445a42e0d 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1484,11 +1484,11 @@ else: # not tempind, covermode smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) - print_msg("Re-solving with appended steps..") - if smt_check_sat() == "unsat": - print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) - retstatus = False - break + print_msg("Re-solving with appended steps..") + if smt_check_sat() == "unsat": + print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + retstatus = False + break print_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) -- cgit v1.2.3 From 1b4fdbb0d881040220cdf1591f415cd2176481ad Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 19:52:02 +0100 Subject: Add more mutation types, improve mutation src cover Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 360 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 268 insertions(+), 92 deletions(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 3ecb955f0..eac00948a 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -24,20 +24,24 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN struct mutate_t { - std::string mode, src; - Module *module; - Cell *cell; - IdString cellport; - SigBit outsigbit; + string mode; + pool src; + IdString module, cell; + IdString port, wire; int portbit = -1; + int ctrlbit = -1; + int wirebit = -1; bool used = false; }; struct mutate_opts_t { int seed = 0; std::string mode; - IdString module, cell, port; - int bit = -1; + pool src; + IdString module, cell, port, wire; + int portbit = -1; + int ctrlbit = -1; + int wirebit = -1; IdString ctrl_name; int ctrl_width, ctrl_value; }; @@ -47,16 +51,35 @@ void database_add(std::vector &database, const mutate_opts_t &opts, co if (!opts.mode.empty() && opts.mode != entry.mode) return; - if (!opts.module.empty() && opts.module != entry.module->name) + if (!opts.src.empty()) { + bool found_match = false; + for (auto &s : opts.src) { + if (entry.src.count(s)) + found_match = true; + } + if (!found_match) + return; + } + + if (!opts.module.empty() && opts.module != entry.module) + return; + + if (!opts.cell.empty() && opts.cell != entry.cell) + return; + + if (!opts.port.empty() && opts.port != entry.port) + return; + + if (opts.portbit >= 0 && opts.portbit != entry.portbit) return; - if (!opts.cell.empty() && opts.cell != entry.cell->name) + if (opts.ctrlbit >= 0 && opts.ctrlbit != entry.ctrlbit) return; - if (!opts.port.empty() && opts.port != entry.cellport) + if (!opts.wire.empty() && opts.wire != entry.wire) return; - if (opts.bit >= 0 && opts.bit != entry.portbit) + if (opts.wirebit >= 0 && opts.wirebit != entry.wirebit) return; database.push_back(entry); @@ -99,18 +122,48 @@ struct mutate_leaf_queue_t { pool db; - mutate_t *pick(xs128_t &rng) { - while (!db.empty()) { - int i = rng(GetSize(db)); - auto it = db.element(i); - mutate_t *m = *it; - db.erase(it); - if (m->used == false) { - m->used = true; - return m; + mutate_t *pick(xs128_t &rng, dict &coverdb) { + mutate_t *m = nullptr; + if (rng(3)) { + vector candidates; + int best_score = -1; + for (auto p : db) { + if (p->used || p->src.empty()) + continue; + int this_score = -1; + for (auto &s : p->src) { + if (this_score == -1 || this_score > coverdb.at(s)) + this_score = coverdb.at(s); + } + log_assert(this_score != -1); + if (best_score == -1 || this_score < best_score) { + candidates.clear(); + best_score = this_score; + } + if (best_score == this_score) + candidates.push_back(p); } + if (!candidates.empty()) + m = candidates[rng(GetSize(candidates))]; } - return nullptr; + if (m == nullptr) { + while (!db.empty()) { + int i = rng(GetSize(db)); + auto it = db.element(i); + mutate_t *p = *it; + db.erase(it); + if (p->used == false) { + m = p; + break; + } + } + } + if (m != nullptr) { + m->used = true; + for (auto &s : m->src) + coverdb[s]++; + } + return m; } void add(mutate_t *m) { @@ -123,11 +176,11 @@ struct mutate_inner_queue_t { dict db; - mutate_t *pick(xs128_t &rng) { + mutate_t *pick(xs128_t &rng, dict &coverdb) { while (!db.empty()) { int i = rng(GetSize(db)); auto it = db.element(i); - mutate_t *m = it->second.pick(rng); + mutate_t *m = it->second.pick(rng, coverdb); if (m != nullptr) return m; db.erase(it); @@ -141,66 +194,67 @@ struct mutate_inner_queue_t } }; -void database_reduce(std::vector &database, const mutate_opts_t &opts, int N) +void database_reduce(std::vector &database, const mutate_opts_t &/* opts */, int N, xs128_t &rng) { + std::vector new_database; + dict coverdb; + + int weight_pq_w = 100; + int weight_pq_b = 100; + int weight_pq_c = 100; + int weight_pq_s = 100; + + int weight_pq_mw = 100; + int weight_pq_mb = 100; + int weight_pq_mc = 100; + int weight_pq_ms = 100; + + int total_weight = weight_pq_w + weight_pq_b + weight_pq_c + weight_pq_s; + total_weight += weight_pq_mw + weight_pq_mb + weight_pq_mc + weight_pq_ms; + if (N >= GetSize(database)) return; - mutate_inner_queue_t primary_queue_wire; - mutate_inner_queue_t primary_queue_bit; - mutate_inner_queue_t primary_queue_cell; + mutate_inner_queue_t primary_queue_wire; + mutate_inner_queue_t, mutate_leaf_queue_t> primary_queue_bit; + mutate_inner_queue_t primary_queue_cell; mutate_inner_queue_t primary_queue_src; - mutate_inner_queue_t> primary_queue_module_wire; - mutate_inner_queue_t> primary_queue_module_bit; - mutate_inner_queue_t> primary_queue_module_cell; - mutate_inner_queue_t> primary_queue_module_src; + mutate_inner_queue_t> primary_queue_module_wire; + mutate_inner_queue_t, mutate_leaf_queue_t>> primary_queue_module_bit; + mutate_inner_queue_t> primary_queue_module_cell; + mutate_inner_queue_t> primary_queue_module_src; for (auto &m : database) { - if (m.outsigbit.wire) { - primary_queue_wire.add(&m, m.outsigbit.wire); - primary_queue_bit.add(&m, m.outsigbit); - primary_queue_module_wire.add(&m, m.module, m.outsigbit.wire); - primary_queue_module_bit.add(&m, m.module, m.outsigbit); + if (!m.wire.empty()) { + primary_queue_wire.add(&m, m.wire); + primary_queue_bit.add(&m, pair(m.wire, m.wirebit)); + primary_queue_module_wire.add(&m, m.module, m.wire); + primary_queue_module_bit.add(&m, m.module, pair(m.wire, m.wirebit)); } primary_queue_cell.add(&m, m.cell); primary_queue_module_cell.add(&m, m.module, m.cell); - if (!m.src.empty()) { - primary_queue_src.add(&m, m.src); - primary_queue_module_src.add(&m, m.module, m.src); + for (auto &s : m.src) { + coverdb[s] = 0; + primary_queue_src.add(&m, s); + primary_queue_module_src.add(&m, m.module, s); } } - int weight_pq_w = 100; - int weight_pq_b = 100; - int weight_pq_c = 100; - int weight_pq_s = 100; - - int weight_pq_mw = 100; - int weight_pq_mb = 100; - int weight_pq_mc = 100; - int weight_pq_ms = 100; - - int total_weight = weight_pq_w + weight_pq_b + weight_pq_c + weight_pq_s; - total_weight += weight_pq_mw + weight_pq_mb + weight_pq_mc + weight_pq_ms; - - std::vector new_database; - xs128_t rng(opts.seed); - while (GetSize(new_database) < N) { int k = rng(total_weight); -#define X(__wght, __queue) \ - k -= __wght; \ - if (k < 0) { \ - mutate_t *m = __queue.pick(rng); \ - if (m != nullptr) \ - new_database.push_back(*m); \ - continue; \ +#define X(__wght, __queue) \ + k -= __wght; \ + if (k < 0) { \ + mutate_t *m = __queue.pick(rng, coverdb); \ + if (m != nullptr) \ + new_database.push_back(*m); \ + continue; \ } X(weight_pq_w, primary_queue_wire) @@ -215,11 +269,19 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, } std::swap(new_database, database); + + int covered_cnt = 0; + for (auto &it : coverdb) + if (it.second) + covered_cnt++; + + log("Covered %d/%d src attributes (%.2f%%).\n", covered_cnt, GetSize(coverdb), 100.0 * covered_cnt / GetSize(coverdb)); } void mutate_list(Design *design, const mutate_opts_t &opts, const string &filename, int N) { std::vector database; + xs128_t rng(opts.seed); for (auto module : design->selected_modules()) { @@ -260,20 +322,40 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena { for (int i = 0; i < GetSize(conn.second); i++) { mutate_t entry; - entry.mode = "inv"; - entry.src = cell->get_src_attribute(); - entry.module = module; - entry.cell = cell; - entry.cellport = conn.first; + entry.module = module->name; + entry.cell = cell->name; + entry.port = conn.first; entry.portbit = i; - if (cell->output(conn.first)) { - SigBit bit = sigmap(conn.second[i]); - if (bit.wire && bit.wire->name[0] == '\\') - entry.outsigbit = bit; + for (auto &s : cell->get_strpool_attribute("\\src")) + entry.src.insert(s); + + SigBit bit = sigmap(conn.second[i]); + if (bit.wire && bit.wire->name[0] == '\\') { + for (auto &s : bit.wire->get_strpool_attribute("\\src")) + entry.src.insert(s); + entry.wire = bit.wire->name; + entry.wirebit = bit.offset; } + entry.mode = "inv"; + database_add(database, opts, entry); + + entry.mode = "const0"; database_add(database, opts, entry); + + entry.mode = "const1"; + database_add(database, opts, entry); + + entry.mode = "cnot0"; + entry.ctrlbit = rng(GetSize(conn.second)); + if (entry.ctrlbit != entry.portbit && conn.second[entry.ctrlbit].wire) + database_add(database, opts, entry); + + entry.mode = "cnot1"; + entry.ctrlbit = rng(GetSize(conn.second)); + if (entry.ctrlbit != entry.portbit && conn.second[entry.ctrlbit].wire) + database_add(database, opts, entry); } } } @@ -281,7 +363,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena log("Raw database size: %d\n", GetSize(database)); if (N != 0) { - database_reduce(database, opts, N); + database_reduce(database, opts, N, rng); log("Reduced database size: %d\n", GetSize(database)); } @@ -300,21 +382,22 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena if (!opts.ctrl_name.empty()) str += stringf(" -ctrl %s %d %d", log_id(opts.ctrl_name), opts.ctrl_width, ctrl_value++); str += stringf(" -mode %s", entry.mode.c_str()); - if (entry.module) + if (!entry.module.empty()) str += stringf(" -module %s", log_id(entry.module)); - if (entry.cell) + if (!entry.cell.empty()) str += stringf(" -cell %s", log_id(entry.cell)); - if (!entry.cellport.empty()) - str += stringf(" -port %s", log_id(entry.cellport)); + if (!entry.port.empty()) + str += stringf(" -port %s", log_id(entry.port)); if (entry.portbit >= 0) - str += stringf(" -bit %d", entry.portbit); - if (entry.outsigbit.wire || !entry.src.empty()) { - str += " #"; - if (!entry.src.empty()) - str += stringf(" %s", entry.src.c_str()); - if (entry.outsigbit.wire) - str += stringf(" %s", log_signal(entry.outsigbit)); - } + str += stringf(" -portbit %d", entry.portbit); + if (entry.ctrlbit >= 0) + str += stringf(" -ctrlbit %d", entry.ctrlbit); + if (!entry.wire.empty()) + str += stringf(" -wire %s", log_id(entry.wire)); + if (entry.wirebit >= 0) + str += stringf(" -wirebit %d", entry.wirebit); + for (auto &s : entry.src) + str += stringf(" -src %s", s.c_str()); if (filename.empty()) log("%s\n", str.c_str()); else @@ -375,18 +458,18 @@ void mutate_inv(Design *design, const mutate_opts_t &opts) Module *module = design->module(opts.module); Cell *cell = module->cell(opts.cell); - SigBit bit = cell->getPort(opts.port)[opts.bit]; + SigBit bit = cell->getPort(opts.port)[opts.portbit]; SigBit inbit, outbit; if (cell->input(opts.port)) { - log("Add input inverter at %s.%s.%s[%d].\n", log_id(module), log_id(cell), log_id(opts.port), opts.bit); + log("Add input inverter at %s.%s.%s[%d].\n", log_id(module), log_id(cell), log_id(opts.port), opts.portbit); SigBit outbit = module->Not(NEW_ID, bit); bit = mutate_ctrl_mux(module, opts, bit, outbit); } else { - log("Add output inverter at %s.%s.%s[%d].\n", log_id(module), log_id(cell), log_id(opts.port), opts.bit); + log("Add output inverter at %s.%s.%s[%d].\n", log_id(module), log_id(cell), log_id(opts.port), opts.portbit); SigBit inbit = module->addWire(NEW_ID); SigBit outbit = module->Not(NEW_ID, inbit); module->connect(bit, mutate_ctrl_mux(module, opts, inbit, outbit)); @@ -394,7 +477,64 @@ void mutate_inv(Design *design, const mutate_opts_t &opts) } SigSpec s = cell->getPort(opts.port); - s[opts.bit] = bit; + s[opts.portbit] = bit; + cell->setPort(opts.port, s); +} + +void mutate_const(Design *design, const mutate_opts_t &opts, bool one) +{ + Module *module = design->module(opts.module); + Cell *cell = module->cell(opts.cell); + + SigBit bit = cell->getPort(opts.port)[opts.portbit]; + SigBit inbit, outbit; + + if (cell->input(opts.port)) + { + log("Add input constant %d at %s.%s.%s[%d].\n", one ? 1 : 0, log_id(module), log_id(cell), log_id(opts.port), opts.portbit); + SigBit outbit = one ? State::S1 : State::S0; + bit = mutate_ctrl_mux(module, opts, bit, outbit); + } + else + { + log("Add output constant %d at %s.%s.%s[%d].\n", one ? 1 : 0, log_id(module), log_id(cell), log_id(opts.port), opts.portbit); + SigBit inbit = module->addWire(NEW_ID); + SigBit outbit = one ? State::S1 : State::S0; + module->connect(bit, mutate_ctrl_mux(module, opts, inbit, outbit)); + bit = inbit; + } + + SigSpec s = cell->getPort(opts.port); + s[opts.portbit] = bit; + cell->setPort(opts.port, s); +} + +void mutate_cnot(Design *design, const mutate_opts_t &opts, bool one) +{ + Module *module = design->module(opts.module); + Cell *cell = module->cell(opts.cell); + + SigBit bit = cell->getPort(opts.port)[opts.portbit]; + SigBit ctrl = cell->getPort(opts.port)[opts.ctrlbit]; + SigBit inbit, outbit; + + if (cell->input(opts.port)) + { + log("Add input cnot%d at %s.%s.%s[%d,%d].\n", one ? 1 : 0, log_id(module), log_id(cell), log_id(opts.port), opts.portbit, opts.ctrlbit); + SigBit outbit = one ? module->Xor(NEW_ID, bit, ctrl) : module->Xnor(NEW_ID, bit, ctrl); + bit = mutate_ctrl_mux(module, opts, bit, outbit); + } + else + { + log("Add output cnot%d at %s.%s.%s[%d,%d].\n", one ? 1 : 0, log_id(module), log_id(cell), log_id(opts.port), opts.portbit, opts.ctrlbit); + SigBit inbit = module->addWire(NEW_ID); + SigBit outbit = one ? module->Xor(NEW_ID, inbit, ctrl) : module->Xnor(NEW_ID, inbit, ctrl); + module->connect(bit, mutate_ctrl_mux(module, opts, inbit, outbit)); + bit = inbit; + } + + SigSpec s = cell->getPort(opts.port); + s[opts.portbit] = bit; cell->setPort(opts.port, s); } @@ -422,7 +562,11 @@ struct MutatePass : public Pass { log(" -module name\n"); log(" -cell name\n"); log(" -port name\n"); - log(" -bit int\n"); + log(" -portbit int\n"); + log(" -ctrlbit int\n"); + log(" -wire name\n"); + log(" -wirebit int\n"); + log(" -src string\n"); log(" Filter list of mutation candidates to those matching\n"); log(" the given parameters.\n"); log("\n"); @@ -438,9 +582,15 @@ struct MutatePass : public Pass { log(" -module name\n"); log(" -cell name\n"); log(" -port name\n"); - log(" -bit int\n"); + log(" -portbit int\n"); + log(" -ctrlbit int\n"); log(" Mutation parameters, as generated by 'mutate -list N'.\n"); log("\n"); + log(" -wire name\n"); + log(" -wirebit int\n"); + log(" -src string\n"); + log(" Ignored. (They are generated by -list for documentation purposes.)\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { @@ -487,8 +637,24 @@ struct MutatePass : public Pass { opts.port = RTLIL::escape_id(args[++argidx]); continue; } - if (args[argidx] == "-bit" && argidx+1 < args.size()) { - opts.bit = atoi(args[++argidx].c_str()); + if (args[argidx] == "-portbit" && argidx+1 < args.size()) { + opts.portbit = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-ctrlbit" && argidx+1 < args.size()) { + opts.ctrlbit = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-wire" && argidx+1 < args.size()) { + opts.wire = RTLIL::escape_id(args[++argidx]); + continue; + } + if (args[argidx] == "-wirebit" && argidx+1 < args.size()) { + opts.wirebit = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-src" && argidx+1 < args.size()) { + opts.src.insert(args[++argidx]); continue; } break; @@ -505,6 +671,16 @@ struct MutatePass : public Pass { return; } + if (opts.mode == "const0" || opts.mode == "const1") { + mutate_const(design, opts, opts.mode == "const1"); + return; + } + + if (opts.mode == "cnot0" || opts.mode == "cnot1") { + mutate_cnot(design, opts, opts.mode == "cnot1"); + return; + } + log_cmd_error("Invalid mode: %s\n", opts.mode.c_str()); } } MutatePass; -- cgit v1.2.3 From 2a4263a75d0bbbc5b8f2de797b572d6f1d64818b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 23:01:01 +0100 Subject: Improve "mutate" wire coverage metric Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index eac00948a..243a1b48a 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -289,6 +289,21 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena continue; SigMap sigmap(module); + dict bit_user_cnt; + + for (auto wire : module->wires()) { + if (wire->name[0] == '\\' && wire->attributes.count("\\src")) + sigmap.add(wire); + } + + for (auto cell : module->cells()) { + for (auto &conn : cell->connections()) { + if (cell->output(conn.first)) + continue; + for (auto bit : sigmap(conn.second)) + bit_user_cnt[bit]++; + } + } for (auto wire : module->selected_wires()) { @@ -331,7 +346,7 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena entry.src.insert(s); SigBit bit = sigmap(conn.second[i]); - if (bit.wire && bit.wire->name[0] == '\\') { + if (bit.wire && bit.wire->name[0] == '\\' && (cell->output(conn.first) || bit_user_cnt[bit] == 1)) { for (auto &s : bit.wire->get_strpool_attribute("\\src")) entry.src.insert(s); entry.wire = bit.wire->name; -- cgit v1.2.3 From 4d304e3da77a571d1febfebca1409f522177af38 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 23:01:55 +0100 Subject: Add a strictly coverage-driven mutation selection strategy Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 70 insertions(+), 1 deletion(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 243a1b48a..440e8b056 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -199,6 +199,8 @@ void database_reduce(std::vector &database, const mutate_opts_t &/* op std::vector new_database; dict coverdb; + int weight_cover = 500; + int weight_pq_w = 100; int weight_pq_b = 100; int weight_pq_c = 100; @@ -209,7 +211,7 @@ void database_reduce(std::vector &database, const mutate_opts_t &/* op int weight_pq_mc = 100; int weight_pq_ms = 100; - int total_weight = weight_pq_w + weight_pq_b + weight_pq_c + weight_pq_s; + int total_weight = weight_cover + weight_pq_w + weight_pq_b + weight_pq_c + weight_pq_s; total_weight += weight_pq_mw + weight_pq_mb + weight_pq_mc + weight_pq_ms; if (N >= GetSize(database)) @@ -244,10 +246,76 @@ void database_reduce(std::vector &database, const mutate_opts_t &/* op } } + vector cover_candidates; + int best_cover_score = -1; + bool skip_cover = false; + while (GetSize(new_database) < N) { int k = rng(total_weight); + k -= weight_cover; + if (k < 0) { + while (!skip_cover) { + if (cover_candidates.empty()) { + best_cover_score = -1; + for (auto &m : database) { + if (m.used || m.src.empty()) + continue; + int this_score = -1; + for (auto &s : m.src) { + if (this_score == -1 || this_score > coverdb.at(s)) + this_score = coverdb.at(s); + } + log_assert(this_score != -1); + if (best_cover_score == -1 || this_score < best_cover_score) { + cover_candidates.clear(); + best_cover_score = this_score; + } + if (best_cover_score == this_score) + cover_candidates.push_back(&m); + } + if (best_cover_score == -1) { + skip_cover = true; + break; + } + } + + mutate_t *m = nullptr; + while (!cover_candidates.empty()) + { + int idx = rng(GetSize(cover_candidates)); + mutate_t *p = cover_candidates[idx]; + cover_candidates[idx] = cover_candidates.back(); + cover_candidates.pop_back(); + + if (p->used) + continue; + + int this_score = -1; + for (auto &s : p->src) { + if (this_score == -1 || this_score > coverdb.at(s)) + this_score = coverdb.at(s); + } + + if (this_score != best_cover_score) + continue; + + m = p; + break; + } + + if (m != nullptr) { + m->used = true; + for (auto &s : m->src) + coverdb[s]++; + new_database.push_back(*m); + break; + } + } + continue; + } + #define X(__wght, __queue) \ k -= __wght; \ if (k < 0) { \ @@ -266,6 +334,7 @@ void database_reduce(std::vector &database, const mutate_opts_t &/* op X(weight_pq_mb, primary_queue_module_bit) X(weight_pq_mc, primary_queue_module_cell) X(weight_pq_ms, primary_queue_module_src) +#undef X } std::swap(new_database, database); -- cgit v1.2.3 From 27a5d9c91e44dd04fa45e1e2aeff8c6d1cd50872 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Mar 2019 23:20:41 +0100 Subject: Add "mutate -cfg", improve pick_cover behavior Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 147 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 101 insertions(+), 46 deletions(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 440e8b056..6b9eb3c04 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -42,8 +42,23 @@ struct mutate_opts_t { int portbit = -1; int ctrlbit = -1; int wirebit = -1; + IdString ctrl_name; - int ctrl_width, ctrl_value; + int ctrl_width = -1, ctrl_value = -1; + + int pick_cover_prcnt = 50; + + int weight_cover = 500; + + int weight_pq_w = 100; + int weight_pq_b = 100; + int weight_pq_c = 100; + int weight_pq_s = 100; + + int weight_pq_mw = 100; + int weight_pq_mb = 100; + int weight_pq_mc = 100; + int weight_pq_ms = 100; }; void database_add(std::vector &database, const mutate_opts_t &opts, const mutate_t &entry) @@ -122,25 +137,19 @@ struct mutate_leaf_queue_t { pool db; - mutate_t *pick(xs128_t &rng, dict &coverdb) { + mutate_t *pick(xs128_t &rng, dict &coverdb, const mutate_opts_t &opts) { mutate_t *m = nullptr; - if (rng(3)) { + if (rng(100) < opts.pick_cover_prcnt) { vector candidates; - int best_score = -1; for (auto p : db) { if (p->used || p->src.empty()) continue; - int this_score = -1; + bool is_covered = false; for (auto &s : p->src) { - if (this_score == -1 || this_score > coverdb.at(s)) - this_score = coverdb.at(s); - } - log_assert(this_score != -1); - if (best_score == -1 || this_score < best_score) { - candidates.clear(); - best_score = this_score; + if (coverdb.at(s)) + is_covered = true; } - if (best_score == this_score) + if (!is_covered) candidates.push_back(p); } if (!candidates.empty()) @@ -176,11 +185,11 @@ struct mutate_inner_queue_t { dict db; - mutate_t *pick(xs128_t &rng, dict &coverdb) { + mutate_t *pick(xs128_t &rng, dict &coverdb, const mutate_opts_t &opts) { while (!db.empty()) { int i = rng(GetSize(db)); auto it = db.element(i); - mutate_t *m = it->second.pick(rng, coverdb); + mutate_t *m = it->second.pick(rng, coverdb, opts); if (m != nullptr) return m; db.erase(it); @@ -194,25 +203,13 @@ struct mutate_inner_queue_t } }; -void database_reduce(std::vector &database, const mutate_opts_t &/* opts */, int N, xs128_t &rng) +void database_reduce(std::vector &database, const mutate_opts_t &opts, int N, xs128_t &rng) { std::vector new_database; dict coverdb; - int weight_cover = 500; - - int weight_pq_w = 100; - int weight_pq_b = 100; - int weight_pq_c = 100; - int weight_pq_s = 100; - - int weight_pq_mw = 100; - int weight_pq_mb = 100; - int weight_pq_mc = 100; - int weight_pq_ms = 100; - - int total_weight = weight_cover + weight_pq_w + weight_pq_b + weight_pq_c + weight_pq_s; - total_weight += weight_pq_mw + weight_pq_mb + weight_pq_mc + weight_pq_ms; + int total_weight = opts.weight_cover + opts.weight_pq_w + opts.weight_pq_b + opts.weight_pq_c + opts.weight_pq_s; + total_weight += opts.weight_pq_mw + opts.weight_pq_mb + opts.weight_pq_mc + opts.weight_pq_ms; if (N >= GetSize(database)) return; @@ -254,7 +251,7 @@ void database_reduce(std::vector &database, const mutate_opts_t &/* op { int k = rng(total_weight); - k -= weight_cover; + k -= opts.weight_cover; if (k < 0) { while (!skip_cover) { if (cover_candidates.empty()) { @@ -316,24 +313,24 @@ void database_reduce(std::vector &database, const mutate_opts_t &/* op continue; } -#define X(__wght, __queue) \ - k -= __wght; \ - if (k < 0) { \ - mutate_t *m = __queue.pick(rng, coverdb); \ - if (m != nullptr) \ - new_database.push_back(*m); \ - continue; \ +#define X(__wght, __queue) \ + k -= __wght; \ + if (k < 0) { \ + mutate_t *m = __queue.pick(rng, coverdb, opts); \ + if (m != nullptr) \ + new_database.push_back(*m); \ + continue; \ } - X(weight_pq_w, primary_queue_wire) - X(weight_pq_b, primary_queue_bit) - X(weight_pq_c, primary_queue_cell) - X(weight_pq_s, primary_queue_src) + X(opts.weight_pq_w, primary_queue_wire) + X(opts.weight_pq_b, primary_queue_bit) + X(opts.weight_pq_c, primary_queue_cell) + X(opts.weight_pq_s, primary_queue_src) - X(weight_pq_mw, primary_queue_module_wire) - X(weight_pq_mb, primary_queue_module_bit) - X(weight_pq_mc, primary_queue_module_cell) - X(weight_pq_ms, primary_queue_module_src) + X(opts.weight_pq_mw, primary_queue_module_wire) + X(opts.weight_pq_mb, primary_queue_module_bit) + X(opts.weight_pq_mc, primary_queue_module_cell) + X(opts.weight_pq_ms, primary_queue_module_src) #undef X } @@ -654,6 +651,12 @@ struct MutatePass : public Pass { log(" Filter list of mutation candidates to those matching\n"); log(" the given parameters.\n"); log("\n"); + log(" -cfg option int\n"); + log(" Set a configuration option. Options available:\n"); + log(" weight_pq_w weight_pq_b weight_pq_c weight_pq_s\n"); + log(" weight_pq_mw weight_pq_mb weight_pq_mc weight_pq_ms\n"); + log(" weight_cover pick_cover_prcnt\n"); + log("\n"); log("\n"); log(" mutate -mode MODE [options]\n"); log("\n"); @@ -741,6 +744,58 @@ struct MutatePass : public Pass { opts.src.insert(args[++argidx]); continue; } + if (args[argidx] == "-cfg" && argidx+2 < args.size()) { + if (args[argidx+1] == "pick_cover_prcnt") { + opts.pick_cover_prcnt = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_cover") { + opts.weight_cover = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_w") { + opts.weight_pq_w = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_b") { + opts.weight_pq_b = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_c") { + opts.weight_pq_c = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_s") { + opts.weight_pq_s = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_mw") { + opts.weight_pq_mw = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_mb") { + opts.weight_pq_mb = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_mc") { + opts.weight_pq_mc = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + if (args[argidx+1] == "weight_pq_ms") { + opts.weight_pq_ms = atoi(args[argidx+2].c_str()); + argidx += 2; + continue; + } + } break; } extra_args(args, argidx, design); -- cgit v1.2.3 From d1985f6a223d18e0ae8545a620e4117fd4ca23b3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 15 Mar 2019 00:18:31 +0100 Subject: Improvements in "mutate" list-reduce algorithm Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 49 ++++++++++++++++++++++++++++++++++++------------- 1 file changed, 36 insertions(+), 13 deletions(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 6b9eb3c04..4c103dcd5 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -133,7 +133,7 @@ struct xs128_t } }; -struct mutate_leaf_queue_t +struct mutate_queue_t { pool db; @@ -181,7 +181,7 @@ struct mutate_leaf_queue_t }; template -struct mutate_inner_queue_t +struct mutate_chain_queue_t { dict db; @@ -203,6 +203,29 @@ struct mutate_inner_queue_t } }; +template +struct mutate_once_queue_t +{ + dict db; + + mutate_t *pick(xs128_t &rng, dict &coverdb, const mutate_opts_t &opts) { + while (!db.empty()) { + int i = rng(GetSize(db)); + auto it = db.element(i); + mutate_t *m = it->second.pick(rng, coverdb, opts); + db.erase(it); + if (m != nullptr) + return m; + } + return nullptr; + } + + template + void add(mutate_t *m, K key, Args... args) { + db[key].add(m, args...); + } +}; + void database_reduce(std::vector &database, const mutate_opts_t &opts, int N, xs128_t &rng) { std::vector new_database; @@ -214,26 +237,26 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, if (N >= GetSize(database)) return; - mutate_inner_queue_t primary_queue_wire; - mutate_inner_queue_t, mutate_leaf_queue_t> primary_queue_bit; - mutate_inner_queue_t primary_queue_cell; - mutate_inner_queue_t primary_queue_src; + mutate_once_queue_t, mutate_queue_t> primary_queue_wire; + mutate_once_queue_t, mutate_queue_t> primary_queue_bit; + mutate_once_queue_t, mutate_queue_t> primary_queue_cell; + mutate_once_queue_t primary_queue_src; - mutate_inner_queue_t> primary_queue_module_wire; - mutate_inner_queue_t, mutate_leaf_queue_t>> primary_queue_module_bit; - mutate_inner_queue_t> primary_queue_module_cell; - mutate_inner_queue_t> primary_queue_module_src; + mutate_chain_queue_t> primary_queue_module_wire; + mutate_chain_queue_t, mutate_queue_t>> primary_queue_module_bit; + mutate_chain_queue_t> primary_queue_module_cell; + mutate_chain_queue_t> primary_queue_module_src; for (auto &m : database) { if (!m.wire.empty()) { - primary_queue_wire.add(&m, m.wire); - primary_queue_bit.add(&m, pair(m.wire, m.wirebit)); + primary_queue_wire.add(&m, tuple(m.module, m.wire)); + primary_queue_bit.add(&m, tuple(m.module, m.wire, m.wirebit)); primary_queue_module_wire.add(&m, m.module, m.wire); primary_queue_module_bit.add(&m, m.module, pair(m.wire, m.wirebit)); } - primary_queue_cell.add(&m, m.cell); + primary_queue_cell.add(&m, tuple(m.module, m.cell)); primary_queue_module_cell.add(&m, m.module, m.cell); for (auto &s : m.src) { -- cgit v1.2.3 From 9820ed6531f8bd3e30f44f59ae9c82bdc896f57c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 15 Mar 2019 00:48:23 +0100 Subject: Disable realmath tests Signed-off-by: Clifford Wolf --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b8fbcc040..2e4605f8b 100644 --- a/Makefile +++ b/Makefile @@ -575,7 +575,7 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/simple && bash run-test.sh $(SEEDOPT) +cd tests/hana && bash run-test.sh $(SEEDOPT) +cd tests/asicworld && bash run-test.sh $(SEEDOPT) - +cd tests/realmath && bash run-test.sh $(SEEDOPT) + # +cd tests/realmath && bash run-test.sh $(SEEDOPT) +cd tests/share && bash run-test.sh $(SEEDOPT) +cd tests/fsm && bash run-test.sh $(SEEDOPT) +cd tests/techmap && bash run-test.sh -- cgit v1.2.3 From 370db33a4c347049cb8f66c181d39fd2f2ce5e3a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 15 Mar 2019 20:18:38 +0100 Subject: Add fmcombine pass Signed-off-by: Clifford Wolf --- kernel/celltypes.h | 45 +++++--- kernel/rtlil.cc | 4 +- passes/sat/Makefile.inc | 1 + passes/sat/fmcombine.cc | 292 ++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 325 insertions(+), 17 deletions(-) create mode 100644 passes/sat/fmcombine.cc diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 8b8a56111..ae88f4aaf 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -81,6 +81,27 @@ struct CellTypes } void setup_internals() + { + setup_internals_eval(); + + IdString A = "\\A", B = "\\B", EN = "\\EN", Y = "\\Y"; + + setup_type("$tribuf", {A, EN}, {Y}, true); + + setup_type("$assert", {A, EN}, pool(), true); + setup_type("$assume", {A, EN}, pool(), true); + setup_type("$live", {A, EN}, pool(), true); + setup_type("$fair", {A, EN}, pool(), true); + setup_type("$cover", {A, EN}, pool(), true); + setup_type("$initstate", pool(), {Y}, true); + setup_type("$anyconst", pool(), {Y}, true); + setup_type("$anyseq", pool(), {Y}, true); + setup_type("$allconst", pool(), {Y}, true); + setup_type("$allseq", pool(), {Y}, true); + setup_type("$equiv", {A, B}, {Y}, true); + } + + void setup_internals_eval() { std::vector unary_ops = { "$not", "$pos", "$neg", @@ -111,20 +132,6 @@ struct CellTypes setup_type("$lcu", {P, G, CI}, {CO}, true); setup_type("$alu", {A, B, CI, BI}, {X, Y, CO}, true); setup_type("$fa", {A, B, C}, {X, Y}, true); - - setup_type("$tribuf", {A, EN}, {Y}, true); - - setup_type("$assert", {A, EN}, pool(), true); - setup_type("$assume", {A, EN}, pool(), true); - setup_type("$live", {A, EN}, pool(), true); - setup_type("$fair", {A, EN}, pool(), true); - setup_type("$cover", {A, EN}, pool(), true); - setup_type("$initstate", pool(), {Y}, true); - setup_type("$anyconst", pool(), {Y}, true); - setup_type("$anyseq", pool(), {Y}, true); - setup_type("$allconst", pool(), {Y}, true); - setup_type("$allseq", pool(), {Y}, true); - setup_type("$equiv", {A, B}, {Y}, true); } void setup_internals_mem() @@ -153,6 +160,15 @@ struct CellTypes } void setup_stdcells() + { + setup_stdcells_eval(); + + IdString A = "\\A", E = "\\E", Y = "\\Y"; + + setup_type("$_TBUF_", {A, E}, {Y}, true); + } + + void setup_stdcells_eval() { IdString A = "\\A", B = "\\B", C = "\\C", D = "\\D"; IdString E = "\\E", F = "\\F", G = "\\G", H = "\\H"; @@ -179,7 +195,6 @@ struct CellTypes setup_type("$_OAI3_", {A, B, C}, {Y}, true); setup_type("$_AOI4_", {A, B, C, D}, {Y}, true); setup_type("$_OAI4_", {A, B, C, D}, {Y}, true); - setup_type("$_TBUF_", {A, E}, {Y}, true); } void setup_stdcells_mem() diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 7f1816190..d0fa88890 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -760,7 +760,7 @@ namespace { void check() { - if (cell->type.substr(0, 1) != "$" || cell->type.substr(0, 3) == "$__" || cell->type.substr(0, 8) == "$paramod" || + if (cell->type.substr(0, 1) != "$" || cell->type.substr(0, 3) == "$__" || cell->type.substr(0, 8) == "$paramod" || cell->type.substr(0,10) == "$fmcombine" || cell->type.substr(0, 9) == "$verific$" || cell->type.substr(0, 7) == "$array:" || cell->type.substr(0, 8) == "$extern:") return; @@ -2360,7 +2360,7 @@ void RTLIL::Cell::check() void RTLIL::Cell::fixup_parameters(bool set_a_signed, bool set_b_signed) { - if (type.substr(0, 1) != "$" || type.substr(0, 2) == "$_" || type.substr(0, 8) == "$paramod" || + if (type.substr(0, 1) != "$" || type.substr(0, 2) == "$_" || type.substr(0, 8) == "$paramod" || type.substr(0,10) == "$fmcombine" || type.substr(0, 9) == "$verific$" || type.substr(0, 7) == "$array:" || type.substr(0, 8) == "$extern:") return; diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index e91df1eb0..4eced2ff1 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -9,5 +9,6 @@ OBJS += passes/sat/assertpmux.o OBJS += passes/sat/clk2fflogic.o OBJS += passes/sat/async2sync.o OBJS += passes/sat/supercover.o +OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc new file mode 100644 index 000000000..b8a0e94c8 --- /dev/null +++ b/passes/sat/fmcombine.cc @@ -0,0 +1,292 @@ +/* + * 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/yosys.h" +#include "kernel/sigtools.h" +#include "kernel/celltypes.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct FmcombineWorker +{ + Design *design; + Module *original = nullptr; + Module *module = nullptr; + IdString orig_type, combined_type; + + FmcombineWorker(Design *design, IdString orig_type) : + design(design), original(design->module(orig_type)), + orig_type(orig_type), combined_type("$fmcombine" + orig_type.str()) + { + } + + SigSpec import_sig(SigSpec sig, const string &suffix) + { + SigSpec newsig; + for (auto chunk : sig.chunks()) { + if (chunk.wire != nullptr) + chunk.wire = module->wire(chunk.wire->name.str() + suffix); + newsig.append(chunk); + } + return newsig; + } + + void import_prim_cell(Cell *cell, const string &suffix) + { + Cell *c = module->addCell(cell->name.str() + suffix, cell->type); + c->parameters = cell->parameters; + c->attributes = cell->attributes; + + for (auto &conn : cell->connections()) + c->setPort(conn.first, import_sig(conn.second, suffix)); + } + + void import_hier_cell(Cell *cell) + { + if (!cell->parameters.empty()) + log_cmd_error("Cell %s.%s has unresolved instance parameters.\n", log_id(original), log_id(cell)); + + FmcombineWorker sub_worker(design, cell->type); + sub_worker.generate(); + + Cell *c = module->addCell(cell->name.str() + "_combined", sub_worker.combined_type); + // c->parameters = cell->parameters; + c->attributes = cell->attributes; + + for (auto &conn : cell->connections()) { + c->setPort(conn.first.str() + "_gold", import_sig(conn.second, "_gold")); + c->setPort(conn.first.str() + "_gate", import_sig(conn.second, "_gate")); + } + } + + void generate() + { + if (design->module(combined_type)) { + // log("Combined module %s already exists.\n", log_id(combined_type)); + return; + } + + log("Generating combined module %s from module %s.\n", log_id(combined_type), log_id(orig_type)); + module = design->addModule(combined_type); + + for (auto wire : original->wires()) { + module->addWire(wire->name.str() + "_gold", wire); + module->addWire(wire->name.str() + "_gate", wire); + } + module->fixup_ports(); + + for (auto cell : original->cells()) { + if (design->module(cell->type) == nullptr) { + import_prim_cell(cell, "_gold"); + import_prim_cell(cell, "_gate"); + } else { + import_hier_cell(cell); + } + } + + for (auto &conn : original->connections()) { + module->connect(import_sig(conn.first, "_gold"), import_sig(conn.second, "_gold")); + module->connect(import_sig(conn.first, "_gate"), import_sig(conn.second, "_gate")); + } + + CellTypes ct; + ct.setup_internals_eval(); + ct.setup_stdcells_eval(); + + SigMap sigmap(module); + + dict data_bit_to_eq_net; + dict cell_to_eq_nets; + dict reduce_db; + dict invert_db; + + for (auto cell : original->cells()) + { + if (!ct.cell_known(cell->type)) + continue; + + for (auto &conn : cell->connections()) + { + if (!cell->output(conn.first)) + continue; + + SigSpec A = import_sig(conn.second, "_gold"); + SigSpec B = import_sig(conn.second, "_gate"); + SigBit EQ = module->Eq(NEW_ID, A, B); + + for (auto bit : sigmap({A, B})) + data_bit_to_eq_net[bit] = EQ; + + cell_to_eq_nets[cell].append(EQ); + } + } + + for (auto cell : original->cells()) + { + if (!ct.cell_known(cell->type)) + continue; + + bool skip_cell = !cell_to_eq_nets.count(cell); + pool src_eq_bits; + + for (auto &conn : cell->connections()) + { + if (skip_cell) + break; + + if (cell->output(conn.first)) + continue; + + SigSpec A = import_sig(conn.second, "_gold"); + SigSpec B = import_sig(conn.second, "_gate"); + + for (auto bit : sigmap({A, B})) { + if (data_bit_to_eq_net.count(bit)) + src_eq_bits.insert(data_bit_to_eq_net.at(bit)); + else + skip_cell = true; + } + } + + if (!skip_cell) { + SigSpec antecedent = SigSpec(src_eq_bits); + antecedent.sort_and_unify(); + + if (GetSize(antecedent) > 1) { + if (reduce_db.count(antecedent) == 0) + reduce_db[antecedent] = module->ReduceAnd(NEW_ID, antecedent); + antecedent = reduce_db.at(antecedent); + } + + SigSpec consequent = cell_to_eq_nets.at(cell); + consequent.sort_and_unify(); + + if (GetSize(consequent) > 1) { + if (reduce_db.count(consequent) == 0) + reduce_db[consequent] = module->ReduceAnd(NEW_ID, consequent); + consequent = reduce_db.at(consequent); + } + + module->addAssume(NEW_ID, consequent, antecedent); + + if (invert_db.count(antecedent) == 0) + invert_db[antecedent] = module->Not(NEW_ID, antecedent); + + if (invert_db.count(consequent) == 0) + invert_db[consequent] = module->Not(NEW_ID, consequent); + + module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent)); + } + } + } +}; + +struct FmcombinePass : public Pass { + FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { } + void help() YS_OVERRIDE + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" fmcombine [options] module_name gold_cell gate_cell\n"); + // log(" fmcombine [options] @gold_cell @gate_cell\n"); + log("\n"); + log("This pass takes two cells, which are instances of the same module, and replaces\n"); + log("them with one instance of a special 'combined' module, that effectively\n"); + log("contains two copies of the original module, plus some formal properties.\n"); + log("\n"); + log("This is useful for formal test benches that check what differences in behavior\n"); + log("a slight difference in input causes in a module.\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE + { + Module *module = nullptr; + Cell *gold_cell = nullptr; + Cell *gate_cell = nullptr; + + log_header(design, "Executing FMCOMBINE pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + // if (args[argidx] == "-o" && argidx+1 < args.size()) { + // filename = args[++argidx]; + // continue; + // } + break; + } + if (argidx+2 == args.size()) + { + string gold_name = args[argidx++]; + string gate_name = args[argidx++]; + log_cmd_error("fmcombine @gold_cell @gate_cell call style is not implemented yet."); + } + else if (argidx+3 == args.size()) + { + IdString module_name = RTLIL::escape_id(args[argidx++]); + IdString gold_name = RTLIL::escape_id(args[argidx++]); + IdString gate_name = RTLIL::escape_id(args[argidx++]); + + module = design->module(module_name); + if (module == nullptr) + log_cmd_error("Module %s not found.\n", log_id(module_name)); + + gold_cell = module->cell(gold_name); + if (gold_cell == nullptr) + log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gold_name), log_id(module)); + + gate_cell = module->cell(gate_name); + if (gate_cell == nullptr) + log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gate_name), log_id(module)); + } + else + { + log_cmd_error("Invalid number of arguments.\n"); + } + // extra_args(args, argidx, design); + + if (gold_cell->type != gate_cell->type) + log_cmd_error("Types of gold and gate cells do not match.\n"); + if (!gold_cell->parameters.empty()) + log_cmd_error("Gold cell has unresolved instance parameters.\n"); + if (!gate_cell->parameters.empty()) + log_cmd_error("Gold cell has unresolved instance parameters.\n"); + + FmcombineWorker worker(design, gold_cell->type); + worker.generate(); + IdString combined_cell_name = module->uniquify(stringf("\\%s_%s", log_id(gold_cell), log_id(gate_cell))); + + Cell *cell = module->addCell(combined_cell_name, worker.combined_type); + cell->attributes = gold_cell->attributes; + cell->add_strpool_attribute("\\src", gate_cell->get_strpool_attribute("\\src")); + + log("Combining cells %s and %s in module %s into new cell %s.\n", log_id(gold_cell), log_id(gate_cell), log_id(module), log_id(cell)); + + for (auto &conn : gold_cell->connections()) + cell->setPort(conn.first.str() + "_gold", conn.second); + module->remove(gold_cell); + + for (auto &conn : gate_cell->connections()) + cell->setPort(conn.first.str() + "_gate", conn.second); + module->remove(gate_cell); + } +} FmcombinePass; + +PRIVATE_NAMESPACE_END -- cgit v1.2.3 From dacaebae35c81b4f4970af3ef8bfdb73691fa215 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 15 Mar 2019 21:45:37 +0100 Subject: Add "fmcombine -fwd -bwd -nop" Signed-off-by: Clifford Wolf --- passes/sat/fmcombine.cc | 69 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 59 insertions(+), 10 deletions(-) diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc index b8a0e94c8..cd75ca860 100644 --- a/passes/sat/fmcombine.cc +++ b/passes/sat/fmcombine.cc @@ -24,15 +24,23 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct opts_t +{ + bool fwd = false; + bool bwd = false; + bool nop = false; +}; + struct FmcombineWorker { + const opts_t &opts; Design *design; Module *original = nullptr; Module *module = nullptr; IdString orig_type, combined_type; - FmcombineWorker(Design *design, IdString orig_type) : - design(design), original(design->module(orig_type)), + FmcombineWorker(Design *design, IdString orig_type, const opts_t &opts) : + opts(opts), design(design), original(design->module(orig_type)), orig_type(orig_type), combined_type("$fmcombine" + orig_type.str()) { } @@ -63,7 +71,7 @@ struct FmcombineWorker if (!cell->parameters.empty()) log_cmd_error("Cell %s.%s has unresolved instance parameters.\n", log_id(original), log_id(cell)); - FmcombineWorker sub_worker(design, cell->type); + FmcombineWorker sub_worker(design, cell->type, opts); sub_worker.generate(); Cell *c = module->addCell(cell->name.str() + "_combined", sub_worker.combined_type); @@ -106,6 +114,9 @@ struct FmcombineWorker module->connect(import_sig(conn.first, "_gate"), import_sig(conn.second, "_gate")); } + if (opts.nop) + return; + CellTypes ct; ct.setup_internals_eval(); ct.setup_stdcells_eval(); @@ -184,15 +195,19 @@ struct FmcombineWorker consequent = reduce_db.at(consequent); } - module->addAssume(NEW_ID, consequent, antecedent); + if (opts.fwd) + module->addAssume(NEW_ID, consequent, antecedent); - if (invert_db.count(antecedent) == 0) - invert_db[antecedent] = module->Not(NEW_ID, antecedent); + if (opts.bwd) + { + if (invert_db.count(antecedent) == 0) + invert_db[antecedent] = module->Not(NEW_ID, antecedent); - if (invert_db.count(consequent) == 0) - invert_db[consequent] = module->Not(NEW_ID, consequent); + if (invert_db.count(consequent) == 0) + invert_db[consequent] = module->Not(NEW_ID, consequent); - module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent)); + module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent)); + } } } } @@ -214,9 +229,25 @@ struct FmcombinePass : public Pass { log("This is useful for formal test benches that check what differences in behavior\n"); log("a slight difference in input causes in a module.\n"); log("\n"); + log(" -fwd\n"); + log(" Insert forward hint assumptions into the combined module.\n"); + log("\n"); + log(" -bwd\n"); + log(" Insert backward hint assumptions into the combined module.\n"); + log(" (Backward hints are logically equivalend to fordward hits, but\n"); + log(" some solvers are faster with bwd hints, or even both -bwd and -fwd.)\n"); + log("\n"); + log(" -nop\n"); + log(" Don't insert hint assumptions into the combined module.\n"); + log(" (This should not provide any speedup over the original design, but\n"); + log(" strangely sometimes it does.)\n"); + log("\n"); + log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) YS_OVERRIDE { + opts_t opts; Module *module = nullptr; Cell *gold_cell = nullptr; Cell *gate_cell = nullptr; @@ -230,6 +261,18 @@ struct FmcombinePass : public Pass { // filename = args[++argidx]; // continue; // } + if (args[argidx] == "-fwd") { + opts.fwd = true; + continue; + } + if (args[argidx] == "-bwd") { + opts.bwd = true; + continue; + } + if (args[argidx] == "-nop") { + opts.nop = true; + continue; + } break; } if (argidx+2 == args.size()) @@ -262,6 +305,12 @@ struct FmcombinePass : public Pass { } // extra_args(args, argidx, design); + if (opts.nop && (opts.fwd || opts.bwd)) + log_cmd_error("Option -nop can not be combined with -fwd and/or -bwd.\n"); + + if (!opts.nop && !opts.fwd && !opts.bwd) + opts.fwd = true; + if (gold_cell->type != gate_cell->type) log_cmd_error("Types of gold and gate cells do not match.\n"); if (!gold_cell->parameters.empty()) @@ -269,7 +318,7 @@ struct FmcombinePass : public Pass { if (!gate_cell->parameters.empty()) log_cmd_error("Gold cell has unresolved instance parameters.\n"); - FmcombineWorker worker(design, gold_cell->type); + FmcombineWorker worker(design, gold_cell->type, opts); worker.generate(); IdString combined_cell_name = module->uniquify(stringf("\\%s_%s", log_id(gold_cell), log_id(gate_cell))); -- cgit v1.2.3 From aa65d3fe65bd45994f8cb053daef3a5e52b31cd3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 16 Mar 2019 00:55:46 +0100 Subject: Improve mix of src/wire/wirebit coverage in "mutate -list" Signed-off-by: Clifford Wolf --- passes/sat/mutate.cc | 113 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 84 insertions(+), 29 deletions(-) diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 4c103dcd5..9621d2855 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -46,7 +46,7 @@ struct mutate_opts_t { IdString ctrl_name; int ctrl_width = -1, ctrl_value = -1; - int pick_cover_prcnt = 50; + int pick_cover_prcnt = 80; int weight_cover = 500; @@ -133,25 +133,69 @@ struct xs128_t } }; +struct coverdb_t +{ + dict src_db; + dict, int> wire_db; + dict, int> wirebit_db; + + void insert(const mutate_t &m) { + if (!m.wire.empty()) { + wire_db[tuple(m.module, m.wire)] = 0; + wirebit_db[tuple(m.module, m.wire, m.wirebit)] = 0; + } + for (auto &s : m.src) { + src_db[s] = 0; + } + } + + void update(const mutate_t &m) { + if (!m.wire.empty()) { + wire_db.at(tuple(m.module, m.wire))++; + wirebit_db.at(tuple(m.module, m.wire, m.wirebit))++; + } + for (auto &s : m.src) { + src_db.at(s)++; + } + } + + int score(const mutate_t &m) { + int this_score = m.src.empty() ? 0 : 1; + if (!m.wire.empty()) { + this_score += wire_db.at(tuple(m.module, m.wire)) ? 0 : 5; + this_score += wirebit_db.at(tuple(m.module, m.wire, m.wirebit)) ? 0 : 1; + } + for (auto &s : m.src) { + this_score += src_db.at(s) ? 0 : 5; + } + return this_score; + } +}; + struct mutate_queue_t { pool db; - mutate_t *pick(xs128_t &rng, dict &coverdb, const mutate_opts_t &opts) { + mutate_t *pick(xs128_t &rng, coverdb_t &coverdb, const mutate_opts_t &opts) { mutate_t *m = nullptr; if (rng(100) < opts.pick_cover_prcnt) { - vector candidates; + vector candidates, rmqueue; + int best_score = -1; for (auto p : db) { - if (p->used || p->src.empty()) + if (p->used) { + rmqueue.push_back(p); continue; - bool is_covered = false; - for (auto &s : p->src) { - if (coverdb.at(s)) - is_covered = true; } - if (!is_covered) + int this_score = coverdb.score(*p); + if (this_score > best_score) { + best_score = this_score; + candidates.clear(); + } + if (best_score == this_score) candidates.push_back(p); } + for (auto p : rmqueue) + db.erase(p); if (!candidates.empty()) m = candidates[rng(GetSize(candidates))]; } @@ -167,11 +211,6 @@ struct mutate_queue_t } } } - if (m != nullptr) { - m->used = true; - for (auto &s : m->src) - coverdb[s]++; - } return m; } @@ -185,7 +224,7 @@ struct mutate_chain_queue_t { dict db; - mutate_t *pick(xs128_t &rng, dict &coverdb, const mutate_opts_t &opts) { + mutate_t *pick(xs128_t &rng, coverdb_t &coverdb, const mutate_opts_t &opts) { while (!db.empty()) { int i = rng(GetSize(db)); auto it = db.element(i); @@ -208,7 +247,7 @@ struct mutate_once_queue_t { dict db; - mutate_t *pick(xs128_t &rng, dict &coverdb, const mutate_opts_t &opts) { + mutate_t *pick(xs128_t &rng, coverdb_t &coverdb, const mutate_opts_t &opts) { while (!db.empty()) { int i = rng(GetSize(db)); auto it = db.element(i); @@ -229,7 +268,7 @@ struct mutate_once_queue_t void database_reduce(std::vector &database, const mutate_opts_t &opts, int N, xs128_t &rng) { std::vector new_database; - dict coverdb; + coverdb_t coverdb; int total_weight = opts.weight_cover + opts.weight_pq_w + opts.weight_pq_b + opts.weight_pq_c + opts.weight_pq_s; total_weight += opts.weight_pq_mw + opts.weight_pq_mb + opts.weight_pq_mc + opts.weight_pq_ms; @@ -249,6 +288,8 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, for (auto &m : database) { + coverdb.insert(m); + if (!m.wire.empty()) { primary_queue_wire.add(&m, tuple(m.module, m.wire)); primary_queue_bit.add(&m, tuple(m.module, m.wire, m.wirebit)); @@ -260,7 +301,6 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, primary_queue_module_cell.add(&m, m.module, m.cell); for (auto &s : m.src) { - coverdb[s] = 0; primary_queue_src.add(&m, s); primary_queue_module_src.add(&m, m.module, s); } @@ -284,8 +324,8 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, continue; int this_score = -1; for (auto &s : m.src) { - if (this_score == -1 || this_score > coverdb.at(s)) - this_score = coverdb.at(s); + if (this_score == -1 || this_score > coverdb.src_db.at(s)) + this_score = coverdb.src_db.at(s); } log_assert(this_score != -1); if (best_cover_score == -1 || this_score < best_cover_score) { @@ -314,8 +354,8 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, int this_score = -1; for (auto &s : p->src) { - if (this_score == -1 || this_score > coverdb.at(s)) - this_score = coverdb.at(s); + if (this_score == -1 || this_score > coverdb.src_db.at(s)) + this_score = coverdb.src_db.at(s); } if (this_score != best_cover_score) @@ -327,8 +367,7 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, if (m != nullptr) { m->used = true; - for (auto &s : m->src) - coverdb[s]++; + coverdb.update(*m); new_database.push_back(*m); break; } @@ -340,8 +379,11 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, k -= __wght; \ if (k < 0) { \ mutate_t *m = __queue.pick(rng, coverdb, opts); \ - if (m != nullptr) \ + if (m != nullptr) { \ + m->used = true; \ + coverdb.update(*m); \ new_database.push_back(*m); \ + }; \ continue; \ } @@ -359,12 +401,25 @@ void database_reduce(std::vector &database, const mutate_opts_t &opts, std::swap(new_database, database); - int covered_cnt = 0; - for (auto &it : coverdb) + int covered_src_cnt = 0; + int covered_wire_cnt = 0; + int covered_wirebit_cnt = 0; + + for (auto &it : coverdb.src_db) + if (it.second) + covered_src_cnt++; + + for (auto &it : coverdb.wire_db) + if (it.second) + covered_wire_cnt++; + + for (auto &it : coverdb.wirebit_db) if (it.second) - covered_cnt++; + covered_wirebit_cnt++; - log("Covered %d/%d src attributes (%.2f%%).\n", covered_cnt, GetSize(coverdb), 100.0 * covered_cnt / GetSize(coverdb)); + log("Covered %d/%d src attributes (%.2f%%).\n", covered_src_cnt, GetSize(coverdb.src_db), 100.0 * covered_src_cnt / GetSize(coverdb.src_db)); + log("Covered %d/%d wires (%.2f%%).\n", covered_wire_cnt, GetSize(coverdb.wire_db), 100.0 * covered_wire_cnt / GetSize(coverdb.wire_db)); + log("Covered %d/%d wire bits (%.2f%%).\n", covered_wirebit_cnt, GetSize(coverdb.wirebit_db), 100.0 * covered_wirebit_cnt / GetSize(coverdb.wirebit_db)); } void mutate_list(Design *design, const mutate_opts_t &opts, const string &filename, int N) -- cgit v1.2.3 From a71c38f163a1972b2da8883b7043b25dd8e2662d Mon Sep 17 00:00:00 2001 From: Felix Vietmeyer Date: Sat, 16 Mar 2019 06:20:59 -0600 Subject: Add note about test requirements in README --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 9bac468a7..c5cd47707 100644 --- a/README.md +++ b/README.md @@ -105,12 +105,15 @@ Makefile. To build Yosys simply type 'make' in this directory. $ make - $ make test $ sudo make install Note that this also downloads, builds and installs ABC (using yosys-abc as executable name). +Tests are located in the tests subdirectory and can be executed using the test target. Note that you need gawk as well as a recent version of iverilog (i.e. build from git). Then, execute tests via: + + $ make test + Getting Started =============== -- cgit v1.2.3 From 6aae502a3647b50e3f5c0f7d02e8056acf080920 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 17 Mar 2019 12:44:23 +0100 Subject: Update issue template Signed-off-by: Clifford Wolf --- .github/issue_template.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/issue_template.md b/.github/issue_template.md index 4563a71de..22ad6f839 100644 --- a/.github/issue_template.md +++ b/.github/issue_template.md @@ -4,6 +4,14 @@ all necessary source files. (You can simply drag&drop a .zip file into the issue editor.)* +Also, make sure that the issue is actually reproducable in current git +master of Yosys. + +Please do not waste our time with issues that don't contain sufficient +information to reproduce the issue easily. We will simply close those issues. + +Contact https://www.symbioticeda.com/ if you need commercial support for Yosys. + ## Expected behavior *Please describe the behavior you would have expected from the tool.* -- cgit v1.2.3 From 90bce0415622a3d7a64bca5914a0fb3abdd3cc5c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 17 Mar 2019 12:53:47 +0100 Subject: Update issue template Signed-off-by: Clifford Wolf --- .github/issue_template.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/issue_template.md b/.github/issue_template.md index 22ad6f839..5a0723c3e 100644 --- a/.github/issue_template.md +++ b/.github/issue_template.md @@ -7,8 +7,11 @@ the issue editor.)* Also, make sure that the issue is actually reproducable in current git master of Yosys. -Please do not waste our time with issues that don't contain sufficient -information to reproduce the issue easily. We will simply close those issues. +See https://stackoverflow.com/help/mcve for some information on how to +create a Minimal, Complete, and Verifiable example (MCVE). + +Please do not waste our time with issues that lack sufficient information +to reproduce the issue easily. We will simply close those issues. Contact https://www.symbioticeda.com/ if you need commercial support for Yosys. @@ -19,6 +22,3 @@ Contact https://www.symbioticeda.com/ if you need commercial support for Yosys. ## Actual behavior *Please describe how the behavior you see differs from the expected behavior.* - -**Important Note:** Nobody will be able to help you and/or fix the issue if you -do not provide sufficient information for reproducing the problem. -- cgit v1.2.3 From a5f4b836376e1457847da4946c1e12d2d41dc4f4 Mon Sep 17 00:00:00 2001 From: Zachary Snow Date: Mon, 18 Mar 2019 20:34:21 -0400 Subject: fix local name resolution in prefix constructs --- frontends/ast/simplify.cc | 6 ++++- tests/simple/generate.v | 56 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 61 insertions(+), 1 deletion(-) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 1c9932ee0..d525c6b8a 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -2863,7 +2863,11 @@ void AstNode::expand_genblock(std::string index_var, std::string prefix, std::ma for (size_t i = 0; i < children.size(); i++) { AstNode *child = children[i]; - if (child->type != AST_FUNCTION && child->type != AST_TASK && child->type != AST_PREFIX) + // AST_PREFIX member names should not be prefixed; a nested AST_PREFIX + // still needs to recursed-into + if (type == AST_PREFIX && i == 1 && child->type == AST_IDENTIFIER) + continue; + if (child->type != AST_FUNCTION && child->type != AST_TASK) child->expand_genblock(index_var, prefix, name_map); } diff --git a/tests/simple/generate.v b/tests/simple/generate.v index 24eb4462c..3c55682cb 100644 --- a/tests/simple/generate.v +++ b/tests/simple/generate.v @@ -90,5 +90,61 @@ generate endcase end endgenerate +endmodule + +// ------------------------------------------ + +module gen_test4(a, b); + +input [3:0] a; +output [3:0] b; + +genvar i; +generate + for (i=0; i < 3; i=i+1) begin : foo + localparam PREV = i - 1; + wire temp; + if (i == 0) + assign temp = a[0]; + else + assign temp = foo[PREV].temp & a[i]; + assign b[i] = temp; + end +endgenerate +endmodule + +// ------------------------------------------ + +module gen_test5(input_bits, out); + +parameter WIDTH = 256; +parameter CHUNK = 4; +input [WIDTH-1:0] input_bits; +output out; + +genvar step, i, j; +generate + for (step = 1; step <= WIDTH; step = step * CHUNK) begin : steps + localparam PREV = step / CHUNK; + localparam DIM = WIDTH / step; + for (i = 0; i < DIM; i = i + 1) begin : outer + localparam LAST_START = i * CHUNK; + for (j = 0; j < CHUNK; j = j + 1) begin : inner + wire temp; + if (step == 1) + assign temp = input_bits[i]; + else if (j == 0) + assign temp = steps[PREV].outer[LAST_START].val; + else + assign temp + = steps[step].outer[i].inner[j-1].temp + & steps[PREV].outer[LAST_START + j].val; + end + wire val; + assign val = steps[step].outer[i].inner[CHUNK - 1].temp; + end + end +endgenerate +assign out = steps[WIDTH].outer[0].val; endmodule -- cgit v1.2.3 From 3e89cf68bdc4e9eeb55bd9450121f421bcdc554a Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 19 Mar 2019 08:52:06 -0700 Subject: Add author name --- frontends/aiger/aigerparse.h | 1 + 1 file changed, 1 insertion(+) diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h index 39a77bd93..c49cd152d 100644 --- a/frontends/aiger/aigerparse.h +++ b/frontends/aiger/aigerparse.h @@ -2,6 +2,7 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf + * Eddie Hung * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above -- cgit v1.2.3 From fe1fb1336b44bb073125aa4b42f12baa316e9fea Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 19 Mar 2019 20:29:54 +0100 Subject: Add Xilinx negedge FFs to synth_xilinx dffinit call, fixes #873 Signed-off-by: Clifford Wolf --- techlibs/xilinx/synth_xilinx.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc index accc7a259..805ae8e6e 100644 --- a/techlibs/xilinx/synth_xilinx.cc +++ b/techlibs/xilinx/synth_xilinx.cc @@ -120,7 +120,8 @@ struct SynthXilinxPass : public Pass log("\n"); log(" map_cells:\n"); log(" techmap -map +/xilinx/cells_map.v\n"); - log(" dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT -ff FDSE Q INIT\n"); + log(" dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT -ff FDSE Q INIT \\\n"); + log(" -ff FDRE_1 Q INIT -ff FDCE_1 Q INIT -ff FDPE_1 Q INIT -ff FDSE_1 Q INIT\n"); log(" clean\n"); log("\n"); log(" check:\n"); @@ -274,7 +275,8 @@ struct SynthXilinxPass : public Pass if (check_label(active, run_from, run_to, "map_cells")) { Pass::call(design, "techmap -map +/xilinx/cells_map.v"); - Pass::call(design, "dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT -ff FDSE Q INIT"); + Pass::call(design, "dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT -ff FDSE Q INIT " + "-ff FDRE_1 Q INIT -ff FDCE_1 Q INIT -ff FDPE_1 Q INIT -ff FDSE_1 Q INIT"); Pass::call(design, "clean"); } -- cgit v1.2.3