Merge upstream yosys

This commit is contained in:
Akash Levy 2025-04-21 17:36:24 -07:00
commit 5f5ed1b29e
41 changed files with 920 additions and 237 deletions

View File

@ -25,7 +25,8 @@ jobs:
steps:
- uses: actions/checkout@v4
with:
submodules: true
submodules: true
persist-credentials: false
- name: Build
run: make vcxsrc YOSYS_VER=latest
- uses: actions/upload-artifact@v4
@ -59,7 +60,8 @@ jobs:
steps:
- uses: actions/checkout@v4
with:
submodules: true
submodules: true
persist-credentials: false
- name: Build
run: |
WASI_SDK=wasi-sdk-19.0
@ -95,6 +97,7 @@ jobs:
- uses: actions/checkout@v4
with:
submodules: true
persist-credentials: false
- uses: cachix/install-nix-action@v26
with:
install_url: https://releases.nixos.org/nix/nix-2.18.1/install

View File

@ -20,7 +20,7 @@ jobs:
# only run on push *or* pull_request, not both
concurrent_skipping: ${{ env.docs_export && 'never' || 'same_content_newer'}}
- id: docs_var
run: echo "docs_export=${{ env.docs_export }}" >> $GITHUB_OUTPUT
run: echo "docs_export=${docs_export}" >> $GITHUB_OUTPUT
prepare-docs:
# docs builds are needed for anything on main, any tagged versions, and any tag
@ -47,12 +47,12 @@ jobs:
echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j${{ env.procs }} ENABLE_LTO=1
make -j$procs ENABLE_LTO=1
- name: Prepare docs
shell: bash
run:
make docs/prep -j${{ env.procs }} TARGETS= EXTRA_TARGETS=
make docs/prep -j$procs TARGETS= EXTRA_TARGETS=
- name: Upload artifact
uses: actions/upload-artifact@v4
@ -72,7 +72,7 @@ jobs:
- name: Test build docs
shell: bash
run: |
make -C docs html -j${{ env.procs }} TARGETS= EXTRA_TARGETS=
make -C docs html -j$procs TARGETS= EXTRA_TARGETS=
- name: Trigger RTDs build
if: ${{ needs.check_docs_rebuild.outputs.docs_export == 'true' }}

View File

@ -123,7 +123,7 @@ jobs:
uses: actions/cache@v4
with:
path: .local/
key: ${{ matrix.os }}-${{ env.IVERILOG_GIT }}
key: ${{ matrix.os }}-${IVERILOG_GIT}
- name: Build iverilog
if: steps.cache-iverilog.outputs.cache-hit != 'true'
@ -206,3 +206,46 @@ jobs:
shell: bash
run: |
make -C docs test -j${{ env.procs }} SMALL=0 ENABLE_ABC=1 ENABLE_PLUGINS=1 ENABLE_PYOSYS=0 ENABLE_CCACHE=0 ENABLE_EDITLINE=0
test-docs-build:
name: Try build docs
runs-on: [self-hosted, linux, x64, fast]
needs: [pre_docs_job]
if: needs.pre_docs_job.outputs.should_skip != 'true'
strategy:
matrix:
docs-target: [html, latexpdf]
fail-fast: false
steps:
- name: Checkout Yosys
uses: actions/checkout@v4
with:
submodules: true
ssh-key: ${{ secrets.SSH_PRIVATE_KEY }}
- name: Runtime environment
run: |
echo "procs=$(nproc)" >> $GITHUB_ENV
- name: Build Yosys
run: |
make config-clang
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: Install doc prereqs
shell: bash
run: |
make docs/reqs
- name: Build docs
shell: bash
run: |
make docs DOC_TARGET=${{ matrix.docs-target }} -j$procs
- name: Store docs build artifact
uses: actions/upload-artifact@v4
with:
name: docs-build-${{ matrix.docs-target }}
path: docs/build/
retention-days: 7

View File

@ -45,6 +45,7 @@ jobs:
uses: actions/checkout@v4
with:
submodules: true
persist-credentials: false
- name: Setup environment
uses: ./.github/actions/setup-build-env

View File

@ -40,7 +40,7 @@ jobs:
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 1" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
echo "ENABLE_FUNCTIONAL_TESTS := 1" >> Makefile.conf
make -j${{ env.procs }} ENABLE_LTO=1
make -j$procs ENABLE_LTO=1
- name: Install Yosys
run: |
@ -51,6 +51,7 @@ jobs:
with:
repository: 'YosysHQ/sby'
path: 'sby'
persist-credentials: false
- name: Build SBY
run: |
@ -58,7 +59,7 @@ jobs:
- name: Run Yosys tests
run: |
make -j${{ env.procs }} test
make -j$procs test
- name: Run Verific specific Yosys tests
run: |

View File

@ -10,6 +10,8 @@ jobs:
steps:
- name: Checkout repository
uses: actions/checkout@v4
with:
persist-credentials: false
- name: Install Nix
uses: DeterminateSystems/nix-installer-action@main
- name: Update flake.lock

View File

@ -14,6 +14,7 @@ jobs:
with:
fetch-depth: 0
submodules: true
persist-credentials: false
- name: Take last commit
id: log
run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT

View File

@ -1,6 +1,10 @@
name: Build Wheels for PyPI
# run every Sunday at 10 AM
on:
workflow_dispatch:
schedule:
- cron: '0 10 * * 0'
jobs:
build_wheels:
@ -14,16 +18,12 @@ jobs:
runner: "ubuntu-22.04",
archs: "x86_64",
},
## Aarch64 is disabled for now: GitHub is committing to EOY
## for free aarch64 runners for open-source projects and
## emulation times out:
## https://github.com/orgs/community/discussions/19197#discussioncomment-10550689
# {
# name: "Ubuntu 22.04",
# family: "linux",
# runner: "ubuntu-22.04",
# archs: "aarch64",
# },
{
name: "Ubuntu 22.04",
family: "linux",
runner: "ubuntu-22.04-arm",
archs: "aarch64",
},
{
name: "macOS 13",
family: "macos",
@ -53,6 +53,7 @@ jobs:
with:
fetch-depth: 0
submodules: true
persist-credentials: false
- if: ${{ matrix.os.family == 'linux' }}
name: "[Linux] Set up QEMU"
uses: docker/setup-qemu-action@v3

View File

@ -112,6 +112,7 @@ LIBS := $(LIBS) -lstdc++ -lm
PLUGIN_LINKFLAGS :=
PLUGIN_LIBS :=
EXE_LINKFLAGS :=
EXE_LIBS :=
ifeq ($(OS), MINGW)
EXE_LINKFLAGS := -Wl,--export-all-symbols -Wl,--out-implib,libyosys_exe.a
PLUGIN_LINKFLAGS += -L"$(LIBDIR)"
@ -175,7 +176,7 @@ ifeq ($(OS), Haiku)
CXXFLAGS += -D_DEFAULT_SOURCE
endif
YOSYS_VER := 0.52+10
YOSYS_VER := 0.52+75
YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2)
YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'.' -f3)
@ -225,11 +226,11 @@ PYTHON_VERSION_TESTCODE := "import sys;t='{v[0]}.{v[1]}'.format(v=list(sys.versi
PYTHON_VERSION := $(shell $(PYTHON_EXECUTABLE) -c ""$(PYTHON_VERSION_TESTCODE)"")
PYTHON_MAJOR_VERSION := $(shell echo $(PYTHON_VERSION) | cut -f1 -d.)
ENABLE_PYTHON_CONFIG_EMBED ?= $(shell $(PYTHON_EXECUTABLE)-config --embed --libs > /dev/null && echo 1)
ifeq ($(ENABLE_PYTHON_CONFIG_EMBED),1)
PYTHON_CONFIG := $(PYTHON_EXECUTABLE)-config --embed
else
PYTHON_CONFIG := $(PYTHON_EXECUTABLE)-config
PYTHON_CONFIG_FOR_EXE := $(PYTHON_CONFIG)
PYTHON_CONFIG_EMBED_AVAILABLE ?= $(shell $(PYTHON_EXECUTABLE)-config --embed --libs > /dev/null && echo 1)
ifeq ($(PYTHON_CONFIG_EMBED_AVAILABLE),1)
PYTHON_CONFIG_FOR_EXE := $(PYTHON_CONFIG) --embed
endif
PYTHON_DESTDIR := $(shell $(PYTHON_EXECUTABLE) -c "import site; print(site.getsitepackages()[-1]);")
@ -362,10 +363,11 @@ ifeq ($(ENABLE_PYOSYS),1)
# python-config --ldflags includes -l and -L, but LINKFLAGS is only -L
LINKFLAGS += $(filter-out -l%,$(shell $(PYTHON_CONFIG) --ldflags))
LIBS += $(shell $(PYTHON_CONFIG) --libs)
EXE_LIBS += $(filter-out $(LIBS),$(shell $(PYTHON_CONFIG_FOR_EXE) --libs))
CXXFLAGS += $(shell $(PYTHON_CONFIG) --includes) -DWITH_PYTHON
# Detect name of boost_python library. Some distros use boost_python-py<version>, other boost_python<version>, some only use the major version number, some a concatenation of major and minor version numbers
CHECK_BOOST_PYTHON = (echo "int main(int argc, char ** argv) {return 0;}" | $(CXX) -xc -o /dev/null $(LINKFLAGS) $(LIBS) -l$(1) - > /dev/null 2>&1 && echo "-l$(1)")
CHECK_BOOST_PYTHON = (echo "int main(int argc, char ** argv) {return 0;}" | $(CXX) -xc -o /dev/null $(LINKFLAGS) $(EXE_LIBS) $(LIBS) -l$(1) - > /dev/null 2>&1 && echo "-l$(1)")
BOOST_PYTHON_LIB ?= $(shell \
$(call CHECK_BOOST_PYTHON,boost_python-py$(subst .,,$(PYTHON_VERSION))) || \
$(call CHECK_BOOST_PYTHON,boost_python-py$(PYTHON_MAJOR_VERSION)) || \
@ -790,7 +792,7 @@ share: $(EXTRA_TARGETS)
@echo ""
$(PROGRAM_PREFIX)yosys$(EXE): $(OBJS)
$(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(LIBS) $(LIBS_VERIFIC)
$(P) $(CXX) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LINKFLAGS) $(LINKFLAGS) $(OBJS) $(EXE_LIBS) $(LIBS) $(LIBS_VERIFIC)
libyosys.so: $(filter-out kernel/driver.o,$(OBJS))
ifeq ($(OS), Darwin)
@ -1024,20 +1026,6 @@ unit-test: libyosys.so
clean-unit-test:
@$(MAKE) -C $(UNITESTPATH) clean
ifeq ($(ENABLE_PYOSYS),1)
wheel: $(TARGETS) $(EXTRA_TARGETS)
$(PYTHON_EXECUTABLE) -m pip wheel .
install-wheel: wheel
$(PYTHON_EXECUTABLE) -m pip install pyosys-$(YOSYS_VER)-*.whl --force-reinstall
else
wheel:
$(error Pyosys is not enabled. Set ENABLE_PYOSYS=1 to enable it.)
install-wheel:
$(error Pyosys is not enabled. Set ENABLE_PYOSYS=1 to enable it.)
endif
install: $(TARGETS) $(EXTRA_TARGETS)
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR)
$(INSTALL_SUDO) cp $(filter-out libyosys.so,$(TARGETS)) $(DESTDIR)$(BINDIR)
@ -1057,7 +1045,13 @@ ifeq ($(ENABLE_LIBYOSYS),1)
$(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(LIBDIR)/
$(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(LIBDIR)/libyosys.so
ifeq ($(ENABLE_PYOSYS),1)
$(INSTALL_SUDO) @$(MAKE) install-wheel
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
$(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so
$(INSTALL_SUDO) cp -r share $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
ifeq ($(ENABLE_ABC),1)
$(INSTALL_SUDO) cp yosys-abc $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/yosys-abc
endif
$(INSTALL_SUDO) cp misc/__init__.py $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/
endif
endif
ifeq ($(ENABLE_PLUGINS),1)
@ -1073,7 +1067,9 @@ uninstall:
ifeq ($(ENABLE_LIBYOSYS),1)
$(INSTALL_SUDO) rm -vf $(DESTDIR)$(LIBDIR)/libyosys.so
ifeq ($(ENABLE_PYOSYS),1)
$(INSTALL_SUDO) $(PYTHON_EXECUTABLE) -m pip uninstall -y pyosys
$(INSTALL_SUDO) rm -vf $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so
$(INSTALL_SUDO) rm -vf $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/__init__.py
$(INSTALL_SUDO) rmdir $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys
endif
endif

View File

@ -200,7 +200,7 @@ bool is_extending_cell(RTLIL::IdString type)
bool is_inlinable_cell(RTLIL::IdString type)
{
return is_unary_cell(type) || is_binary_cell(type) || type.in(
ID($mux), ID($concat), ID($slice), ID($pmux), ID($bmux), ID($demux));
ID($mux), ID($concat), ID($slice), ID($pmux), ID($bmux), ID($demux), ID($bwmux));
}
bool is_ff_cell(RTLIL::IdString type)
@ -1198,6 +1198,14 @@ struct CxxrtlWorker {
f << ">(";
dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
f << ").val()";
// Bitwise muxes
} else if (cell->type == ID($bwmux)) {
dump_sigspec_rhs(cell->getPort(ID::A), for_debug);
f << ".bwmux(";
dump_sigspec_rhs(cell->getPort(ID::B), for_debug);
f << ",";
dump_sigspec_rhs(cell->getPort(ID::S), for_debug);
f << ").val()";
// Demuxes
} else if (cell->type == ID($demux)) {
dump_sigspec_rhs(cell->getPort(ID::A), for_debug);

View File

@ -498,6 +498,11 @@ struct value : public expr_base<value<Bits>> {
return result;
}
CXXRTL_ALWAYS_INLINE
value<Bits> bwmux(const value<Bits> &b, const value<Bits> &s) const {
return (bit_and(s.bit_not())).bit_or(b.bit_and(s));
}
template<size_t ResultBits, size_t SelBits>
value<ResultBits> demux(const value<SelBits> &sel) const {
static_assert(Bits << SelBits == ResultBits, "invalid sizes used in demux()");

View File

@ -0,0 +1,114 @@
Dataflow tracking
-------------------
Yosys can be used to answer questions such as "can this signal affect this other
signal?" via its *dataflow tracking* support. For this, four special cells,
`$get_tag`, `$set_tag`, `$overwrite_tag` and `$original_tag` are inserted into
the design (e.g. by a custom Yosys pass) and then the `dft_tag` is run, which
converts these cells into ordinary logic. Typically, one would then use `SBY`_
to prove assertions involving these cells.
.. _SBY: https://yosyshq.readthedocs.io/projects/sby
Ordinarily in Yosys, the state of a bit is simply ``0`` or ``1`` (or one of the
special values, ``z`` and ``x``). During dataflow tracking they are augmented
with a set of tags. For example, the state of a bit could be ``0`` and the set
of tags ``"KEY"`` and ``"OVERFLOW"``.
In addition to their usual operations on the logical bits, Yosys operations must
now also process the status of the tags. For this, tags are simply *forwarded*
or *propagated* (i.e. copied) from inputs to outputs, according to the following
general rule:
A tag is forwarded from an input to an output if the input can affect the
output, for that particular state of all other inputs.
For example, XOR, AND and OR cells propagate tags as follows:
#. XOR simply forwards all tags from its inputs to its output, because inputs to
XOR can always affect the output.
#. AND forwards tags on a given input only if the other input is ``1``. Because
if one input is ``0``, the other input can never affect the output.
#. Similarly, OR forwards tags only if the other input is ``0``.
There are two exceptions to this rule:
#. In general, propagation is only determined approximately. For example, unless
the ``dft_tag`` code knows about a cell, it simply assumes the worst-case
behaviour that all inputs can affect all outputs. Further, the code also does
not consider that, when a signal affects multiple inputs of a cell, the
resulting simultaneous changes of the inputs can cancel each other out, for
example ``A ^ A`` or ``A ^ (B ^ A)`` is independent of ``A``, but its tags
would be propagated nonetheless.
#. If tag groups are used, the rules are modified (see below).
Because of this propagation behaviour, we can answer questions about what
signals are affected by a certain signal, by injecting a tag at that point in
the circuit, and observing where the tag is visible.
Example use cases
~~~~~~~~~~~~~~~~~~
As an example use case, consider a cryptographic processor which is not supposed
to expose its secret keys to the outside world. We can tag all key bits with the
``"KEY"`` tag and use `SBY`_ to formally verify that no external signal ever
carries the ``"KEY"`` tag, meaning that key information is not visible to the
outside. As a caveat, we have to manually clear the ``"KEY"`` tag during
cryptographic operations, as proving that the cryptographic operations
themselves do not leak key information is beyond the ability of Yosys. However
we can still easily detect, if e.g. an engineer forgot to remove debugging code
that allows reading back key data.
As a different use case, we can modify all adders in the design to set the
``"OVERFLOW"`` tag on their output bits, if the addition overflowed, and then
add asserts to all flip-flop inputs and output signals that they do not carry
the ``"OVERFLOW"`` tag, i.e. that the results of overflowed additions never
affect system state. Note that in this particular example we use the ability of
tag insertion to be conditional on logic, in this case the overflow condition of
an adder.
Semantics of dataflow tracking cells
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
``$set_tag`` has inputs ``A``, ``SET``, ``CLR``, an output ``Y`` and a string
parameter ``TAG``. The logic value of ``A`` and all tags other than the one
named by the ``TAG`` parameter are simply copied to ``Y``. If ``SET`` is ``1``,
then the named tag is added to ``Y``. Otherwise, if ``CLR`` is ``1``, then the
named tag is removed. Otherwise, the tag is unchanged, i.e. it is present in
``Y`` if it is present in ``A``.
``$get_tag`` has an input ``A`` and an output ``Y`` and a string parameter
``TAG``. ``$get_tag`` inspects ``A`` for the presence or absence of a tag of the
given name and sets ``Y`` to ``1`` if the tag is present. The logical value of
``A`` is completely ignored.
``$overwrite_tag`` functions like ``$set_tag``, but lacks the ``Y`` output.
Instead of providing a modified version of the input signal, it modifies the
signal ``A`` "in-place", i.e. if a signal is input to ``$overwrite_tag``, that
is equivalent to interposing a ``$set_tag`` between its driver and all cells it
is connected to. The main purpose of ``$overwrite_tag`` is adding tags to
signals produced within a module that cannot or should not be modified itself.
``$original_tag`` functions identically to ``$get_tag``, but ignores
``$overwrite_tag``, i.e. when converting the ``$overwrite_tag`` to ``$set_tag``
as described above, it is equivalent to inserting the ``$get_tag`` *before* the
``$set_tag``.
Tag groups
~~~~~~~~~~~~~~
Tag groups are an advanced feature that modify the propagation rule discussed
above. To use tag groups, simply name tags according to the schema
``"group:name"``. For example, ``"key:0"``, ``"key:a"``, ``"key:b"`` would be
three tags in the ``"key"`` group.
The propagation rule is then amended by
Inputs cannot block the propagation of each other's tags for tags of the same
group.
For example, an AND gate will propagate a given tag on one input, if the other
input is either 1 or carries a tag of the same group. So if one input is ``0,
"key:a"`` and the other is ``0, "key:b"`` the result would be ``0, "key:a",
"key:b"``, rather than simply ``0``. Note that if we add an unrelated
``"overflow"`` tag to the first input, it would still not be propagated.

View File

@ -12,5 +12,6 @@ More scripting
selections
interactive_investigation
model_checking
data_flow_tracking
.. troubleshooting

View File

@ -315,7 +315,7 @@ struct ConstEval
Macc macc;
macc.from_cell(cell);
for (auto &port : macc.ports) {
for (auto &port : macc.terms) {
if (!eval(port.in_a, undef, cell))
return false;
if (!eval(port.in_b, undef, cell))

View File

@ -1,4 +1,5 @@
#include "kernel/cost.h"
#include "kernel/macc.h"
USING_YOSYS_NAMESPACE
@ -155,6 +156,9 @@ unsigned int CellCosts::get(RTLIL::Cell *cell)
log_assert(cell->hasPort(ID::Q) && "Weird flip flop");
log_debug("%s is ff\n", cell->name.c_str());
return cell->getParam(ID::WIDTH).as_int();
} else if (cell->type.in(ID($mem), ID($mem_v2))) {
log_debug("%s is mem\n", cell->name.c_str());
return cell->getParam(ID::WIDTH).as_int() * cell->getParam(ID::SIZE).as_int();
} else if (y_coef(cell->type)) {
// linear with Y_WIDTH or WIDTH
log_assert((cell->hasParam(ID::Y_WIDTH) || cell->hasParam(ID::WIDTH)) && "Unknown width");
@ -180,6 +184,22 @@ unsigned int CellCosts::get(RTLIL::Cell *cell)
unsigned int coef = cell->type == ID($mul) ? 3 : 5;
log_debug("%s coef*(sum**2) %d * %d\n", cell->name.c_str(), coef, sum * sum);
return coef * sum * sum;
} else if (cell->type.in(ID($macc), ID($macc_v2))) {
// quadratic per term
unsigned int cost_sum = 0;
Macc macc;
macc.from_cell(cell);
unsigned int y_width = cell->getParam(ID::Y_WIDTH).as_int();
for (auto &term: macc.terms) {
if (term.in_b.empty()) {
// neglect addends
continue;
}
unsigned a_width = term.in_a.size(), b_width = term.in_b.size();
unsigned int sum = a_width + b_width + std::min(y_width, a_width + b_width);
cost_sum += 3 * sum * sum;
}
return cost_sum;
} else if (cell->type == ID($lut)) {
int width = cell->getParam(ID::WIDTH).as_int();
unsigned int cost = 1U << (unsigned int)width;
@ -198,7 +218,7 @@ unsigned int CellCosts::get(RTLIL::Cell *cell)
log_debug("%s is mem\n", cell->name.c_str());
return 1;
}
// TODO: $fsm $macc
// TODO: $fsm
// ignored: $pow
log_warning("Can't determine cost of %s cell (%d parameters).\n", log_id(cell->type), GetSize(cell->parameters));

View File

@ -26,18 +26,18 @@ YOSYS_NAMESPACE_BEGIN
struct Macc
{
struct port_t {
struct term_t {
RTLIL::SigSpec in_a, in_b;
bool is_signed, do_subtract;
};
std::vector<port_t> ports;
std::vector<term_t> terms;
void optimize(int width)
{
std::vector<port_t> new_ports;
std::vector<term_t> new_terms;
RTLIL::Const off(0, width);
for (auto &port : ports)
for (auto &port : terms)
{
if (GetSize(port.in_a) == 0 && GetSize(port.in_b) == 0)
continue;
@ -68,25 +68,25 @@ struct Macc
port.in_b.remove(GetSize(port.in_b)-1);
}
new_ports.push_back(port);
new_terms.push_back(port);
}
if (off.as_bool()) {
port_t port;
term_t port;
port.in_a = off;
port.is_signed = false;
port.do_subtract = false;
new_ports.push_back(port);
new_terms.push_back(port);
}
new_ports.swap(ports);
new_terms.swap(terms);
}
void from_cell_v1(RTLIL::Cell *cell)
{
RTLIL::SigSpec port_a = cell->getPort(ID::A);
ports.clear();
terms.clear();
auto config_bits = cell->getParam(ID::CONFIG);
int config_cursor = 0;
@ -105,7 +105,7 @@ struct Macc
{
log_assert(config_cursor + 2 + 2*num_bits <= config_width);
port_t this_port;
term_t this_port;
this_port.is_signed = config_bits[config_cursor++] == State::S1;
this_port.do_subtract = config_bits[config_cursor++] == State::S1;
@ -126,11 +126,11 @@ struct Macc
port_a_cursor += size_b;
if (size_a || size_b)
ports.push_back(this_port);
terms.push_back(this_port);
}
for (auto bit : cell->getPort(ID::B))
ports.push_back(port_t{{bit}, {}, false, false});
terms.push_back(term_t{{bit}, {}, false, false});
log_assert(config_cursor == config_width);
log_assert(port_a_cursor == GetSize(port_a));
@ -148,7 +148,7 @@ struct Macc
RTLIL::SigSpec port_b = cell->getPort(ID::B);
RTLIL::SigSpec port_c = cell->getPort(ID::C);
ports.clear();
terms.clear();
int nproducts = cell->getParam(ID::NPRODUCTS).as_int();
const Const &product_neg = cell->getParam(ID::PRODUCT_NEGATED);
@ -158,7 +158,7 @@ struct Macc
const Const &b_signed = cell->getParam(ID::B_SIGNED);
int ai = 0, bi = 0;
for (int i = 0; i < nproducts; i++) {
port_t term;
term_t term;
log_assert(a_signed[i] == b_signed[i]);
term.is_signed = (a_signed[i] == State::S1);
@ -171,7 +171,7 @@ struct Macc
bi += b_width;
term.do_subtract = (product_neg[i] == State::S1);
ports.push_back(term);
terms.push_back(term);
}
log_assert(port_a.size() == ai);
log_assert(port_b.size() == bi);
@ -182,7 +182,7 @@ struct Macc
const Const &c_signed = cell->getParam(ID::C_SIGNED);
int ci = 0;
for (int i = 0; i < naddends; i++) {
port_t term;
term_t term;
term.is_signed = (c_signed[i] == State::S1);
int c_width = c_widths.extract(16 * i, 16).as_int(false);
@ -191,7 +191,7 @@ struct Macc
ci += c_width;
term.do_subtract = (addend_neg[i] == State::S1);
ports.push_back(term);
terms.push_back(term);
}
log_assert(port_c.size() == ci);
}
@ -205,23 +205,23 @@ struct Macc
Const c_signed, c_widths, addend_negated;
SigSpec a, b, c;
for (int i = 0; i < (int) ports.size(); i++) {
SigSpec term_a = ports[i].in_a, term_b = ports[i].in_b;
for (int i = 0; i < (int) terms.size(); i++) {
SigSpec term_a = terms[i].in_a, term_b = terms[i].in_b;
if (term_b.empty()) {
// addend
c_widths.append(Const(term_a.size(), 16));
c_signed.append(ports[i].is_signed ? RTLIL::S1 : RTLIL::S0);
addend_negated.append(ports[i].do_subtract ? RTLIL::S1 : RTLIL::S0);
c_signed.append(terms[i].is_signed ? RTLIL::S1 : RTLIL::S0);
addend_negated.append(terms[i].do_subtract ? RTLIL::S1 : RTLIL::S0);
c.append(term_a);
naddends++;
} else {
// product
a_widths.append(Const(term_a.size(), 16));
b_widths.append(Const(term_b.size(), 16));
a_signed.append(ports[i].is_signed ? RTLIL::S1 : RTLIL::S0);
b_signed.append(ports[i].is_signed ? RTLIL::S1 : RTLIL::S0);
product_negated.append(ports[i].do_subtract ? RTLIL::S1 : RTLIL::S0);
a_signed.append(terms[i].is_signed ? RTLIL::S1 : RTLIL::S0);
b_signed.append(terms[i].is_signed ? RTLIL::S1 : RTLIL::S0);
product_negated.append(terms[i].do_subtract ? RTLIL::S1 : RTLIL::S0);
a.append(term_a);
b.append(term_b);
nproducts++;
@ -265,7 +265,7 @@ struct Macc
for (auto &bit : result.bits())
bit = State::S0;
for (auto &port : ports)
for (auto &port : terms)
{
if (!port.in_a.is_fully_const() || !port.in_b.is_fully_const())
return false;
@ -287,9 +287,9 @@ struct Macc
bool is_simple_product()
{
return ports.size() == 1 &&
!ports[0].in_b.empty() &&
!ports[0].do_subtract;
return terms.size() == 1 &&
!terms[0].in_b.empty() &&
!terms[0].do_subtract;
}
Macc(RTLIL::Cell *cell = nullptr)

View File

@ -2150,7 +2150,7 @@ namespace {
param(ID::TYPE);
check_expected();
std::string scope_type = cell->getParam(ID::TYPE).decode_string();
if (scope_type != "module" && scope_type != "struct")
if (scope_type != "module" && scope_type != "struct" && scope_type != "blackbox")
error(__LINE__);
return;
}

View File

@ -750,7 +750,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
for (auto &port : macc.ports)
for (auto &port : macc.terms)
{
std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
@ -788,12 +788,18 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
{
std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
std::vector<int> undef_c;
if (cell->type == ID($macc_v2))
undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
int undef_any_c = ez->expression(ezSAT::OpOr, undef_c);
int undef_any = ez->OR(undef_any_a, ez->OR(undef_any_b, undef_any_c));
std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), undef_any)));
undefGating(y, tmp, undef_y);
}

View File

@ -41,7 +41,7 @@ struct statdata_t
X(num_ports) X(num_port_bits) X(num_memories) X(num_memory_bits) X(num_cells) \
X(num_processes)
#define STAT_NUMERIC_MEMBERS STAT_INT_MEMBERS X(area)
#define STAT_NUMERIC_MEMBERS STAT_INT_MEMBERS X(area) X(sequential_area)
#define X(_name) unsigned int _name;
STAT_INT_MEMBERS

View File

@ -994,6 +994,11 @@ struct HierarchyPass : public Pass {
}
}
bool verific_mod = false;
#ifdef YOSYS_ENABLE_VERIFIC
verific_mod = verific_import_pending;
#endif
if (top_mod == nullptr && !load_top_mod.empty()) {
#ifdef YOSYS_ENABLE_VERIFIC
if (verific_import_pending) {
@ -1434,13 +1439,18 @@ struct HierarchyPass : public Pass {
if (m == nullptr)
continue;
if (m->get_blackbox_attribute() && !cell->parameters.empty() && m->get_bool_attribute(ID::dynports)) {
IdString new_m_name = m->derive(design, cell->parameters, true);
if (new_m_name.empty())
continue;
if (new_m_name != m->name) {
m = design->module(new_m_name);
blackbox_derivatives.insert(m);
bool boxed_params = false;
if (m->get_blackbox_attribute() && !cell->parameters.empty()) {
if (m->get_bool_attribute(ID::dynports)) {
IdString new_m_name = m->derive(design, cell->parameters, true);
if (new_m_name.empty())
continue;
if (new_m_name != m->name) {
m = design->module(new_m_name);
blackbox_derivatives.insert(m);
}
} else {
boxed_params = true;
}
}
@ -1456,8 +1466,12 @@ struct HierarchyPass : public Pass {
SigSpec sig = conn.second;
if (!keep_portwidths && GetSize(w) != GetSize(conn.second))
{
bool resize_widths = !keep_portwidths && GetSize(w) != GetSize(conn.second);
if (resize_widths && verific_mod && boxed_params)
log_warning("Ignoring width mismatch on %s.%s.%s from verific, is port width parametrizable?\n",
log_id(module), log_id(cell), log_id(conn.first)
);
else if (resize_widths) {
if (GetSize(w) < GetSize(conn.second))
{
int n = GetSize(conn.second) - GetSize(w);

View File

@ -2232,11 +2232,11 @@ struct MemoryLibMapPass : public Pass {
if (module->has_processes_warn())
continue;
MapWorker worker(module);
auto worker = std::make_unique<MapWorker>(module);
auto mems = Mem::get_selected_memories(module);
for (auto &mem : mems)
{
MemMapping map(worker, mem, lib, opts);
MemMapping map(*worker, mem, lib, opts);
int idx = -1;
int best = map.logic_cost;
if (!map.logic_ok) {
@ -2259,7 +2259,7 @@ struct MemoryLibMapPass : public Pass {
} else {
map.emit(map.cfgs[idx]);
// Rebuild indices after modifying module
worker = MapWorker(module);
worker = std::make_unique<MapWorker>(module);
}
}
}

View File

@ -110,7 +110,7 @@ struct ShareWorker
// Code for sharing and comparing MACC cells
// ---------------------------------------------------
static int bits_macc_port(const Macc::port_t &p, int width)
static int bits_macc_term(const Macc::term_t &p, int width)
{
if (GetSize(p.in_a) == 0 || GetSize(p.in_b) == 0)
return min(max(GetSize(p.in_a), GetSize(p.in_b)), width);
@ -120,8 +120,8 @@ struct ShareWorker
static int bits_macc(const Macc &m, int width)
{
int bits = 0;
for (auto &p : m.ports)
bits += bits_macc_port(p, width);
for (auto &p : m.terms)
bits += bits_macc_term(p, width);
return bits;
}
@ -132,7 +132,7 @@ struct ShareWorker
return bits_macc(m, width);
}
static bool cmp_macc_ports(const Macc::port_t &p1, const Macc::port_t &p2)
static bool cmp_macc_ports(const Macc::term_t &p1, const Macc::term_t &p2)
{
bool mul1 = GetSize(p1.in_a) && GetSize(p1.in_b);
bool mul2 = GetSize(p2.in_a) && GetSize(p2.in_b);
@ -161,7 +161,7 @@ struct ShareWorker
return false;
}
int share_macc_ports(Macc::port_t &p1, Macc::port_t &p2, int w1, int w2,
int share_macc_ports(Macc::term_t &p1, Macc::term_t &p2, int w1, int w2,
RTLIL::SigSpec act = RTLIL::SigSpec(), Macc *supermacc = nullptr, pool<RTLIL::Cell*> *supercell_aux = nullptr)
{
if (p1.do_subtract != p2.do_subtract)
@ -216,12 +216,12 @@ struct ShareWorker
supercell_aux->insert(module->addMux(NEW_ID, sig_b2, sig_b1, act, sig_b));
}
Macc::port_t p;
Macc::term_t p;
p.in_a = sig_a;
p.in_b = sig_b;
p.is_signed = force_signed;
p.do_subtract = p1.do_subtract;
supermacc->ports.push_back(p);
supermacc->terms.push_back(p);
}
int score = 1000 + abs(GetSize(p1.in_a) - GetSize(p2.in_a)) * max(abs(GetSize(p1.in_b) - GetSize(p2.in_b)), 1);
@ -248,15 +248,15 @@ struct ShareWorker
m1.optimize(w1);
m2.optimize(w2);
std::sort(m1.ports.begin(), m1.ports.end(), cmp_macc_ports);
std::sort(m2.ports.begin(), m2.ports.end(), cmp_macc_ports);
std::sort(m1.terms.begin(), m1.terms.end(), cmp_macc_ports);
std::sort(m2.terms.begin(), m2.terms.end(), cmp_macc_ports);
std::set<int> m1_unmapped, m2_unmapped;
for (int i = 0; i < GetSize(m1.ports); i++)
for (int i = 0; i < GetSize(m1.terms); i++)
m1_unmapped.insert(i);
for (int i = 0; i < GetSize(m2.ports); i++)
for (int i = 0; i < GetSize(m2.terms); i++)
m2_unmapped.insert(i);
while (1)
@ -265,7 +265,7 @@ struct ShareWorker
for (int i : m1_unmapped)
for (int j : m2_unmapped) {
int score = share_macc_ports(m1.ports[i], m2.ports[j], w1, w2);
int score = share_macc_ports(m1.terms[i], m2.terms[j], w1, w2);
if (score >= 0 && (best_i < 0 || best_score > score))
best_i = i, best_j = j, best_score = score;
}
@ -273,55 +273,55 @@ struct ShareWorker
if (best_i >= 0) {
m1_unmapped.erase(best_i);
m2_unmapped.erase(best_j);
share_macc_ports(m1.ports[best_i], m2.ports[best_j], w1, w2, act, &supermacc, supercell_aux);
share_macc_ports(m1.terms[best_i], m2.terms[best_j], w1, w2, act, &supermacc, supercell_aux);
} else
break;
}
for (int i : m1_unmapped)
{
RTLIL::SigSpec sig_a = m1.ports[i].in_a;
RTLIL::SigSpec sig_b = m1.ports[i].in_b;
RTLIL::SigSpec sig_a = m1.terms[i].in_a;
RTLIL::SigSpec sig_b = m1.terms[i].in_b;
if (supercell_aux && GetSize(sig_a)) {
sig_a = module->addWire(NEW_ID, GetSize(sig_a));
supercell_aux->insert(module->addMux(NEW_ID, RTLIL::SigSpec(0, GetSize(sig_a)), m1.ports[i].in_a, act, sig_a));
supercell_aux->insert(module->addMux(NEW_ID, RTLIL::SigSpec(0, GetSize(sig_a)), m1.terms[i].in_a, act, sig_a));
}
if (supercell_aux && GetSize(sig_b)) {
sig_b = module->addWire(NEW_ID, GetSize(sig_b));
supercell_aux->insert(module->addMux(NEW_ID, RTLIL::SigSpec(0, GetSize(sig_b)), m1.ports[i].in_b, act, sig_b));
supercell_aux->insert(module->addMux(NEW_ID, RTLIL::SigSpec(0, GetSize(sig_b)), m1.terms[i].in_b, act, sig_b));
}
Macc::port_t p;
Macc::term_t p;
p.in_a = sig_a;
p.in_b = sig_b;
p.is_signed = m1.ports[i].is_signed;
p.do_subtract = m1.ports[i].do_subtract;
supermacc.ports.push_back(p);
p.is_signed = m1.terms[i].is_signed;
p.do_subtract = m1.terms[i].do_subtract;
supermacc.terms.push_back(p);
}
for (int i : m2_unmapped)
{
RTLIL::SigSpec sig_a = m2.ports[i].in_a;
RTLIL::SigSpec sig_b = m2.ports[i].in_b;
RTLIL::SigSpec sig_a = m2.terms[i].in_a;
RTLIL::SigSpec sig_b = m2.terms[i].in_b;
if (supercell_aux && GetSize(sig_a)) {
sig_a = module->addWire(NEW_ID, GetSize(sig_a));
supercell_aux->insert(module->addMux(NEW_ID, m2.ports[i].in_a, RTLIL::SigSpec(0, GetSize(sig_a)), act, sig_a));
supercell_aux->insert(module->addMux(NEW_ID, m2.terms[i].in_a, RTLIL::SigSpec(0, GetSize(sig_a)), act, sig_a));
}
if (supercell_aux && GetSize(sig_b)) {
sig_b = module->addWire(NEW_ID, GetSize(sig_b));
supercell_aux->insert(module->addMux(NEW_ID, m2.ports[i].in_b, RTLIL::SigSpec(0, GetSize(sig_b)), act, sig_b));
supercell_aux->insert(module->addMux(NEW_ID, m2.terms[i].in_b, RTLIL::SigSpec(0, GetSize(sig_b)), act, sig_b));
}
Macc::port_t p;
Macc::term_t p;
p.in_a = sig_a;
p.in_b = sig_b;
p.is_signed = m2.ports[i].is_signed;
p.do_subtract = m2.ports[i].do_subtract;
supermacc.ports.push_back(p);
p.is_signed = m2.terms[i].is_signed;
p.do_subtract = m2.terms[i].do_subtract;
supermacc.terms.push_back(p);
}
if (supercell)
@ -1000,6 +1000,61 @@ struct ShareWorker
}
}
pool<std::pair<SigBit, State>> pattern_bits(const pool<ssc_pair_t> &activation_patterns)
{
pool<std::pair<SigBit, State>> bits;
for (auto const &pattern : activation_patterns) {
for (int i = 0; i < GetSize(pattern.second); ++i) {
SigBit bit = pattern.first[i];
State val = pattern.second[i];
bits.emplace(bit, val);
}
}
return bits;
}
bool onesided_restrict_activation_patterns(
pool<ssc_pair_t> &activation_patterns, const pool<std::pair<SigBit, State>> &other_bits)
{
pool<ssc_pair_t> new_activation_patterns;
bool simplified = false;
for (auto const &pattern : activation_patterns) {
ssc_pair_t new_pair;
for (int i = 0; i < GetSize(pattern.second); ++i) {
SigBit bit = pattern.first[i];
State val = pattern.second[i];
if (other_bits.count({bit, val == State::S0 ? State::S1 : State::S0})) {
new_pair.first.append(bit);
new_pair.second.append(val);
} else {
simplified = true;
}
}
new_activation_patterns.emplace(std::move(new_pair));
}
activation_patterns = std::move(new_activation_patterns);
return simplified;
}
// Only valid if the patterns on their own (i.e. without considering their input cone) are mutually exclusive!
bool restrict_activation_patterns(pool<ssc_pair_t> &activation_patterns, pool<ssc_pair_t> &other_activation_patterns)
{
pool<std::pair<SigBit, State>> bits = pattern_bits(activation_patterns);
pool<std::pair<SigBit, State>> other_bits = pattern_bits(other_activation_patterns);
bool simplified = false;
simplified |= onesided_restrict_activation_patterns(activation_patterns, other_bits);
simplified |= onesided_restrict_activation_patterns(other_activation_patterns, bits);
optimize_activation_patterns(activation_patterns);
optimize_activation_patterns(other_activation_patterns);
return simplified;
}
RTLIL::SigSpec make_cell_activation_logic(const pool<ssc_pair_t> &activation_patterns, pool<RTLIL::Cell*> &supercell_aux)
{
RTLIL::Wire *all_cases_wire = module->addWire(NEW_ID, 0);
@ -1299,17 +1354,18 @@ struct ShareWorker
other_cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
all_ctrl_signals.append(p.first);
}
int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active);
int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active);
bool pattern_only_solve = qcsat.ez->solve(qcsat.ez->AND(sub1, sub2));
qcsat.prepare();
int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active);
if (!qcsat.ez->solve(sub1)) {
log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell));
cells_to_remove.insert(cell);
break;
}
int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active);
if (!qcsat.ez->solve(sub2)) {
log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell));
cells_to_remove.insert(other_cell);
@ -1317,28 +1373,43 @@ struct ShareWorker
continue;
}
qcsat.ez->non_incremental();
pool<ssc_pair_t> optimized_cell_activation_patterns = filtered_cell_activation_patterns;
pool<ssc_pair_t> optimized_other_cell_activation_patterns = filtered_other_cell_activation_patterns;
all_ctrl_signals.sort_and_unify();
std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
std::vector<bool> sat_model_values;
if (pattern_only_solve) {
qcsat.ez->non_incremental();
qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
all_ctrl_signals.sort_and_unify();
std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
std::vector<bool> sat_model_values;
log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n",
qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
if (qcsat.ez->solve(sat_model, sat_model_values)) {
log(" According to the SAT solver this pair of cells can not be shared.\n");
log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values));
for (int i = GetSize(sat_model_values)-1; i >= 0; i--)
log("%c", sat_model_values[i] ? '1' : '0');
log("\n");
continue;
log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n",
qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
if (qcsat.ez->solve(sat_model, sat_model_values)) {
log(" According to the SAT solver this pair of cells can not be shared.\n");
log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values));
for (int i = GetSize(sat_model_values)-1; i >= 0; i--)
log("%c", sat_model_values[i] ? '1' : '0');
log("\n");
continue;
}
log(" According to the SAT solver this pair of cells can be shared.\n");
} else {
log(" According to the SAT solver this pair of cells can be shared. (Pattern only case)\n");
if (restrict_activation_patterns(optimized_cell_activation_patterns, optimized_other_cell_activation_patterns)) {
for (auto &p : optimized_cell_activation_patterns)
log(" Simplified activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second));
for (auto &p : optimized_other_cell_activation_patterns)
log(" Simplified activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second));
}
}
log(" According to the SAT solver this pair of cells can be shared.\n");
if (find_in_input_cone(cell, other_cell)) {
log(" Sharing not possible: %s is in input cone of %s.\n", log_id(other_cell), log_id(cell));
continue;
@ -1354,20 +1425,20 @@ struct ShareWorker
int cell_select_score = 0;
int other_cell_select_score = 0;
for (auto &p : filtered_cell_activation_patterns)
for (auto &p : optimized_cell_activation_patterns)
cell_select_score += p.first.size();
for (auto &p : filtered_other_cell_activation_patterns)
for (auto &p : optimized_other_cell_activation_patterns)
other_cell_select_score += p.first.size();
RTLIL::Cell *supercell;
pool<RTLIL::Cell*> supercell_aux;
if (cell_select_score <= other_cell_select_score) {
RTLIL::SigSpec act = make_cell_activation_logic(filtered_cell_activation_patterns, supercell_aux);
RTLIL::SigSpec act = make_cell_activation_logic(optimized_cell_activation_patterns, supercell_aux);
supercell = make_supercell(cell, other_cell, act, supercell_aux);
log(" Activation signal for %s: %s\n", log_id(cell), log_signal(act));
} else {
RTLIL::SigSpec act = make_cell_activation_logic(filtered_other_cell_activation_patterns, supercell_aux);
RTLIL::SigSpec act = make_cell_activation_logic(optimized_other_cell_activation_patterns, supercell_aux);
supercell = make_supercell(other_cell, cell, act, supercell_aux);
log(" Activation signal for %s: %s\n", log_id(other_cell), log_signal(act));
}

View File

@ -37,10 +37,20 @@ struct CutpointPass : public Pass {
log(" set cutpoint nets to undef (x). the default behavior is to create\n");
log(" an $anyseq cell and drive the cutpoint net from that\n");
log("\n");
log(" -noscopeinfo\n");
log(" do not create '$scopeinfo' cells that preserve attributes of cells that\n");
log(" were removed by this pass\n");
log("\n");
log(" cutpoint -blackbox [options]\n");
log("\n");
log("Replace all instances of blackboxes in the design with a formal cut point.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool flag_undef = false;
bool flag_undef = false;
bool flag_scopeinfo = true;
bool flag_blackbox = false;
log_header(design, "Executing CUTPOINT pass.\n");
@ -51,26 +61,31 @@ struct CutpointPass : public Pass {
flag_undef = true;
continue;
}
if (args[argidx] == "-noscopeinfo") {
flag_scopeinfo = false;
continue;
}
if (args[argidx] == "-blackbox") {
flag_blackbox = true;
continue;
}
break;
}
extra_args(args, argidx, design);
for (auto module : design->selected_modules())
{
if (module->is_selected_whole()) {
log("Making all outputs of module %s cut points, removing module contents.\n", log_id(module));
module->new_connections(std::vector<RTLIL::SigSig>());
for (auto cell : vector<Cell*>(module->cells()))
module->remove(cell);
vector<Wire*> output_wires;
for (auto wire : module->wires())
if (wire->port_output)
output_wires.push_back(wire);
for (auto wire : output_wires)
module->connect(wire, flag_undef ? Const(State::Sx, GetSize(wire)) : module->Anyseq(NEW_ID, GetSize(wire)));
continue;
}
if (flag_blackbox) {
if (!design->full_selection())
log_cmd_error("This command only operates on fully selected designs!\n");
design->push_empty_selection();
auto &selection = design->selection();
for (auto module : design->modules())
for (auto cell : module->cells())
if (selection.boxed_module(cell->type))
selection.select(module, cell);
}
for (auto module : design->all_selected_modules())
{
SigMap sigmap(module);
pool<SigBit> cutpoint_bits;
@ -82,7 +97,26 @@ struct CutpointPass : public Pass {
if (cell->output(conn.first))
module->connect(conn.second, flag_undef ? Const(State::Sx, GetSize(conn.second)) : module->Anyseq(NEW_ID, GetSize(conn.second)));
}
RTLIL::Cell *scopeinfo = nullptr;
auto cell_name = cell->name;
if (flag_scopeinfo && cell_name.isPublic()) {
auto scopeinfo = module->addCell(NEW_ID, ID($scopeinfo));
scopeinfo->setParam(ID::TYPE, RTLIL::Const("blackbox"));
for (auto const &attr : cell->attributes)
{
if (attr.first == ID::hdlname)
scopeinfo->attributes.insert(attr);
else
scopeinfo->attributes.emplace(stringf("\\cell_%s", RTLIL::unescape_id(attr.first).c_str()), attr.second);
}
}
module->remove(cell);
if (scopeinfo != nullptr)
module->rename(scopeinfo, cell_name);
}
for (auto wire : module->selected_wires()) {

View File

@ -54,6 +54,7 @@ OBJS += passes/techmap/flowmap.o
OBJS += passes/techmap/extractinv.o
OBJS += passes/techmap/cellmatch.o
OBJS += passes/techmap/clockgate.o
OBJS += passes/techmap/constmap.o
endif
ifeq ($(DISABLE_SPAWN),0)
@ -62,5 +63,5 @@ EXTRA_OBJS += passes/techmap/filterlib.o
$(PROGRAM_PREFIX)yosys-filterlib$(EXE): passes/techmap/filterlib.o
$(Q) mkdir -p $(dir $@)
$(P) $(CXX) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LINKFLAGS) $^ $(LIBS)
$(P) $(CXX) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LINKFLAGS) $^ $(EXE_LIBS) $(LIBS)
endif

View File

@ -142,7 +142,7 @@ struct AlumaccWorker
log(" creating $macc model for %s (%s).\n", log_id(cell), log_id(cell->type));
maccnode_t *n = new maccnode_t;
Macc::port_t new_port;
Macc::term_t new_term;
n->cell = cell;
n->y = sigmap(cell->getPort(ID::Y));
@ -153,32 +153,32 @@ struct AlumaccWorker
if (cell->type.in(ID($pos), ID($neg)))
{
new_port.in_a = sigmap(cell->getPort(ID::A));
new_port.is_signed = cell->getParam(ID::A_SIGNED).as_bool();
new_port.do_subtract = cell->type == ID($neg);
n->macc.ports.push_back(new_port);
new_term.in_a = sigmap(cell->getPort(ID::A));
new_term.is_signed = cell->getParam(ID::A_SIGNED).as_bool();
new_term.do_subtract = cell->type == ID($neg);
n->macc.terms.push_back(new_term);
}
if (cell->type.in(ID($add), ID($sub)))
{
new_port.in_a = sigmap(cell->getPort(ID::A));
new_port.is_signed = cell->getParam(ID::A_SIGNED).as_bool();
new_port.do_subtract = false;
n->macc.ports.push_back(new_port);
new_term.in_a = sigmap(cell->getPort(ID::A));
new_term.is_signed = cell->getParam(ID::A_SIGNED).as_bool();
new_term.do_subtract = false;
n->macc.terms.push_back(new_term);
new_port.in_a = sigmap(cell->getPort(ID::B));
new_port.is_signed = cell->getParam(ID::B_SIGNED).as_bool();
new_port.do_subtract = cell->type == ID($sub);
n->macc.ports.push_back(new_port);
new_term.in_a = sigmap(cell->getPort(ID::B));
new_term.is_signed = cell->getParam(ID::B_SIGNED).as_bool();
new_term.do_subtract = cell->type == ID($sub);
n->macc.terms.push_back(new_term);
}
if (cell->type.in(ID($mul)))
{
new_port.in_a = sigmap(cell->getPort(ID::A));
new_port.in_b = sigmap(cell->getPort(ID::B));
new_port.is_signed = cell->getParam(ID::A_SIGNED).as_bool();
new_port.do_subtract = false;
n->macc.ports.push_back(new_port);
new_term.in_a = sigmap(cell->getPort(ID::A));
new_term.in_b = sigmap(cell->getPort(ID::B));
new_term.is_signed = cell->getParam(ID::A_SIGNED).as_bool();
new_term.do_subtract = false;
n->macc.terms.push_back(new_term);
}
log_assert(sig_macc.count(n->y) == 0);
@ -190,7 +190,7 @@ struct AlumaccWorker
{
std::vector<int> port_sizes;
for (auto &port : macc.ports) {
for (auto &port : macc.terms) {
if (port.is_signed != is_signed)
return true;
if (!port.is_signed && port.do_subtract)
@ -235,9 +235,9 @@ struct AlumaccWorker
if (delete_nodes.count(n))
continue;
for (int i = 0; i < GetSize(n->macc.ports); i++)
for (int i = 0; i < GetSize(n->macc.terms); i++)
{
auto &port = n->macc.ports[i];
auto &port = n->macc.terms[i];
if (GetSize(port.in_b) > 0 || sig_macc.count(port.in_a) == 0)
continue;
@ -253,13 +253,13 @@ struct AlumaccWorker
log(" merging $macc model for %s into %s.\n", log_id(other_n->cell), log_id(n->cell));
bool do_subtract = port.do_subtract;
for (int j = 0; j < GetSize(other_n->macc.ports); j++) {
for (int j = 0; j < GetSize(other_n->macc.terms); j++) {
if (do_subtract)
other_n->macc.ports[j].do_subtract = !other_n->macc.ports[j].do_subtract;
other_n->macc.terms[j].do_subtract = !other_n->macc.terms[j].do_subtract;
if (j == 0)
n->macc.ports[i--] = other_n->macc.ports[j];
n->macc.terms[i--] = other_n->macc.terms[j];
else
n->macc.ports.push_back(other_n->macc.ports[j]);
n->macc.terms.push_back(other_n->macc.terms[j]);
}
delete_nodes.insert(other_n);
@ -288,7 +288,7 @@ struct AlumaccWorker
bool subtract_b = false;
alunode_t *alunode;
for (auto &port : n->macc.ports)
for (auto &port : n->macc.terms)
if (GetSize(port.in_b) > 0) {
goto next_macc;
} else if (GetSize(port.in_a) == 1 && !port.is_signed && !port.do_subtract) {

View File

@ -227,9 +227,9 @@ struct BoothPassWorker {
continue;
}
A = macc.ports[0].in_a;
B = macc.ports[0].in_b;
is_signed = macc.ports[0].is_signed;
A = macc.terms[0].in_a;
B = macc.terms[0].in_b;
is_signed = macc.terms[0].is_signed;
Y = cell->getPort(ID::Y);
} else {
continue;

106
passes/techmap/constmap.cc Normal file
View File

@ -0,0 +1,106 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2025 King Lok Chung <king.chung@manchester.ac.uk>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*/
#include "kernel/register.h"
#include "kernel/rtlil.h"
#include "kernel/log.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
static std::string celltype, cell_portname, cell_paramname;
static RTLIL::Module *module;
static RTLIL::SigChunk value;
void constmap_worker(RTLIL::SigSpec &sig)
{
if (sig.is_fully_const()){
value = module->addWire(NEW_ID, sig.size());
RTLIL::Cell *cell = module->addCell(NEW_ID, celltype);
cell->setParam(cell_paramname, sig.as_const());
cell->setPort(cell_portname, value);
sig = value;
}
}
struct ConstmapPass : public Pass {
ConstmapPass() : Pass("constmap", "technology mapping of coarse constant value") { }
void help() override
{
log("\n");
log(" constmap [options] [selection]\n");
log("\n");
log("Map constants to a driver cell.\n");
log("\n");
log(" -cell <celltype> <portname> <paramname>\n");
log(" Replace constant bits with this cell.\n");
log(" The value of the constant will be stored to the parameter specified.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
log_header(design, "Executing CONSTMAP pass (mapping to constant driver).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
if (args[argidx] == "-cell" && argidx+3 < args.size()){
celltype = RTLIL::escape_id(args[++argidx]);
cell_portname = RTLIL::escape_id(args[++argidx]);
cell_paramname = RTLIL::escape_id(args[++argidx]);
continue;
}
break;
}
extra_args(args, argidx, design);
if (design->has(celltype)) {
Module *existing = design->module(celltype);
bool has_port = false;
for (auto &p : existing->ports){
if (p == cell_portname){
has_port = true;
break;
}
}
if (!has_port)
log_cmd_error("Cell type '%s' does not have port '%s'.\n", celltype.c_str(), cell_portname.c_str());
bool has_param = false;
for (auto &p : existing->avail_parameters){
if (p == cell_paramname)
has_param = true;
}
if (!has_param)
log_cmd_error("Cell type '%s' does not have parameter '%s'.\n", celltype.c_str(), cell_paramname.c_str());
}
for (auto mod : design->selected_modules())
{
module = mod;
module->rewrite_sigspecs(constmap_worker);
}
}
} ConstmapPass;
PRIVATE_NAMESPACE_END

View File

@ -75,7 +75,7 @@ bool LibertyInputStream::extend_buffer_once()
buffer.resize(buf_end + chunk_size);
}
size_t read_size = f.rdbuf()->sgetn(buffer.data() + buf_end, chunk_size);
size_t read_size = f.rdbuf()->sgetn((char *)buffer.data() + buf_end, chunk_size);
buf_end += read_size;
if (read_size < chunk_size)
eof = true;
@ -436,6 +436,9 @@ void LibertyParser::report_unexpected_token(int tok)
eReport += "'.";
error(eReport);
break;
case EOF:
error("Unexpected end of file");
break;
default:
eReport = "Unexpected token: ";
eReport += static_cast<char>(tok);
@ -484,7 +487,7 @@ void LibertyParser::parse_vector_range(int tok)
}
}
LibertyAst *LibertyParser::parse()
LibertyAst *LibertyParser::parse(bool top_level)
{
std::string str;
@ -498,7 +501,13 @@ LibertyAst *LibertyParser::parse()
while ((tok == 'n') || (tok == ';'))
tok = lexer(str);
if (tok == '}' || tok < 0)
if (tok == EOF) {
if (top_level)
return NULL;
report_unexpected_token(tok);
}
if (tok == '}')
return NULL;
if (tok != 'v') {
@ -571,12 +580,18 @@ LibertyAst *LibertyParser::parse()
}
if (tok == '{') {
bool terminated = false;
while (1) {
LibertyAst *child = parse();
if (child == NULL)
LibertyAst *child = parse(false);
if (child == NULL) {
terminated = true;
break;
}
ast->children.push_back(child);
}
if (!terminated) {
report_unexpected_token(EOF);
}
break;
}

View File

@ -92,7 +92,7 @@ namespace Yosys
class LibertyInputStream {
std::istream &f;
std::vector<char> buffer;
std::vector<unsigned char> buffer;
size_t buf_pos = 0;
size_t buf_end = 0;
bool eof = false;
@ -107,7 +107,7 @@ namespace Yosys
LibertyInputStream(std::istream &f) : f(f) {}
size_t buffered_size() { return buf_end - buf_pos; }
const char *buffered_data() { return buffer.data() + buf_pos; }
const unsigned char *buffered_data() { return buffer.data() + buf_pos; }
int get() {
if (buf_pos == buf_end)
@ -165,7 +165,7 @@ namespace Yosys
void report_unexpected_token(int tok);
void parse_vector_range(int tok);
LibertyAst *parse();
LibertyAst *parse(bool top_level);
void error() const;
void error(const std::string &str) const;
@ -174,18 +174,29 @@ namespace Yosys
const LibertyAst *ast = nullptr;
LibertyParser(std::istream &f) : f(f), line(1) {
shared_ast.reset(parse());
shared_ast.reset(parse(true));
ast = shared_ast.get();
if (!ast) {
#ifdef FILTERLIB
fprintf(stderr, "No entries found in liberty file.\n");
exit(1);
#else
log_error("No entries found in liberty file.\n");
#endif
}
}
#ifndef FILTERLIB
LibertyParser(std::istream &f, const std::string &fname) : f(f), line(1) {
shared_ast = LibertyAstCache::instance.cached_ast(fname);
if (!shared_ast) {
shared_ast.reset(parse());
shared_ast.reset(parse(true));
LibertyAstCache::instance.parsed_ast(fname, shared_ast);
}
ast = shared_ast.get();
if (!ast) {
log_error("No entries found in liberty file `%s'.\n", fname.c_str());
}
}
#endif
};

View File

@ -278,42 +278,42 @@ void maccmap(RTLIL::Module *module, RTLIL::Cell *cell, bool unmap)
return;
}
for (auto &port : macc.ports)
if (GetSize(port.in_b) == 0)
log(" %s %s (%d bits, %s)\n", port.do_subtract ? "sub" : "add", log_signal(port.in_a),
GetSize(port.in_a), port.is_signed ? "signed" : "unsigned");
for (auto &term : macc.terms)
if (GetSize(term.in_b) == 0)
log(" %s %s (%d bits, %s)\n", term.do_subtract ? "sub" : "add", log_signal(term.in_a),
GetSize(term.in_a), term.is_signed ? "signed" : "unsigned");
else
log(" %s %s * %s (%dx%d bits, %s)\n", port.do_subtract ? "sub" : "add", log_signal(port.in_a), log_signal(port.in_b),
GetSize(port.in_a), GetSize(port.in_b), port.is_signed ? "signed" : "unsigned");
log(" %s %s * %s (%dx%d bits, %s)\n", term.do_subtract ? "sub" : "add", log_signal(term.in_a), log_signal(term.in_b),
GetSize(term.in_a), GetSize(term.in_b), term.is_signed ? "signed" : "unsigned");
if (unmap)
{
typedef std::pair<RTLIL::SigSpec, bool> summand_t;
std::vector<summand_t> summands;
RTLIL::SigSpec bit_ports;
RTLIL::SigSpec bit_terms;
for (auto &port : macc.ports) {
for (auto &term : macc.terms) {
summand_t this_summand;
if (GetSize(port.in_b)) {
if (GetSize(term.in_b)) {
this_summand.first = module->addWire(NEW_ID, width);
module->addMul(NEW_ID, port.in_a, port.in_b, this_summand.first, port.is_signed);
} else if (GetSize(port.in_a) == 1 && GetSize(port.in_b) == 0 && !port.is_signed && !port.do_subtract) {
// Mimic old 'bit_ports' treatment in case it's relevant for performance,
module->addMul(NEW_ID, term.in_a, term.in_b, this_summand.first, term.is_signed);
} else if (GetSize(term.in_a) == 1 && GetSize(term.in_b) == 0 && !term.is_signed && !term.do_subtract) {
// Mimic old 'bit_terms' treatment in case it's relevant for performance,
// i.e. defer single-bit summands to be the last ones
bit_ports.append(port.in_a);
bit_terms.append(term.in_a);
continue;
} else if (GetSize(port.in_a) != width) {
} else if (GetSize(term.in_a) != width) {
this_summand.first = module->addWire(NEW_ID, width);
module->addPos(NEW_ID, port.in_a, this_summand.first, port.is_signed);
module->addPos(NEW_ID, term.in_a, this_summand.first, term.is_signed);
} else {
this_summand.first = port.in_a;
this_summand.first = term.in_a;
}
this_summand.second = port.do_subtract;
this_summand.second = term.do_subtract;
summands.push_back(this_summand);
}
for (auto &bit : bit_ports)
for (auto &bit : bit_terms)
summands.push_back(summand_t(bit, false));
if (GetSize(summands) == 0)
@ -350,20 +350,20 @@ void maccmap(RTLIL::Module *module, RTLIL::Cell *cell, bool unmap)
else
{
MaccmapWorker worker(module, width);
RTLIL::SigSpec bit_ports;
RTLIL::SigSpec bit_terms;
for (auto &port : macc.ports) {
// Mimic old 'bit_ports' treatment in case it's relevant for performance,
for (auto &term : macc.terms) {
// Mimic old 'bit_terms' treatment in case it's relevant for performance,
// i.e. defer single-bit summands to be the last ones
if (GetSize(port.in_a) == 1 && GetSize(port.in_b) == 0 && !port.is_signed && !port.do_subtract)
bit_ports.append(port.in_a);
else if (GetSize(port.in_b) == 0)
worker.add(port.in_a, port.is_signed, port.do_subtract);
if (GetSize(term.in_a) == 1 && GetSize(term.in_b) == 0 && !term.is_signed && !term.do_subtract)
bit_terms.append(term.in_a);
else if (GetSize(term.in_b) == 0)
worker.add(term.in_a, term.is_signed, term.do_subtract);
else
worker.add(port.in_a, port.in_b, port.is_signed, port.do_subtract);
worker.add(term.in_a, term.in_b, term.is_signed, term.do_subtract);
}
for (auto bit : bit_ports)
for (auto bit : bit_terms)
worker.add(bit, 0);
module->connect(cell->getPort(ID::Y), worker.synth());

View File

@ -189,17 +189,17 @@ static RTLIL::Cell* create_gold_module(RTLIL::Design *design, RTLIL::IdString ce
} else
size_b = 0;
Macc::port_t this_port;
Macc::term_t this_term;
wire_a->width += size_a;
this_port.in_a = RTLIL::SigSpec(wire_a, wire_a->width - size_a, size_a);
this_term.in_a = RTLIL::SigSpec(wire_a, wire_a->width - size_a, size_a);
wire_a->width += size_b;
this_port.in_b = RTLIL::SigSpec(wire_a, wire_a->width - size_b, size_b);
this_term.in_b = RTLIL::SigSpec(wire_a, wire_a->width - size_b, size_b);
this_port.is_signed = xorshift32(2) == 1;
this_port.do_subtract = xorshift32(2) == 1;
macc.ports.push_back(this_port);
this_term.is_signed = xorshift32(2) == 1;
this_term.do_subtract = xorshift32(2) == 1;
macc.terms.push_back(this_term);
}
// Macc::to_cell sets the input ports
macc.to_cell(cell);

View File

@ -37,8 +37,6 @@ class libyosys_so_ext(Extension):
)
self.args = [
"ENABLE_PYOSYS=1",
# Wheel meant to be imported from interpreter
"ENABLE_PYTHON_CONFIG_EMBED=0",
# Would need to be installed separately by the user
"ENABLE_TCL=0",
"ENABLE_READLINE=0",
@ -86,9 +84,6 @@ class libyosys_so_ext(Extension):
shutil.copytree("share", share_target)
# I don't know how debug info is getting here.
class custom_build_ext(build_ext):
def build_extension(self, ext) -> None:
if not hasattr(ext, "custom_build"):

View File

@ -0,0 +1,14 @@
// The parser used to choke on the copyright symbol even in comments
// © ® ø Φ
library(dummy) {
cell(buffer) {
area : 1 ;
pin(A) {
direction : input ;
}
pin(Y) {
direction : output ;
function : "A" ;
}
}
}

View File

@ -0,0 +1,12 @@
library(dummy) {
cell(buffer) {
area : 1 ;
pin(A) {
direction : input ;
}
pin(Y) {
direction : output ;
function : "A" ;
}
}
}

View File

@ -0,0 +1,5 @@
module buffer (A, Y);
input A;
output Y;
assign Y = A; // "A"
endmodule

View File

@ -30,3 +30,26 @@ module test_2(
end
endmodule
module test_3(
input [3:0] s,
input [7:0] a, b, c,
output reg [7:0] y0,
output reg [7:0] y1,
output reg [7:0] y2,
output reg [7:0] y3,
);
wire is_onehot = s & (s - 1);
always @* begin
y0 <= 0;
y1 <= 0;
y2 <= 0;
y3 <= 0;
if (s < 3) y0 <= b / c;
if (3 <= s && s < 6) y1 <= c / b;
if (6 <= s && s < 9) y2 <= a / b;
if (9 <= s && s < 12) y3 <= b / a;
end
endmodule

View File

@ -3,11 +3,13 @@ proc;;
copy test_1 gold_1
copy test_2 gold_2
share test_1 test_2;;
copy test_3 gold_3
share test_1 test_2 test_3;;
select -assert-count 1 test_1/t:$mul
select -assert-count 1 test_2/t:$mul
select -assert-count 1 test_2/t:$div
select -assert-count 1 test_3/t:$div
miter -equiv -flatten -make_outputs -make_outcmp gold_1 test_1 miter_1
sat -verify -prove trigger 0 -show-inputs -show-outputs miter_1
@ -15,3 +17,5 @@ sat -verify -prove trigger 0 -show-inputs -show-outputs miter_1
miter -equiv -flatten -make_outputs -make_outcmp gold_2 test_2 miter_2
sat -verify -prove trigger 0 -show-inputs -show-outputs miter_2
miter -equiv -flatten -make_outputs -make_outcmp gold_3 test_3 miter_3
sat -verify -prove trigger 0 -show-inputs -show-outputs miter_3

43
tests/techmap/constmap.ys Normal file
View File

@ -0,0 +1,43 @@
read_verilog << EOT
module test();
wire [31:0] in;
wire [31:0] out;
assign out = in + 16;
endmodule
EOT
constmap -cell const_cell O value
select -assert-count 1 t:const_cell r:value=16 %i
design -reset
read_verilog -lib << EOT
module const_cell(O);
parameter value=0;
output O;
endmodule
EOT
read_verilog << EOT
module test();
wire [31:0] in;
wire [31:0] out1;
wire [31:0] out2;
assign out1 = in + 16;
assign out2 = in + 32;
endmodule
EOT
constmap -cell const_cell O value
select -assert-count 2 t:const_cell
select -assert-count 1 r:value=16
select -assert-count 1 r:value=32
select -assert-count 1 test/out1 %ci* r:value=16 %i
select -assert-count 1 test/out2 %ci* r:value=32 %i
select -assert-count 1 t:const_cell r:value=16 %i
select -assert-count 1 t:const_cell r:value=32 %i

View File

@ -1,6 +1,7 @@
/*.log
/*.out
/aiger2*.aig
/*.sel
/write_gzip.v
/write_gzip.v.gz
/run-test.mk

View File

@ -0,0 +1,72 @@
read_verilog -specify << EOT
module top(input a, b, output o);
wire c, d, e;
bb #(.SOME_PARAM(1)) bb1 (.a (a), .b (b), .o (c));
bb #(.SOME_PARAM(2)) bb2 (.a (a), .b (b), .o (d));
wb wb1 (.a (a), .b (b), .o (e));
some_mod some_inst (.a (c), .b (d), .c (e), .o (o));
endmodule
(* blackbox *)
module bb #( parameter SOME_PARAM=0 ) (input a, b, output o);
assign o = a | b;
specify
(a => o) = 1;
endspecify
endmodule
(* whitebox *)
module wb(input a, b, output o);
assign o = a ^ b;
endmodule
module some_mod(input a, b, c, output o);
assign o = a & (b | c);
endmodule
EOT
hierarchy -top top
design -save hier
select -assert-none t:$anyseq
select -assert-count 3 =t:?b
cutpoint -blackbox
select -assert-none =t:?b
select -assert-none r:SOME_PARAM
select -assert-count 3 t:$anyseq
select -assert-count 3 t:$scopeinfo
select -assert-count 3 t:$scopeinfo r:TYPE=blackbox %i
select -assert-count 3 t:$scopeinfo n:*cutpoint.cc* %i
# -noscopeinfo works with -blackbox
design -load hier
cutpoint -blackbox -noscopeinfo
select -assert-none t:$scopeinfo
# cutpoint -blackbox === cutpoint =A:whitebox =A:blackbox %u %C
# (simplified to =A:*box %C)
design -load hier
cutpoint -blackbox
rename -enumerate -pattern A_% t:$scopeinfo
rename -enumerate -pattern B_% t:$anyseq
rename -enumerate -pattern C_% w:*Anyseq*
design -save gold
select -write cutpoint.gold.sel =*
design -load hier
cutpoint =A:*box %C
rename -enumerate -pattern A_% t:$scopeinfo
rename -enumerate -pattern B_% t:$anyseq
rename -enumerate -pattern C_% w:*Anyseq*
design -save gate
select -write cutpoint.gate.sel
select -read cutpoint.gold.sel
# nothing in gate but not gold
select -assert-none % %n
design -load gold
select -read cutpoint.gate.sel
# nothing in gold but not gate
select -assert-none % %n

View File

@ -1,4 +1,4 @@
read_rtlil << EOF
read_rtlil << EOT
module \top
wire input 1 \A
wire output 2 \Y
@ -8,7 +8,67 @@ module \top
connect \Y \Y
end
end
EOF
EOT
logger -expect log "Chip area for module '\\top': 9.072000" 1
logger -expect-no-warnings
stat -liberty ../../tests/liberty/foundry_data/sg13g2_stdcell_typ_1p20V_25C.lib.filtered.gz
design -reset
read_rtlil << EOT
module \top
wire input 1 \A
wire output 2 \Y
wire output 3 \N
cell \sg13g2_and2_1 \sub1
connect \A \A
connect \B 1'0
connect \Y \Y
end
cell \child \sequential
connect \A \A
connect \B 1'0
connect \R 1'0
connect \Y \Y
connect \N \N
end
cell \child \sequential1
connect \A \A
connect \B 1'0
connect \R 1'0
connect \Y \Y
connect \N \N
end
cell \sg13g2_and2_1 \sub2
connect \A \A
connect \B 1'0
connect \Y \Y
end
end
module \child
wire input 1 \A
wire input 2 \B
wire input 3 \R
wire output 4 \Y
wire output 5 \N
cell \sg13g2_dfrbp_1 \sequential_ff
connect \CLK \A
connect \D \B
connect \Q \Y
connect \Q_N \N
connect \RESET_B \R
end
end
EOT
logger -expect log "Chip area for top module '\\top': 112.492800" 1
logger -expect log "of which used for sequential elements: 94.348800" 1
logger -expect-no-warnings
stat -liberty ../../tests/liberty/foundry_data/sg13g2_stdcell_typ_1p20V_25C.lib.filtered.gz -top \top