mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-19 13:45:48 +00:00
Code Activity

Merge branch 'main' of github.com:Silimate/yosys into force-ram-modules

Browse source
This commit is contained in:
Stan Lee 2026-07-07 13:18:12 -07:00
commit 6d51908820
32 changed files with 4680 additions and 236 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.github/actions/setup-build-env/action.yml vendored
View file

@ -56,7 +56,7 @@ runs:
if: runner.os == 'macOS'
shell: bash
run: |
brew bundle
brew install bison flex gawk libffi git pkg-config python3 bash googletest tcl-tk llvm
- name: Linux runtime environment
if: runner.os == 'Linux'

20
.github/workflows/extra-builds.yml vendored
View file

@ -172,32 +172,12 @@ jobs:
cmake -B build -DCMAKE_TOOLCHAIN_FILE=${WASI_SDK_PATH}/share/cmake/wasi-sdk-p1.cmake -DCMAKE_BUILD_TYPE=Release -DYOSYS_COMPILER_LAUNCHER=ccache .
cmake --build build -j$(nproc)
nix-build:
name: "Build nix flake"
needs: pre_job
if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch') && needs.pre_job.outputs.should_skip != 'true'
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest]
fail-fast: false
steps:
- uses: actions/checkout@v7
with:
submodules: true
persist-credentials: false
- uses: cachix/install-nix-action@v31
with:
install_url: https://releases.nixos.org/nix/nix-2.30.0/install
- run: nix build -L
extra-builds-result:
runs-on: ubuntu-latest
needs:
- vs-build
- mingw-build
- wasi-build
- nix-build
if: always()
steps:
- name: Check results

24
.github/workflows/nix.yml vendored Normal file
View file

@ -0,0 +1,24 @@
name: Test nix build
on:
workflow_dispatch:
schedule:
- cron: '0 5 * * 6'
jobs:
nix-build:
name: "Build nix flake"
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest]
fail-fast: false
steps:
- uses: actions/checkout@v7
with:
submodules: true
persist-credentials: false
- uses: cachix/install-nix-action@v31
with:
install_url: https://releases.nixos.org/nix/nix-2.30.0/install
- run: nix build -L

123
.github/workflows/release.yml vendored
View file

@ -22,6 +22,13 @@ jobs:
persist-credentials: false
ssh-key: ${{ secrets.SSH_PRIVATE_KEY }}
- name: Cache Dist Directory
uses: actions/cache@v6
with:
path: dist-x86_64-musllinux
key: ${{ github.run_id }}-x86_64-musllinux-wheel
enableCrossOsArchive: true
- name: Build wheel in Alpine container
run: |
docker run --rm \
@ -51,15 +58,10 @@ jobs:
# Build the wheel via setup.py
pip install --break-system-packages pybind11 cxxheaderparser
mkdir -p /src/dist
python3 -m pip wheel . --wheel-dir /src/dist
mkdir -p /src/dist-x86_64-musllinux
python3 -m pip wheel . --wheel-dir /src/dist-x86_64-musllinux
'
- uses: actions/upload-artifact@v4
with:
name: linux-musl-wheel
path: dist/*.whl
build-manylinux-wheel:
runs-on: ubuntu-latest
name: Build Linux amd64 wheel (manylinux2014, glibc 2.17+)
@ -71,6 +73,13 @@ jobs:
submodules: recursive
ssh-key: ${{ secrets.SSH_PRIVATE_KEY }}
- name: Cache Dist Directory
uses: actions/cache@v6
with:
path: dist-x86_64-manylinux
key: ${{ github.run_id }}-x86_64-manylinux-wheel
enableCrossOsArchive: true
- name: Build wheel in manylinux2014 container
run: |
docker run --rm \
@ -110,22 +119,18 @@ jobs:
make
cd /src
WHEEL_DIR=/src/dist-x86_64-manylinux
pip3 install --upgrade pip setuptools wheel pybind11 cxxheaderparser
mkdir -p dist-manylinux
python3 -m pip wheel . --wheel-dir /src/dist-manylinux
python3 -m pip wheel . --wheel-dir $WHEEL_DIR
# Tag wheel as manylinux2014
pip3 install auditwheel || true
for whl in /src/dist-manylinux/*.whl; do
auditwheel repair "$whl" --plat manylinux2014_x86_64 -w /src/dist-manylinux/ 2>/dev/null || true
for whl in $WHEEL_DIR/*.whl; do
auditwheel repair "$whl" --plat manylinux2014_x86_64 -w $WHEEL_DIR/ 2>/dev/null || true
done
'
- uses: actions/upload-artifact@v4
with:
name: linux-manylinux-wheel
path: dist-manylinux/*.whl
build-macos-wheel:
runs-on: macos-15
name: Build macOS arm64 wheel
@ -155,49 +160,76 @@ jobs:
cd verific/tclmain
make
- name: Cache Dist Directory
uses: actions/cache@v6
with:
path: dist-aarch64-macos
key: ${{ github.run_id }}-aarch64-macos-wheel
enableCrossOsArchive: true
- name: Build wheel
run: |
export PATH="$(brew --prefix bison)/bin:$(brew --prefix flex)/bin:$PATH"
export MACOSX_DEPLOYMENT_TARGET=11.0
mkdir -p dist
python3 -m pip wheel . --wheel-dir dist
- uses: actions/upload-artifact@v4
with:
name: macos-wheel
path: dist/*.whl
python3 -m pip wheel . --wheel-dir dist-aarch64-macos
release:
# allow testing outside main branch
if: github.ref_name == 'main'
# if: github.ref_name == 'main'
runs-on: ubuntu-latest
needs: [build-linux-wheel, build-manylinux-wheel, build-macos-wheel]
name: Create GitHub releases
steps:
- uses: actions/checkout@v4
- uses: actions/checkout@v6
with:
ssh-key: ${{ secrets.SSH_PRIVATE_KEY }}
fetch-depth: 0
- name: Download artifacts
uses: actions/download-artifact@v4
with:
path: all-wheels
merge-multiple: true
- name: Generate release notes
id: meta
- id: meta
name: Get repo metadata and clean up
run: |
SHORT_SHA=$(git rev-parse --short HEAD)
FULL_SHA=$(git rev-parse HEAD)
DATE=$(date -u +%Y-%m-%d)
echo "short_sha=$SHORT_SHA" >> "$GITHUB_OUTPUT"
echo "date=$DATE" >> "$GITHUB_OUTPUT"
REPO_URL="${{ github.server_url }}/${{ github.repository }}"
echo "short_sha=$SHORT_SHA" >> "$GITHUB_OUTPUT"
echo "full_sha=$FULL_SHA" >> "$GITHUB_OUTPUT"
echo "date=$DATE" >> "$GITHUB_OUTPUT"
echo "repo_url=$REPO_URL" >> "$GITHUB_OUTPUT"
rm -rf ./* ./.*
- uses: actions/checkout@v6
with:
repository: silimate/yosys-wheels
ssh-key: ${{ secrets.SSH_PRIVATE_KEY }}
fetch-depth: 0
- name: Restore dist from cache (x86_64-musllinux)
uses: actions/cache@v6
with:
path: dist-x86_64-musllinux
key: ${{ github.run_id }}-x86_64-musllinux-wheel
enableCrossOsArchive: true
fail-on-cache-miss: true
- name: Restore dist from cache (x86_64-manylinux)
uses: actions/cache@v6
with:
path: dist-x86_64-manylinux
key: ${{ github.run_id }}-x86_64-manylinux-wheel
enableCrossOsArchive: true
fail-on-cache-miss: true
- name: Restore dist from cache (aarch64-macos)
uses: actions/cache@v6
with:
path: dist-aarch64-macos
key: ${{ github.run_id }}-aarch64-macos-wheel
enableCrossOsArchive: true
fail-on-cache-miss: true
- name: Update release notes
run: |
printf '%s\n' \
"Automated build from \`main\` @ [\`${SHORT_SHA}\`](${REPO_URL}/commit/${FULL_SHA})" \
"Automated build from \`main\` @ [\`${{ steps.meta.outputs.short_sha }}\`](${{ steps.meta.outputs.repo_url }}/commit/${{ steps.meta.outputs.full_sha }})" \
"" \
"**Built:** ${DATE}" \
"**Built:** ${{ steps.meta.outputs.date }}" \
"" \
"### Assets" \
"| File | Platform |" \
@ -211,17 +243,22 @@ jobs:
"pip install pyosys-*.whl" \
"\`\`\`" \
> release_notes.md
- name: Commit and push
run: |
git config user.name "github-actions[bot]"
git config user.email "github-actions[bot]@users.noreply.github.com"
git commit --all --message="Build for ${{ steps.meta.outputs.date }}-${{ steps.meta.outputs.short_sha }}"
git push
- name: Create permanent release
run: |
TAG="build-${{ steps.meta.outputs.date }}-${{ steps.meta.outputs.short_sha }}"
gh release create "$TAG" \
all-wheels/*.whl \
--target "${{ github.sha }}" \
dist-*/*.whl \
--target "$(git rev-parse HEAD)" \
--title "Build ${{ steps.meta.outputs.date }} (${{ steps.meta.outputs.short_sha }})" \
--notes-file release_notes.md
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
GH_TOKEN: ${{ secrets.YOSYS_WHEELS_TOKEN }}
- name: Update latest release
run: |
@ -229,10 +266,10 @@ jobs:
git push -f origin latest
gh release delete latest --yes 2>/dev/null || true
gh release create latest \
all-wheels/*.whl \
--target "${{ github.sha }}" \
dist-*/*.whl \
--target "$(git rev-parse HEAD)" \
--title "Latest Build (${{ steps.meta.outputs.date }})" \
--notes-file release_notes.md \
--prerelease
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
GH_TOKEN: ${{ secrets.YOSYS_WHEELS_TOKEN }}

65
.github/workflows/test-build.yml vendored
View file

@ -49,7 +49,7 @@ jobs:
- id: set_output
run: |
if [ "${{ github.event_name }}" = "merge_group" ]; then
echo "should_skip=false" >> $GITHUB_OUTPUT
echo "should_skip=true" >> $GITHUB_OUTPUT
elif [ "${{ github.event_name }}" = "push" ]; then
should_skip=false
else
@ -90,7 +90,13 @@ jobs:
key: test-build-${{ matrix.os }}
save: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }}
restore-keys: |
test-build-${{ matrix.os }}-
test-build-${{ matrix.os }}
- name: Cache Build Directory
uses: actions/cache@v6
with:
path: build
key: ${{ runner.os }}-build-${{ github.run_id }}
- name: Build
shell: bash
@ -104,19 +110,6 @@ jobs:
run: |
./build/yosys-config || true
- name: Compress build
shell: bash
run: |
cd build
tar -cvf ../build.tar share/ yosys yosys-*
- name: Store build artifact
uses: actions/upload-artifact@v7
with:
name: build-${{ matrix.os }}
path: build.tar
retention-days: 1
test-yosys:
name: Run tests
runs-on: ${{ matrix.os }}
@ -142,16 +135,12 @@ jobs:
get-build-deps: true
get-iverilog: true
- name: Download build artifact
uses: actions/download-artifact@v8
- name: Restore Build Directory from Cache
uses: actions/cache@v6
with:
name: build-${{ matrix.os }}
- name: Uncompress build
shell: bash
run: |
mkdir -p build
tar -xvf build.tar -C build
path: build
key: ${{ runner.os }}-build-${{ github.run_id }}
fail-on-cache-miss: true
- name: Log yosys-config output
run: |
@ -192,19 +181,17 @@ jobs:
with:
runs-on: ${{ matrix.os }}
- name: Download build artifact
uses: actions/download-artifact@v8
- name: Restore Build Directory from Cache
uses: actions/cache@v6
with:
name: build-${{ matrix.os }}
- name: Uncompress build
shell: bash
run:
tar -xvf build.tar
path: build
key: ${{ runner.os }}-build-${{ github.run_id }}
fail-on-cache-miss: true
- name: test_cell
shell: bash
run: |
cd build
./yosys -p 'test_cell -n 20 -s 1 all'
./yosys -p 'test_cell -n 20 -s 1 -nosat -aigmap $pow $pmux'
./yosys -p 'test_cell -n 20 -s 1 -nosat -aigmap $eqx $nex $bweqx'
@ -233,16 +220,12 @@ jobs:
get-build-deps: true
get-docs-deps: true
- name: Download build artifact
uses: actions/download-artifact@v8
- name: Restore Build Directory from Cache
uses: actions/cache@v6
with:
name: build-${{ matrix.os }}
- name: Uncompress build
shell: bash
run: |
mkdir -p build
tar -xvf build.tar -C build
path: build
key: ${{ runner.os }}-build-${{ github.run_id }}
fail-on-cache-miss: true
- name: Log yosys-config output
run: |

5
.vscode/settings.json vendored
View file

@ -71,6 +71,9 @@
"variant": "cpp",
"algorithm": "cpp",
"*.inc": "cpp",
"tuple": "cpp"
"tuple": "cpp",
"__verbose_trap": "cpp",
"cstddef": "cpp",
"__log_hardening_failure": "cpp"
}
}

2
abc

@ -1 +1 @@
Subproject commit 648de7a21751cfab01c253aca6d4751f642577df
Subproject commit bec0695f0de539e974d95ab845e581da326ea3d7

6
kernel/log.cc
View file

@ -388,12 +388,6 @@ void log_formatted_file_error(std::string_view filename, int lineno, std::string
log_error_with_prefix(prefix, str);
}
void logv_file_error(const string &filename, int lineno,
const char *format, va_list ap)
{
log_formatted_file_error(filename, lineno, vstringf(format, ap));
}
void log_experimental(const std::string &str)
{
if (log_experimentals_ignored.count(str) == 0 && log_experimentals.count(str) == 0) {

13
kernel/log.h
View file

@ -24,7 +24,6 @@
#include <time.h>
#include <atomic>
#include <regex>
#define YS_REGEX_COMPILE(param) std::regex(param, \
std::regex_constants::nosubs | \
@ -44,20 +43,11 @@
# endif
#endif
#if defined(_MSC_VER)
// At least this is not in MSVC++ 2013.
# define __PRETTY_FUNCTION__ __FUNCTION__
#endif
// from libs/sha1/sha1.h
class SHA1;
YOSYS_NAMESPACE_BEGIN
#define S__LINE__sub2(x) #x
#define S__LINE__sub1(x) S__LINE__sub2(x)
#define S__LINE__ S__LINE__sub1(__LINE__)
// YS_DEBUGTRAP is a macro that is functionally equivalent to a breakpoint
// if the platform provides such functionality, and does nothing otherwise.
// If no debugger is attached, it starts a just-in-time debugger if available,
@ -120,9 +110,6 @@ extern int log_make_debug;
extern int log_force_debug;
extern int log_debug_suppressed;
[[deprecated]]
[[noreturn]] void logv_file_error(const string &filename, int lineno, const char *format, va_list ap);
void set_verific_logging(void (*cb)(int msg_type, const char *message_id, const char* file_path, unsigned int left_line, unsigned int left_col, unsigned int right_line, unsigned int right_col, const char *msg));
extern void (*log_verific_callback)(int msg_type, const char *message_id, const char* file_path, unsigned int left_line, unsigned int left_col, unsigned int right_line, unsigned int right_col, const char *msg);

4
passes/opt/CMakeLists.txt
View file

@ -108,6 +108,10 @@ yosys_pass(opt_first_fit_alloc
opt_first_fit_alloc.cc
)
yosys_pass(opt_priokey
opt_priokey.cc
)
pmgen_command(peepopt
peepopt_shiftmul_right.pmg
peepopt_shiftmul_left.pmg

14
passes/opt/cut_region.h
View file

@ -826,6 +826,20 @@ struct CutRegionWorker
return sig;
}
// Shared ConstEval for the whole matching phase. The netlist is not
// modified until rewrites are applied, so one instance (built once, at
// O(module) cost) serves every fingerprint eval instead of rebuilding
// one per candidate. Callers keep push/pop balanced, so the base state
// stays clean between uses (asserted on each hand-out).
std::unique_ptr<ConstEval> shared_ce_ptr;
ConstEval &shared_ce()
{
if (!shared_ce_ptr)
shared_ce_ptr = std::make_unique<ConstEval>(module);
log_assert(shared_ce_ptr->stack.empty());
return *shared_ce_ptr;
}
// Evaluate `out_sig` under the given input assignments; returns false if
// the cut does not fully determine the output. Charges the eval budget
// by `cone_cells_estimate`.

491
passes/opt/opt_dff.cc
View file

@ -43,6 +43,91 @@ struct OptDffOptions
bool keepdc;
};
// Bit-parallel random simulation used as a cheap pre-filter for equivalence
struct BitSim {
Module *module;
SigMap &sigmap;
ModWalker &modwalker;
dict<SigBit, uint64_t> sim_vals;
uint64_t rng_state;
int max_depth;
int evals_left;
BitSim(Module *m, SigMap &sm, ModWalker &mw)
: module(m), sigmap(sm), modwalker(mw), rng_state(1337)
{
max_depth = module->design->scratchpad_get_int("opt_dff.sim_depth", 10000);
evals_left = module->design->scratchpad_get_int("opt_dff.sim_evals", 1000000);
}
uint64_t next_rand() {
uint32_t lo = mkhash_xorshift((uint32_t)rng_state);
uint32_t hi = mkhash_xorshift((uint32_t)(rng_state >> 32) ^ lo);
rng_state = ((uint64_t)hi << 32) | lo;
return rng_state;
}
uint64_t eval_bit(SigBit b, int depth = 0) {
SigBit mapped = sigmap(b);
if (mapped == State::S0) return 0ULL;
if (mapped == State::S1) return ~0ULL;
if (mapped == State::Sx || mapped == State::Sz) return 0ULL;
auto it = sim_vals.find(mapped);
if (it != sim_vals.end()) return it->second;
// Failsafe for huge designs
if (depth >= max_depth || evals_left <= 0) {
uint64_t r = next_rand();
sim_vals[mapped] = r;
return r;
}
evals_left--;
sim_vals[mapped] = 0;
uint64_t res = 0;
if (!modwalker.has_drivers(mapped)) {
res = next_rand();
} else {
auto &drivers = modwalker.signal_drivers[mapped];
if (drivers.empty()) {
res = next_rand();
} else {
auto driver = *drivers.begin();
Cell *cell = driver.cell;
if (cell->is_builtin_ff()) {
res = next_rand();
} else if (cell->type == ID($_AND_)) {
res = eval_bit(cell->getPort(ID::A)[0], depth+1) & eval_bit(cell->getPort(ID::B)[0], depth+1);
} else if (cell->type == ID($_OR_)) {
res = eval_bit(cell->getPort(ID::A)[0], depth+1) | eval_bit(cell->getPort(ID::B)[0], depth+1);
} else if (cell->type == ID($_XOR_)) {
res = eval_bit(cell->getPort(ID::A)[0], depth+1) ^ eval_bit(cell->getPort(ID::B)[0], depth+1);
} else if (cell->type == ID($_NOT_)) {
res = ~eval_bit(cell->getPort(ID::A)[0], depth+1);
} else if (cell->type == ID($_MUX_)) {
uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1);
uint64_t a = eval_bit(cell->getPort(ID::A)[0], depth+1);
uint64_t b = eval_bit(cell->getPort(ID::B)[0], depth+1);
res = (a & ~s) | (b & s);
} else if (cell->type == ID($mux)) {
uint64_t s = eval_bit(cell->getPort(ID::S)[0], depth+1);
uint64_t a = eval_bit(cell->getPort(ID::A)[driver.offset], depth+1);
uint64_t b = eval_bit(cell->getPort(ID::B)[driver.offset], depth+1);
res = (a & ~s) | (b & s);
} else {
res = next_rand();
}
}
}
sim_vals[mapped] = res;
return res;
}
};
struct OptDffWorker
{
const OptDffOptions &opt;
@ -702,7 +787,7 @@ struct OptDffWorker
if (new_cell)
dff_cells.push_back(new_cell);
log("Adding EN signal on %s (%s) from module %s (D = %s, Q = %s).\n",
log_debug("Adding EN signal on %s (%s) from module %s (D = %s, Q = %s).\n",
cell, cell->type.unescape(), module,
log_signal(new_ff.sig_d), log_signal(new_ff.sig_q));
}
@ -921,6 +1006,397 @@ struct OptDffWorker
return did_something;
}
struct EqBit {
Cell *cell;
int idx;
SigBit q;
};
// NOTE: This intentionally duplicates a subset of FfData, as flattening just the
// fields that matter for merging into a single comparable/hashable key is cheaper
struct SigKey {
enum Flag : uint16_t {
InitOne = 1u << 0,
InitX = 1u << 1,
PolClk = 1u << 2,
PolCe = 1u << 3,
PolSrst = 1u << 4,
PolArst = 1u << 5,
PolAload = 1u << 6,
PolClr = 1u << 7,
PolSet = 1u << 8,
CeOverSrst = 1u << 9,
};
SigBit clk, ce, srst, arst, aload, clr, set;
IdString cell_type; // for SR
uint16_t flags;
bool operator==(const SigKey &o) const {
return flags == o.flags && clk == o.clk && ce == o.ce && srst == o.srst && arst == o.arst
&& aload == o.aload && clr == o.clr && set == o.set && cell_type == o.cell_type;
}
Hasher hash_into(Hasher h) const {
h.eat(flags);
h.eat(clk);
h.eat(ce);
h.eat(srst);
h.eat(arst);
h.eat(aload);
h.eat(clr);
h.eat(set);
h.eat(cell_type);
return h;
}
};
bool is_def(State s) {
// Concrete constant bit (0 or 1), as opposed to x/z
return s == State::S0 || s == State::S1;
}
std::vector<std::vector<int>> gather_initial_eq_classes(std::vector<EqBit> &bits, dict<Cell *, FfData> &ff_for_cell)
{
std::vector<SigKey> keys;
// Collect FF bits eligible for merging
for (auto cell : module->selected_cells()) {
if (!cell->is_builtin_ff())
continue;
FfData ff(&initvals, cell);
if (!ff.has_clk && !ff.has_gclk)
continue;
ff_for_cell.emplace(cell, ff);
for (int i = 0; i < ff.width; i++) {
// Skip bits whose reset value is undefined (x)
if (ff.has_srst && !is_def(ff.val_srst[i])) continue;
if (ff.has_arst && !is_def(ff.val_arst[i])) continue;
// Class members are assumed equal in the current cycle and proven equal in the next, which needs
// a base case anchoring them to a common known value
bool def_init = is_def(ff.val_init[i]);
if (!def_init && !ff.has_srst && !ff.has_arst)
continue;
SigKey k = {};
// Flags
if (def_init && ff.val_init[i] == State::S1)
k.flags |= SigKey::InitOne;
else if (!def_init)
k.flags |= SigKey::InitX;
if (ff.has_clk) {
k.clk = ff.sig_clk;
if (ff.pol_clk) k.flags |= SigKey::PolClk;
}
if (ff.has_ce) {
k.ce = ff.sig_ce;
if (ff.pol_ce) k.flags |= SigKey::PolCe;
}
if (ff.has_srst) {
k.srst = ff.sig_srst;
if (ff.pol_srst) k.flags |= SigKey::PolSrst;
if (ff.ce_over_srst) k.flags |= SigKey::CeOverSrst;
}
if (ff.has_arst) {
k.arst = ff.sig_arst;
if (ff.pol_arst) k.flags |= SigKey::PolArst;
}
if (ff.has_aload) {
k.aload = ff.sig_aload;
if (ff.pol_aload) k.flags |= SigKey::PolAload;
}
if (ff.has_sr) {
k.clr = ff.sig_clr[i];
k.set = ff.sig_set[i];
k.cell_type = cell->type;
if (ff.pol_clr) k.flags |= SigKey::PolClr;
if (ff.pol_set) k.flags |= SigKey::PolSet;
}
bits.push_back({cell, i, ff.sig_q[i]});
keys.push_back(k);
}
}
dict<SigKey, std::vector<int>> buckets;
for (int i = 0; i < GetSize(bits); i++)
buckets[keys[i]].push_back(i);
std::vector<std::vector<int>> classes;
for (auto &kv : buckets)
if (GetSize(kv.second) >= 2)
classes.push_back(std::move(kv.second));
return classes;
}
std::vector<std::vector<int>> filter_classes_sim(
const std::vector<std::vector<int>> &classes,
const std::vector<EqBit> &bits,
const dict<Cell *, FfData> &ff_for_cell,
ModWalker &modwalker
) {
BitSim sim(module, sigmap, modwalker);
// Assume same class
for (auto &cls : classes) {
uint64_t class_q_val = sim.next_rand();
for (int idx : cls) {
sim.sim_vals[sigmap(bits[idx].q)] = class_q_val;
}
}
std::vector<std::vector<int>> refined_classes;
for (auto &cls : classes) {
dict<uint64_t, std::vector<int>> sim_buckets;
for (int idx : cls) {
const EqBit &eb = bits[idx];
const FfData &ff = ff_for_cell.at(eb.cell);
uint64_t n_val = sim.eval_bit(ff.sig_d[eb.idx]);
if (ff.has_aload) {
uint64_t al = sim.eval_bit(ff.sig_aload);
if (!ff.pol_aload) al = ~al;
uint64_t ad = sim.eval_bit(ff.sig_ad[eb.idx]);
n_val = (n_val & ~al) | (ad & al);
}
if (ff.has_arst) {
uint64_t ar = sim.eval_bit(ff.sig_arst);
if (!ff.pol_arst) ar = ~ar;
uint64_t ar_val = (ff.val_arst[eb.idx] == State::S1) ? ~0ULL : 0ULL;
n_val = (n_val & ~ar) | (ar_val & ar);
}
if (ff.has_sr) {
uint64_t clr = sim.eval_bit(ff.sig_clr[eb.idx]);
if (!ff.pol_clr) clr = ~clr;
uint64_t set = sim.eval_bit(ff.sig_set[eb.idx]);
if (!ff.pol_set) set = ~set;
n_val = ~clr & (set | n_val);
}
if (ff.has_srst) {
uint64_t srst = sim.eval_bit(ff.sig_srst);
if (!ff.pol_srst) srst = ~srst;
uint64_t srst_val = (ff.val_srst[eb.idx] == State::S1) ? ~0ULL : 0ULL;
n_val = (n_val & ~srst) | (srst_val & srst);
}
sim_buckets[n_val].push_back(idx);
}
for (auto &kv : sim_buckets)
if (GetSize(kv.second) >= 2)
refined_classes.push_back(std::move(kv.second));
}
return refined_classes;
}
std::vector<std::vector<int>> filter_classes_sat(
std::vector<std::vector<int>> classes,
const std::vector<EqBit> &bits,
const dict<Cell *, FfData> &ff_for_cell,
ModWalker &modwalker
) {
QuickConeSat qcsat(modwalker);
std::vector<int> q_lit(bits.size(), -1);
std::vector<int> n_lit(bits.size(), -1);
// Build the next-state function n_lit[idx] of every candidate bit by
// folding the FF's control logic on top of the D input (-> next value)
// Two bits are equivalent if their next states always agree whenever their
// current states (and those of every other candidate pair) agree
for (auto &cls : classes) {
for (int idx : cls) {
const EqBit &eb = bits[idx];
const FfData &ff = ff_for_cell.at(eb.cell);
q_lit[idx] = qcsat.importSigBit(eb.q);
int n = qcsat.importSigBit(ff.sig_d[eb.idx]);
if (ff.has_aload) {
int al = qcsat.importSigBit(ff.sig_aload);
if (!ff.pol_aload) al = qcsat.ez->NOT(al);
n = qcsat.ez->ITE(al, qcsat.importSigBit(ff.sig_ad[eb.idx]), n);
}
if (ff.has_arst) {
int ar = qcsat.importSigBit(ff.sig_arst);
if (!ff.pol_arst) ar = qcsat.ez->NOT(ar);
n = qcsat.ez->ITE(ar, qcsat.ez->value(ff.val_arst[eb.idx] == State::S1), n);
}
if (ff.has_sr) {
int clr = qcsat.importSigBit(ff.sig_clr[eb.idx]);
if (!ff.pol_clr) clr = qcsat.ez->NOT(clr);
int set = qcsat.importSigBit(ff.sig_set[eb.idx]);
if (!ff.pol_set) set = qcsat.ez->NOT(set);
n = qcsat.ez->AND(qcsat.ez->NOT(clr), qcsat.ez->OR(set, n));
}
if (ff.has_srst) {
int srst = qcsat.importSigBit(ff.sig_srst);
if (!ff.pol_srst) srst = qcsat.ez->NOT(srst);
n = qcsat.ez->ITE(srst, qcsat.ez->value(ff.val_srst[eb.idx] == State::S1), n);
}
n_lit[idx] = n;
}
}
qcsat.prepare();
// Assume the induction hypo (that every current class is internally equal in the present cycle), and try
// to prove that the members of each class therefore also agree in the next cycle
// A class survives only if no counterexample exists under that hypo, so combined with the common init/reset
// value that every class shares, this makes the equality an inductive invariant -> bits are eq and safe to merge
std::vector<int> worklist;
std::vector<bool> in_worklist(GetSize(classes), true);
for (int i = 0; i < GetSize(classes); i++)
worklist.push_back(i);
while (!worklist.empty()) {
int cls_idx = worklist.back();
worklist.pop_back();
in_worklist[cls_idx] = false;
auto &cls = classes[cls_idx];
if (GetSize(cls) < 2) continue;
// Induction hypo: assume every candidate class is equal
std::vector<int> assumptions;
for (auto &c : classes) {
if (GetSize(c) < 2) continue;
int rep = c[0];
for (int k = 1; k < GetSize(c); k++)
assumptions.push_back(qcsat.ez->IFF(q_lit[rep], q_lit[c[k]]));
}
// Scan the class members against the representative and issue a query per pair,
// stopping early at the first counterexample, which is reused to split the entire
// class at once
int rep = cls[0];
for (int i = 1; i < GetSize(cls); i++) {
if (n_lit[rep] == n_lit[cls[i]])
continue;
// Can the next state of the rep and this member ever differ?
int query = qcsat.ez->XOR(n_lit[rep], n_lit[cls[i]]);
// Capture every member's next-state value in that model so one counterexample
// partitions the whole class
std::vector<int> modelExprs;
for (int b : cls)
modelExprs.push_back(n_lit[b]);
std::vector<bool> modelVals;
assumptions.push_back(query);
if (qcsat.ez->solve(modelExprs, modelVals, assumptions)) {
// SAT -> partition entire class
std::vector<int> sub0;
std::vector<int> sub1;
for (size_t b_idx = 0; b_idx < cls.size(); b_idx++) {
if (modelVals[b_idx])
sub1.push_back(cls[b_idx]);
else
sub0.push_back(cls[b_idx]);
}
classes[cls_idx] = std::move(sub0);
classes.push_back(std::move(sub1));
in_worklist.push_back(false);
// Partition was split -> the induction hypo weakened
for (int j = 0; j < GetSize(classes); j++) {
if (GetSize(classes[j]) >= 2 && !in_worklist[j]) {
worklist.push_back(j);
in_worklist[j] = true;
}
}
break; // Process new splits
}
assumptions.pop_back(); // Remove query for the next pairwise check if UNSAT
}
}
return classes;
}
bool apply_eq_merges(const std::vector<std::vector<int>> &classes, const std::vector<EqBit> &bits, dict<Cell *, FfData> &ff_for_cell)
{
bool any_change = false;
dict<Cell *, std::set<int>> remove_bits;
// Drive every non-rep Q from its class rep, drop merged bits from their FFs
for (auto &cls : classes) {
if (GetSize(cls) < 2)
continue;
SigBit rep_q = bits[cls[0]].q;
any_change = true;
for (int k = 1; k < GetSize(cls); k++) {
const EqBit &eb = bits[cls[k]];
initvals.remove_init(eb.q);
module->connect(eb.q, rep_q);
remove_bits[eb.cell].insert(eb.idx);
}
}
for (auto &kv : remove_bits) {
Cell *cell = kv.first;
const std::set<int> &drop = kv.second;
FfData &ff = ff_for_cell.at(cell);
std::vector<int> keep;
for (int i = 0; i < ff.width; i++)
if (!drop.count(i))
keep.push_back(i);
if (keep.empty()) {
module->remove(cell);
} else {
FfData new_ff = ff.slice(keep);
new_ff.cell = cell;
new_ff.emit();
}
}
return any_change;
}
bool run_eqbits()
{
if (!opt.sat)
return false;
std::vector<EqBit> bits;
dict<Cell *, FfData> ff_for_cell;
std::vector<std::vector<int>> classes = gather_initial_eq_classes(bits, ff_for_cell);
if (classes.empty())
return false;
ModWalker modwalker(module->design, module);
// Simulation prepass
classes = filter_classes_sim(classes, bits, ff_for_cell, modwalker);
if (classes.empty())
return false;
// SAT prove
classes = filter_classes_sat(std::move(classes), bits, ff_for_cell, modwalker);
if (classes.empty())
return false;
return apply_eq_merges(classes, bits, ff_for_cell);
}
};
struct OptDffPass : public Pass {
@ -950,7 +1426,9 @@ struct OptDffPass : public Pass {
log("\n");
log(" -sat\n");
log(" additionally invoke SAT solver to detect and remove flip-flops (with\n");
log(" non-constant inputs) that can also be replaced with a constant driver\n");
log(" non-constant inputs) that can also be replaced with a constant driver,\n");
log(" or merged with equivalent flip-flops. this reasons in 2-valued logic\n");
log(" and may resolve don't-care bits, so it is incompatible with -keepdc.\n");
log("\n");
log(" -keepdc\n");
log(" some optimizations change the behavior of the circuit with respect to\n");
@ -982,6 +1460,13 @@ struct OptDffPass : public Pass {
}
extra_args(args, argidx, design);
// The SAT engine reasons in 2-valued logic (a constant x is treated as
// 0), so it can resolve don't-care bits to concrete values -- exactly
// what -keepdc promises not to do. Refuse the combination rather than
// silently ignore -keepdc.
if (opt.sat && opt.keepdc)
log_cmd_error("The -sat and -keepdc options are mutually exclusive.\n");
bool did_something = false;
for (auto mod : design->selected_modules()) {
OptDffWorker worker(opt, mod);
@ -989,6 +1474,8 @@ struct OptDffPass : public Pass {
did_something = true;
if (worker.run_constbits())
did_something = true;
if (worker.run_eqbits())
did_something = true;
}
if (did_something)

130
passes/opt/opt_first_fit_alloc.cc
View file

@ -165,6 +165,56 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
return r;
}
// ----------------------------------------------------------------
// Reference semantics of the "coalesce matrix" allocator variant.
//
// Leadership and slot assignment are identical to the greedy first-fit
// above, but the per-lane rank does NOT depend on the lane's own enable:
// every lane k (enabled or not) inherits the slot of the first leader at
// or before k (in priority order) whose category matches cat[k]. This
// models RTL that precomputes a per-leader "same_cat[i][k]" mask (gated
// only on the leader's enable) and forward-coalesces into lane k without
// re-checking en[k]. There is no broadcast lane in this variant.
// ----------------------------------------------------------------
AllocResult compute_alloc_coalesce(const vector<int> &en, const vector<int> &cat,
int n) const
{
AllocResult r = compute_alloc(en, vector<int>(n, 0), cat, n);
for (int k = 0; k < n; k++) {
r.dsel[k] = 0;
for (int i = 0; i <= k; i++)
if (r.leader[i] && cat[i] == cat[k]) {
r.dsel[k] = r.slot[i];
break;
}
}
return r;
}
AllocResult compute_alloc_coalesce_dir(const vector<int> &en, const vector<int> &cat,
int n, bool msb_first) const
{
if (!msb_first)
return compute_alloc_coalesce(en, cat, n);
vector<int> er(n), cr(n);
for (int i = 0; i < n; i++) {
er[i] = en[n - 1 - i];
cr[i] = cat[n - 1 - i];
}
AllocResult rr = compute_alloc_coalesce(er, cr, n);
AllocResult r;
r.dsel.assign(n, 0);
r.leader.assign(n, 0);
r.slot.assign(n, 0);
r.M = rr.M;
for (int i = 0; i < n; i++) {
r.dsel[i] = rr.dsel[n - 1 - i];
r.leader[i] = rr.leader[n - 1 - i];
r.slot[i] = rr.slot[n - 1 - i];
}
return r;
}
// ----------------------------------------------------------------
// Test vectors. `nval` is the number of distinct label values (2^c for
// the category, 2^a for the xbar attribute). The vectors deliberately
@ -412,6 +462,10 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
int field_w = 0;
SigSpec en_sig, bc_sig, cat_sig;
bool has_bc = false;
// Enable-independent forward coalescing: lanes inherit the slot of the
// first same-category leader at or before them in priority order,
// regardless of their own enable (the "same_cat matrix" RTL shape).
bool coalesce = false;
int c = 0;
bool msb_first = false;
Cell *anchor = nullptr;
@ -594,9 +648,39 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
{
Cell *anchor = rg.anchor;
int n = rg.n, c = rg.c, w = rg.field_w;
SigSpec cat = sigmap(rg.cat_sig);
// Enable-independent forward coalescing: lane k inherits the slot of the
// unique same-category leader at or before k in priority order, with no
// enable/broadcast gating. The priority position of a lane is a compile-
// time constant, so the "leader at or before k" restriction is static.
if (rg.coalesce) {
auto pos = [&](int l) { return rg.msb_first ? (n - 1 - l) : l; };
SigSpec out;
for (int k = 0; k < n; k++) {
SigSpec cat_k = cat.extract(k * c, c);
vector<SigBit> g(n, SigBit(State::S0));
for (int i = 0; i < n; i++) {
if (pos(i) > pos(k))
continue;
SigBit eq = emit_eq_sig(anchor, cat.extract(i * c, c), cat_k);
g[i] = emit_and(anchor, leader[i], eq);
}
SigSpec rank(Const(0, cnt_w));
for (int b = 0; b < cnt_w; b++) {
SigSpec terms;
for (int i = 0; i < n; i++)
if (pos(i) <= pos(k))
terms.append(emit_and(anchor, g[i], slot[i][b]));
rank[b] = emit_reduce_or(anchor, terms);
}
out.append(zext_sig(rank, w));
}
return out;
}
SigSpec en = sigmap(rg.en_sig);
SigSpec bc = rg.has_bc ? sigmap(rg.bc_sig) : SigSpec();
SigSpec cat = sigmap(rg.cat_sig);
// bc rank: (M>=1) ? M-1 : 0
SigBit any_leader = emit_reduce_or(anchor, total);
@ -707,15 +791,22 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
internal_bits.insert(bit);
pool<SigSpec> seen;
auto all_internal = [&](const SigSpec &s) {
// Accept a bus bit if it is a cone-internal (computed) signal or a
// primary input / undriven bit. The enable/broadcast lanes are usually
// computed signals (e.g. valid & format), but some RTL drives the scan
// straight from a top-level request port (e.g. lane_en), so input buses
// must be admissible too. Inputs sort shallowest (depth 0) below, so they
// survive the candidate cap ahead of the deep intermediate nets.
auto all_internal_or_input = [&](const SigSpec &s) {
for (auto bit : s)
if (!bit.wire || !internal_bits.count(bit))
if (!bit.wire || (!internal_bits.count(bit) &&
bit_to_driver.at(bit, nullptr) != nullptr))
return false;
return true;
};
auto add = [&](const SigSpec &sig, const std::string &nm) {
SigSpec s = sigmap(sig);
if (GetSize(s) != n || !sig_bus_ok(s) || !all_internal(s))
if (GetSize(s) != n || !sig_bus_ok(s) || !all_internal_or_input(s))
return;
if (!seen.insert(s).second)
return;
@ -868,17 +959,28 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
bool fpm = fingerprint_dsel(ce, root_sig, n, field_w, en_bus.sig,
bc_bus ? bc_bus->sig : SigSpec(), bc_bus != nullptr,
cat_sig, c, msb_first, cone_est);
log_debug(" en=%s bc=%s cat=%dx%d %s: fingerprint %s\n", en_bus.name.c_str(),
// Standard first-fit failed: try the enable-independent
// forward-coalescing variant (no broadcast lane).
bool coalesce = false;
if (!fpm && bc_bus == nullptr) {
fpm = fingerprint_dsel(ce, root_sig, n, field_w, en_bus.sig,
SigSpec(), false, cat_sig, c, msb_first,
cone_est, /*coalesce=*/true);
coalesce = fpm;
}
log_debug(" en=%s bc=%s cat=%dx%d %s: fingerprint %s%s\n", en_bus.name.c_str(),
bc_bus ? bc_bus->name.c_str() : "-", n, c,
msb_first ? "MSB" : "LSB", fpm ? "MATCH" : "no");
msb_first ? "MSB" : "LSB", fpm ? "MATCH" : "no",
coalesce ? " (coalesce)" : "");
if (fpm) {
out.dsel_sig = root_sig;
out.dsel_name = root_name;
out.n = n;
out.field_w = field_w;
out.en_sig = en_bus.sig;
out.bc_sig = bc_bus ? bc_bus->sig : SigSpec();
out.has_bc = (bc_bus != nullptr);
out.bc_sig = (!coalesce && bc_bus) ? bc_bus->sig : SigSpec();
out.has_bc = (!coalesce && bc_bus != nullptr);
out.coalesce = coalesce;
out.cat_sig = cat_sig;
out.c = c;
out.msb_first = msb_first;
@ -901,7 +1003,8 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
// Any eval failure or single mismatch rejects the candidate.
bool fingerprint_dsel(ConstEval &ce, const SigSpec &root, int n, int field_w,
const SigSpec &en_sig, const SigSpec &bc_sig, bool has_bc,
const SigSpec &cat_sig, int c, bool msb_first, int64_t cone_est)
const SigSpec &cat_sig, int c, bool msb_first, int64_t cone_est,
bool coalesce = false)
{
int nval = 1 << c;
vector<TestVector> vs = make_vectors(n, nval, has_bc);
@ -920,7 +1023,9 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
if (!eval_root(ce, sets, root, res, cone_est))
return false;
AllocResult ar = compute_alloc_dir(tv.en, tv.bc, tv.label, n, msb_first);
AllocResult ar = coalesce
? compute_alloc_coalesce_dir(tv.en, tv.label, n, msb_first)
: compute_alloc_dir(tv.en, tv.bc, tv.label, n, msb_first);
for (int k = 0; k < n; k++) {
int got = lane_val(res, k, field_w);
int exp = ar.dsel[k] & ((1 << field_w) - 1);
@ -1239,11 +1344,12 @@ struct OptFirstFitAllocWorker : CutRegionWorker {
claim_region(rg.dsel_sig, rg.dsel_cut_cells);
regions_rewritten++;
log(" %s: %s <- first_fit_alloc(en=%s%s, cat=%dx%d, %s)\n",
log(" %s: %s <- first_fit_alloc(en=%s%s, cat=%dx%d, %s%s)\n",
log_id(module), rg.dsel_name.c_str(),
log_signal(rg.en_sig),
rg.has_bc ? stringf(", bc=%s", log_signal(rg.bc_sig)).c_str() : "",
rg.n, rg.c, rg.msb_first ? "MSB-first" : "LSB-first");
rg.n, rg.c, rg.msb_first ? "MSB-first" : "LSB-first",
rg.coalesce ? ", coalesce" : "");
if (have_xbar) {
SigSpec new_xbar = emit_xbar(rg, xb, leader, slot, cnt_w);

329
passes/opt/opt_prienc.cc
View file

@ -82,6 +82,7 @@ struct OptPriEncWorker {
// Configuration.
bool detect_clz = true;
bool detect_ctz = true;
bool detect_rr = true;
int max_input_width = 256;
int min_input_width = 4;
@ -242,6 +243,56 @@ struct OptPriEncWorker {
return vs;
}
// ConstEval::set() requires every (sigmap-canonical) bit it pins to be a
// distinct free wire bit. Real designs can tie parts of a bus to constants
// or alias nets together, so guard the fingerprint inputs: reject signals
// containing constant or repeated bits, and (across the whole set) any
// overlap between them. This prevents a ConstEval assertion; skipping an
// unclean candidate only forgoes a possible rewrite, never yields a wrong
// one.
static bool clean_set_signals(std::initializer_list<const SigSpec*> sigs) {
pool<SigBit> seen;
for (const SigSpec* sp : sigs)
for (auto bit : *sp) {
if (bit.wire == nullptr) return false;
if (!seen.insert(bit).second) return false;
}
return true;
}
// A set of signals is a valid ConstEval "cut" to pin as free inputs only if
// pinning them can never collide with a value ConstEval derives while
// evaluating the cone. ConstEval::eval() re-computes and re-set()s the FULL
// output of any combinational cell it needs: so if a pinned bit is a
// combinational-cell output and a *sibling* output bit of that same cell
// lies outside the cut (and is pulled into the cone), evaluating the sibling
// re-sets the pinned bit to the cell's real value, which contradicts the
// free value we pinned -> the ConstEval assertion in set() fires.
//
// A bit is a safe leaf when it is a primary input, sequential-cell output or
// undriven (all absent from bit_to_driver, which holds combinational drivers
// only). A combinational-cell output is safe only if that cell's entire
// output lies within the cut. `cut` must be the union of every signal pinned
// together before a shared eval.
bool is_valid_consteval_cut(const SigSpec& cut) {
pool<SigBit> cut_bits;
for (auto bit : cut)
if (bit.wire) cut_bits.insert(bit);
for (auto bit : cut) {
if (bit.wire == nullptr) return false;
auto it = bit_to_driver.find(bit);
if (it == bit_to_driver.end()) continue; // safe leaf
Cell* d = it->second;
for (auto& conn : d->connections()) {
if (!d->output(conn.first)) continue;
for (auto ob : sigmap(conn.second))
if (ob.wire && !cut_bits.count(ob))
return false;
}
}
return true;
}
// Run all candidate test vectors through ConstEval and try to match each of
// the four PE variants against the recorded outputs. Returns the matched
// variant, or NONE.
@ -256,6 +307,12 @@ struct OptPriEncWorker {
if (!clz_full_ok && !ctz_full_ok && !clz_short_ok && !ctz_short_ok)
return PEVariant::NONE;
if (!clean_set_signals({&T_sig}))
return PEVariant::NONE;
if (!is_valid_consteval_cut(T_sig))
return PEVariant::NONE;
auto vs = gen_test_vectors(N);
for (auto& v : vs) {
ce.push();
@ -390,6 +447,177 @@ struct OptPriEncWorker {
return full;
}
// ------------------------------------------------------------------
// Round-robin (rotated priority) detection + rewrite.
//
// A round-robin arbiter grants the first set request bit scanning
// *upward* (increasing index, wrapping) starting just after a stored
// pointer `s` (= idx_last):
//
// grant = anyreq ? (first set bit at index > s, else first set
// bit overall) : 0
// idx_next = anyreq ? grant : s
//
// RTL usually spells this as a DEPTH-iteration loop that walks `idx`
// downward from idx_last with wraparound and keeps the last hit, which
// elaborates into a serial mux/shift chain of depth ~DEPTH. The rewrite
// below is log-depth:
//
// above[i] = (i > s) (per-bit threshold mask)
// mask_hi = req & above
// grant = anyreq ? (|mask_hi ? ctz(mask_hi) : ctz(req)) : 0
//
// where ctz() reuses the log-depth CTZ network. For power-of-2 DEPTH the
// rewrite is fully combinationally equivalent for every pointer value;
// for non-power-of-2 DEPTH it is equivalent for every *reachable* pointer
// (idx_last only ever holds a valid index in [0,DEPTH)), which is the
// range the fingerprint checks. Detection therefore sweeps s over
// [0,DEPTH) only.
// ------------------------------------------------------------------
// kind: 0 = grant, 1 = idx_next.
int rr_expected(const Const& reqv, int s, int N, int W, int kind) {
auto bits = reqv.to_bits();
int lo_all = -1, lo_hi = -1;
for (int i = 0; i < N; i++) {
bool set = (i < (int)bits.size() && bits[i] == State::S1);
if (!set) continue;
if (lo_all < 0) lo_all = i;
if (i > s && lo_hi < 0) lo_hi = i;
}
bool anyreq = (lo_all >= 0);
int gsel = (lo_hi >= 0) ? lo_hi : (lo_all >= 0 ? lo_all : 0);
int val = kind == 0 ? (anyreq ? gsel : 0)
: (anyreq ? gsel : s);
return val & ((W >= 31) ? -1 : ((1 << W) - 1));
}
// Returns matched kind (0 grant, 1 idx_next), or -1 for no match.
int fingerprint_rr(SigSpec req_sig, SigSpec start_sig, SigSpec S_sig,
int N, int W) {
ConstEval ce(module);
if (!clean_set_signals({&req_sig, &start_sig}))
return -1;
SigSpec cut = req_sig;
cut.append(start_sig);
if (!is_valid_consteval_cut(cut))
return -1;
bool ok0 = true, ok1 = true;
auto deck = gen_test_vectors(N);
int checks = 0;
for (auto& rv : deck) {
for (int s = 0; s < N; s++) {
ce.push();
ce.set(req_sig, rv);
ce.set(start_sig, Const(s, W));
SigSpec out = S_sig, undef;
bool ok = ce.eval(out, undef);
ce.pop();
if (!ok || !out.is_fully_const()) return -1;
int ov = out.as_const().as_int();
if (ok0 && ov != rr_expected(rv, s, N, W, 0)) ok0 = false;
if (ok1 && ov != rr_expected(rv, s, N, W, 1)) ok1 = false;
checks++;
if (!ok0 && !ok1) return -1;
}
}
if (checks < 2 * N) return -1;
if (ok0) return 0;
if (ok1) return 1;
return -1;
}
// Emit the log-depth round-robin network. Shared subexpressions across
// the grant / idx_next pair for the same (req, start) inputs are cached.
dict<std::pair<Wire*, Wire*>, std::tuple<SigSpec, SigSpec, SigBit>> rr_core_cache;
SigSpec emit_rr(Wire* req_wire, Wire* start_wire, int N, int W, int kind) {
SigSpec req = sigmap(SigSpec(req_wire));
SigSpec s = sigmap(SigSpec(start_wire));
SigSpec gsel;
SigBit anyreq;
auto key = std::make_pair(req_wire, start_wire);
auto it = rr_core_cache.find(key);
if (it != rr_core_cache.end()) {
SigSpec cached_gsel;
std::tie(cached_gsel, std::ignore, anyreq) = it->second;
gsel = cached_gsel;
} else {
SigSpec above;
for (int i = 0; i < N; i++) {
above.append(module->Lt(NEW_ID2_SUFFIX("rrabove"), s, SigSpec(Const(i, W))));
cells_added++;
}
SigSpec mask_hi = module->And(NEW_ID2_SUFFIX("rrmask"), req, above);
cells_added++;
SigSpec cz_hi = emit_ctz_full(mask_hi, N);
SigSpec cz_all = emit_ctz_full(req, N);
auto low_w = [&](SigSpec x) {
if (GetSize(x) > W) return x.extract(0, W);
while (GetSize(x) < W) x.append(SigSpec(State::S0));
return x;
};
cz_hi = low_w(cz_hi);
cz_all = low_w(cz_all);
SigBit any_hi = module->ReduceOr(NEW_ID2_SUFFIX("rranyhi"), mask_hi);
cells_added++;
anyreq = module->ReduceOr(NEW_ID2_SUFFIX("rranyreq"), req);
cells_added++;
// any_hi ? cz_hi : cz_all
gsel = module->Mux(NEW_ID2_SUFFIX("rrgsel"), cz_all, cz_hi, any_hi);
cells_added++;
rr_core_cache[key] = std::make_tuple(gsel, SigSpec(), anyreq);
}
SigSpec fallback = (kind == 0) ? SigSpec(Const(0, W)) : s;
// anyreq ? gsel : fallback
SigSpec res = module->Mux(NEW_ID2_SUFFIX("rrsel"), fallback, gsel, anyreq);
cells_added++;
return res;
}
// Generalisation of cone_depends_only_on_T to a set of allowed leaf bits.
bool cone_depends_only_on_set(SigSpec S_sig, const pool<SigBit>& allowed) {
pool<SigBit> visited;
std::queue<SigBit> worklist;
for (auto bit : sigmap(S_sig)) {
if (!bit.wire) continue;
if (visited.insert(bit).second) worklist.push(bit);
}
while (!worklist.empty()) {
SigBit bit = worklist.front();
worklist.pop();
if (allowed.count(bit)) continue;
if (input_port_bits.count(bit)) return false;
auto it = bit_to_driver.find(bit);
if (it == bit_to_driver.end()) return false;
Cell* drv = it->second;
if (sequential_cells.count(drv)) return false;
for (auto& conn : drv->connections()) {
if (!drv->input(conn.first)) continue;
for (auto in_bit : sigmap(conn.second)) {
if (!in_bit.wire) continue;
if (visited.insert(in_bit).second) worklist.push(in_bit);
}
}
}
return true;
}
struct RRRewrite {
Wire* S_wire;
Wire* req_wire;
Wire* start_wire;
int N;
int W;
int kind;
Cell* sole_driver;
IdString out_port;
};
struct Rewrite {
Wire* S_wire;
Wire* T_wire;
@ -584,6 +812,77 @@ struct OptPriEncWorker {
}
}
// Stage 3: round-robin (rotated priority) detection. Reuses the same
// candidate cones; an output S is grant/idx_next of a round-robin
// arbiter over a wide request bus `req` and a same-width-as-S pointer
// `start`, both bottoming out the cone.
vector<RRRewrite> rr_rewrites;
if (detect_rr) {
const int max_pairs = 64;
for (auto& cand : candidates) {
if (claimed_outputs.count(cand.S_wire)) continue;
if (claimed_drivers.count(cand.sole_driver)) continue;
int W = cand.S_wire->width;
if (W < 2 || W > max_W) continue;
SigSpec S_sig = sigmap(SigSpec(cand.S_wire));
vector<Wire*> req_cands, start_cands;
for (Wire* w : wires_snapshot) {
if (w == cand.S_wire) continue;
bool all_in = true;
for (auto bit : sigmap(SigSpec(w)))
if (!cand.cone_bits.count(bit)) { all_in = false; break; }
if (!all_in) continue;
int wn = w->width;
if (wn >= min_input_width && wn <= max_input_width &&
clog2_int(wn) == W)
req_cands.push_back(w);
if (wn == W)
start_cands.push_back(w);
}
std::sort(req_cands.begin(), req_cands.end(),
[](Wire* a, Wire* b) { return a->width > b->width; });
bool matched = false;
for (Wire* req_wire : req_cands) {
if (matched) break;
int N = req_wire->width;
SigSpec req_sig = sigmap(SigSpec(req_wire));
pool<SigBit> req_bits;
for (auto bit : req_sig)
if (bit.wire) req_bits.insert(bit);
// Per-req_wire fingerprint budget: a start-candidate-heavy
// first req size must not exhaust a shared budget and starve
// later (narrower) req sizes.
int pairs = 0;
for (Wire* start_wire : start_cands) {
if (start_wire == req_wire) continue;
if (++pairs > max_pairs) break;
SigSpec start_sig = sigmap(SigSpec(start_wire));
pool<SigBit> allowed = req_bits;
for (auto bit : start_sig)
if (bit.wire) allowed.insert(bit);
if (!cone_depends_only_on_set(S_sig, allowed)) continue;
int kind = fingerprint_rr(req_sig, start_sig, S_sig, N, W);
if (kind < 0) continue;
log(" %s: %s <- round_robin_%s(req=%s, start=%s) [N=%d, W=%d]\n",
log_id(module), log_id(cand.S_wire),
kind == 0 ? "grant" : "next",
log_id(req_wire), log_id(start_wire), N, W);
rr_rewrites.push_back({cand.S_wire, req_wire, start_wire, N, W,
kind, cand.sole_driver, cand.out_port});
claimed_outputs.insert(cand.S_wire);
claimed_drivers.insert(cand.sole_driver);
matched = true;
break;
}
}
}
}
// Apply rewrites. We collected first to avoid the index growing stale
// while we add new cells/wires.
for (auto& r : rewrites) {
@ -595,6 +894,14 @@ struct OptPriEncWorker {
module->connect(SigSpec(r.S_wire), new_S);
regions_rewritten++;
}
for (auto& r : rr_rewrites) {
cell = r.sole_driver;
SigSpec new_S = emit_rr(r.req_wire, r.start_wire, r.N, r.W, r.kind);
Wire* dangling = module->addWire(NEW_ID2_SUFFIX("dangling"), r.W);
r.sole_driver->setPort(r.out_port, dangling);
module->connect(SigSpec(r.S_wire), new_S);
regions_rewritten++;
}
}
};
@ -624,11 +931,23 @@ struct OptPriEncPass : public Pass {
log(" ctz_full : symmetric to clz_full from the LSB side.\n");
log(" ctz_short : symmetric to clz_short from the LSB side.\n");
log("\n");
log("In addition, the pass detects round-robin (rotated priority)\n");
log("arbiters: grant / idx_next = first set request bit scanning upward\n");
log("(wrapping) from just after a stored pointer idx_last. RTL typically\n");
log("spells this as a DEPTH-iteration idx-- loop over req[idx], which\n");
log("elaborates into a serial chain; it is replaced with a log-depth\n");
log("threshold-mask + CTZ network. For power-of-2 DEPTH the rewrite is\n");
log("equivalent for every pointer value; for other widths it is\n");
log("equivalent for every reachable pointer (idx_last in [0,DEPTH)).\n");
log("\n");
log(" -clz\n");
log(" detect CLZ patterns only.\n");
log(" detect CLZ patterns only (also disables round-robin).\n");
log("\n");
log(" -ctz\n");
log(" detect CTZ patterns only.\n");
log(" detect CTZ patterns only (also disables round-robin).\n");
log("\n");
log(" -no-rr\n");
log(" disable round-robin / rotated-priority detection.\n");
log("\n");
log(" -max-width N\n");
log(" maximum input bus width to consider (default 64).\n");
@ -648,6 +967,7 @@ struct OptPriEncPass : public Pass {
bool only_clz = false;
bool only_ctz = false;
bool no_rr = false;
int max_width = 64;
int min_width = 4;
@ -655,6 +975,7 @@ struct OptPriEncPass : public Pass {
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-clz") { only_clz = true; continue; }
if (args[argidx] == "-ctz") { only_ctz = true; continue; }
if (args[argidx] == "-no-rr") { no_rr = true; continue; }
if (args[argidx] == "-max-width" && argidx + 1 < args.size()) {
max_width = std::stoi(args[++argidx]); continue;
}
@ -664,6 +985,9 @@ struct OptPriEncPass : public Pass {
break;
}
extra_args(args, argidx, design);
// -clz / -ctz select a single leading/trailing variant and disable
// round-robin detection unless the user re-enables it explicitly.
if (only_clz || only_ctz) no_rr = true;
int total_regions = 0;
int total_cells_added = 0;
@ -671,6 +995,7 @@ struct OptPriEncPass : public Pass {
OptPriEncWorker worker(module);
worker.detect_clz = !only_ctz;
worker.detect_ctz = !only_clz;
worker.detect_rr = !no_rr;
worker.max_input_width = max_width;
worker.min_input_width = min_width;
worker.run();

464
passes/opt/opt_priokey.cc Normal file
View file

@ -0,0 +1,464 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2026 Akash Levy <akash@silimate.com>
*
* 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/consteval.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
// ---------------------------------------------------------------------------
// opt_priokey: priority-by-key deduplication ("taken" accumulator) rewrite.
//
// RTL that resolves conflicts between several sources that each carry a small
// key is often written as a serial scan over a wide one-hot "set" accumulator
// indexed by the key:
//
// taken = '0;
// for (i = 0; i < P; i++)
// if (act[i] && !taken[key[i]]) begin // this source wins its key
// taken[key[i]] = 1'b1; // claim the key
// ...use win[i]...
// end
//
// This elaborates into a serial chain of dynamic-index reads (taken[key[i]] =
// $shiftx into an S-bit vector) and dynamic-index writes (taken | 1<<key[i],
// muxed by the winner). Each dynamic access is an O(log S) wide mux, so the
// critical path grows with both P and S even though the underlying decision
// only needs pairwise key comparisons:
//
// taken[key[j]] (at step j) == OR over i<j of ( win_guard[i] & key[i]==key[j] )
//
// The pass identifies the accumulator chain, then replaces each dynamic read
// with the equivalent pairwise-key-compare reduction, eliminating the wide
// dynamic indexing entirely. Correctness of every rewrite is validated by a
// ConstEval fingerprint (the read output vs. the compare reduction, over the
// free key/guard signals) before it is applied. For non-power-of-two S the
// rewrite is equivalent over the reachable key range [0,S), which the
// fingerprint sweeps.
// ---------------------------------------------------------------------------
struct OptPrioKeyWorker {
Module *module;
SigMap sigmap;
Cell *cell = nullptr;
dict<SigBit, Cell *> bit_to_driver;
int max_slots = 1 << 14; // maximum accumulator width S
int max_chain = 256; // maximum number of sources P
int fp_trials = 256; // ConstEval validation vectors
bool strict = false; // validate over the full key range, not [0,S)
int regions_rewritten = 0;
int cells_added = 0;
OptPrioKeyWorker(Module *m) : module(m), sigmap(m) { build_index(); }
void build_index() {
for (auto c : module->cells())
for (auto &conn : c->connections())
if (c->output(conn.first))
for (auto bit : sigmap(conn.second))
if (bit.wire) bit_to_driver[bit] = c;
}
Cell *sole_driver(const SigSpec &s) {
SigSpec ss = sigmap(s);
Cell *d = nullptr;
for (auto bit : ss) {
if (!bit.wire) return nullptr;
auto it = bit_to_driver.find(bit);
if (it == bit_to_driver.end()) return nullptr;
if (d && d != it->second) return nullptr;
d = it->second;
}
return d;
}
bool is_all_zero(const SigSpec &s) {
for (auto bit : s)
if (bit != SigBit(State::S0)) return false;
return true;
}
bool is_const_one(const SigSpec &s) {
SigSpec ss = sigmap(s);
if (!ss.is_fully_const()) return false;
return ss.as_const().as_int() == 1;
}
// Recover the index bus `key` from a one-hot set-mask (1 << key), spelled
// as $shl(1, key) or $shift(1, -key).
SigSpec decode_onehot_key(const SigSpec &mask) {
Cell *d = sole_driver(mask);
if (!d) return SigSpec();
if ((d->type == ID($shl) || d->type == ID($sshl)) &&
is_const_one(d->getPort(ID::A)))
return sigmap(d->getPort(ID::B));
if (d->type == ID($shift) && is_const_one(d->getPort(ID::A))) {
Cell *neg = sole_driver(d->getPort(ID::B));
if (neg && neg->type == ID($neg))
return sigmap(neg->getPort(ID::A));
}
return SigSpec();
}
// A set-arm is `taken_prev` with one bit (1 << key) OR'ed in. After opt it
// appears either as the raw one-hot (prev was 0) or as an $or whose two
// operands are the one-hot mask and the (masked) previous state. Return the
// key bus of the one-hot mask.
SigSpec extract_key_from_setarm(const SigSpec &arm) {
SigSpec k = decode_onehot_key(arm);
if (GetSize(k)) return k;
Cell *d = sole_driver(arm);
if (d && d->type == ID($or)) {
k = decode_onehot_key(d->getPort(ID::A));
if (GetSize(k)) return k;
k = decode_onehot_key(d->getPort(ID::B));
if (GetSize(k)) return k;
}
return SigSpec();
}
// One guarded "set key" applied to the accumulator (guard may be const-1
// for an unconditional set).
struct SetStep {
SigBit guard;
SigSpec key;
};
// Cache of trace results: chained reads share accumulator prefixes (read j
// indexes the state produced by sets 0..j-1), so without memoization the
// same chain is re-walked once per read -> O(P^2 * S). The cache makes the
// total walk O(P * S).
dict<SigSpec, std::pair<bool, vector<SetStep>>> acc_memo;
// Walk an accumulator value back to constant zero, collecting the guarded
// key-sets that produced it. Returns false (leaving `steps` unchanged) if it
// is not a pure set-only accumulator (mux/or of prev with a one-hot key)
// rooted at 0.
bool trace_acc(SigSpec acc, vector<SetStep> &steps, int depth) {
acc = sigmap(acc);
auto mit = acc_memo.find(acc);
if (mit != acc_memo.end()) {
if (mit->second.first)
steps.insert(steps.end(), mit->second.second.begin(),
mit->second.second.end());
return mit->second.first;
}
int start = GetSize(steps);
bool ok = trace_acc_uncached(acc, steps, depth);
if (ok) {
acc_memo[acc] = {true, vector<SetStep>(steps.begin() + start,
steps.end())};
} else {
steps.resize(start); // discard any partial trace
acc_memo[acc] = {false, {}};
}
return ok;
}
bool trace_acc_uncached(SigSpec acc, vector<SetStep> &steps, int depth) {
if (is_all_zero(acc))
return true;
if (depth > max_chain)
return false;
Cell *d = sole_driver(acc);
if (!d)
return false;
if (d->type == ID($mux)) {
SigSpec s = sigmap(d->getPort(ID::S));
if (GetSize(s) != 1)
return false;
if (!trace_acc(d->getPort(ID::A), steps, depth + 1))
return false;
SigSpec key = extract_key_from_setarm(d->getPort(ID::B));
if (GetSize(key) == 0)
return false;
steps.push_back(SetStep{s[0], key});
return true;
}
if (d->type == ID($or)) {
SigSpec a = d->getPort(ID::A), b = d->getPort(ID::B);
SigSpec ka = decode_onehot_key(a), kb = decode_onehot_key(b);
if (GetSize(ka) && trace_acc(b, steps, depth + 1)) {
steps.push_back(SetStep{SigBit(State::S1), ka});
return true;
}
if (GetSize(kb) && trace_acc(a, steps, depth + 1)) {
steps.push_back(SetStep{SigBit(State::S1), kb});
return true;
}
}
return false;
}
// A dynamic read of the accumulator: the 1-bit read cell, the accumulator
// value it indexes (with any out-of-range x-padding stripped) and the index.
struct Read {
Cell *cell;
SigSpec acc;
SigSpec key;
};
// Recognize a 1-bit dynamic read of a vector: either $shiftx(A=acc, B=key)
// or $bmux(A={x.., acc}, S=key). Returns false otherwise.
bool match_read(Cell *c, Read &r) {
if (c->type == ID($shiftx)) {
if (GetSize(c->getPort(ID::Y)) != 1)
return false;
r.cell = c;
r.acc = sigmap(c->getPort(ID::A));
r.key = sigmap(c->getPort(ID::B));
return GetSize(r.acc) >= 2;
}
if (c->type == ID($bmux)) {
if (c->getParam(ID::WIDTH).as_int() != 1)
return false;
SigSpec a = sigmap(c->getPort(ID::A));
// Strip the high x-padding to recover the real accumulator bits.
int w = 0;
while (w < GetSize(a) && a[w] != SigBit(State::Sx))
w++;
if (w < 2)
return false;
r.cell = c;
r.acc = a.extract(0, w);
r.key = sigmap(c->getPort(ID::S));
return true;
}
return false;
}
// Prove read == OR over steps of ( guard & key == read_key ) by ConstEval
// fingerprinting over the reachable key range [0,S). Guards and key buses
// (which are disjoint sel slices) are driven as free inputs.
bool validate_read(const Read &rd, const vector<SetStep> &steps, int S) {
Cell *read = rd.cell;
SigSpec read_key = rd.key;
// In strict mode sweep the full key range so the rewrite is proven for
// every value the index bus can take (out-of-range reads included);
// otherwise sweep only the reachable slots [0,S).
int kw = GetSize(read_key);
uint64_t range = (uint64_t)S;
if (strict) {
int cap = kw < 30 ? kw : 30;
range = 1ULL << cap;
}
ConstEval ce(module);
uint64_t lfsr = 0x9e3779b97f4a7c15ULL ^ (uintptr_t)read;
auto rnd = [&]() {
lfsr ^= lfsr << 13; lfsr ^= lfsr >> 7; lfsr ^= lfsr << 17;
return lfsr;
};
for (int t = 0; t < fp_trials; t++) {
ce.push();
int rk = (int)(rnd() % range);
ce.set(read_key, Const(rk, GetSize(read_key)));
vector<int> kv(GetSize(steps));
vector<int> gv(GetSize(steps));
for (int i = 0; i < GetSize(steps); i++) {
kv[i] = (int)(rnd() % range);
ce.set(steps[i].key, Const(kv[i], GetSize(steps[i].key)));
if (steps[i].guard == State::S1) {
gv[i] = 1;
} else {
gv[i] = (int)(rnd() & 1);
ce.set(SigSpec(steps[i].guard), Const(gv[i], 1));
}
}
SigSpec out(read->getPort(ID::Y));
SigSpec undef;
bool ok = ce.eval(out, undef) && out.is_fully_const();
int actual = ok ? (out.as_const().as_int() & 1) : -1;
int expect = 0;
for (int i = 0; i < GetSize(steps); i++)
if (gv[i] && kv[i] == rk) { expect = 1; break; }
ce.pop();
if (!ok || actual != expect)
return false;
}
return true;
}
void rewrite_read(const Read &rd, const vector<SetStep> &steps) {
Cell *read = rd.cell;
cell = read;
SigSpec read_key = rd.key;
SigSpec new_r;
if (steps.empty()) {
new_r = SigSpec(State::S0);
} else {
SigSpec terms;
for (auto &st : steps) {
SigSpec eq = module->Eq(NEW_ID2_SUFFIX("priokey_eq"),
st.key, read_key);
cells_added++;
SigSpec g = module->And(NEW_ID2_SUFFIX("priokey_and"),
SigSpec(st.guard), eq);
cells_added++;
terms.append(g);
}
new_r = module->ReduceOr(NEW_ID2_SUFFIX("priokey_or"), terms);
cells_added++;
}
// Tag wire so the rewrite is externally observable, then detach the old
// dynamic read and drive its consumers from the reduction.
Wire *tag = module->addWire(NEW_ID2_SUFFIX("priokey_read"), 1);
module->connect(SigSpec(tag), new_r);
SigSpec old_y = sigmap(read->getPort(ID::Y));
Wire *dangling = module->addWire(NEW_ID2_SUFFIX("priokey_dangling"),
GetSize(read->getPort(ID::Y)));
read->setPort(ID::Y, dangling);
module->connect(old_y, SigSpec(tag));
regions_rewritten++;
}
void run() {
vector<Read> reads;
for (auto c : module->cells()) {
Read r;
if (!match_read(c, r))
continue;
if (GetSize(r.acc) > max_slots)
continue;
reads.push_back(r);
}
int max_sources = 0;
int accum_width = 0;
vector<Read> zero_reads; // read of the all-zero head (== 0)
for (auto &rd : reads) {
int S = GetSize(rd.acc);
vector<SetStep> steps;
if (!trace_acc(rd.acc, steps, 0))
continue;
// The all-zero head read is only rewritten (to 0) once we know the
// pattern is really present in this module.
if (steps.empty()) {
zero_reads.push_back(rd);
continue;
}
if (!validate_read(rd, steps, S))
continue;
rewrite_read(rd, steps);
max_sources = std::max(max_sources, GetSize(steps) + 1);
accum_width = S;
}
if (regions_rewritten)
for (auto &rd : zero_reads)
rewrite_read(rd, {});
if (regions_rewritten)
log(" %s: priority-by-key dedup, up to %d source(s), "
"%d-slot accumulator\n",
log_id(module), max_sources, accum_width);
}
};
struct OptPrioKeyPass : public Pass {
OptPrioKeyPass() : Pass("opt_priokey",
"detect and rewrite priority-by-key deduplication accumulators") {}
void help() override {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" opt_priokey [options] [selection]\n");
log("\n");
log("This pass detects a serial 'set accumulator' that resolves conflicts\n");
log("between several sources that each carry a small key:\n");
log("\n");
log(" taken = '0;\n");
log(" for (i = 0; i < P; i++)\n");
log(" if (act[i] && !taken[key[i]]) begin taken[key[i]] = 1; ... end\n");
log("\n");
log("Such RTL elaborates into a chain of dynamic-index reads/writes into a\n");
log("wide one-hot vector ($shiftx / $shift), whose depth grows with both the\n");
log("number of sources and the accumulator width. Each dynamic read\n");
log("taken[key[j]] is provably equal to\n");
log("\n");
log(" OR over i<j of ( set_guard[i] & key[i] == key[j] )\n");
log("\n");
log("so the pass replaces every read with that pairwise-key-compare\n");
log("reduction, removing the wide dynamic indexing. Each rewrite is\n");
log("validated by a ConstEval fingerprint before being applied; for\n");
log("non-power-of-two accumulator widths the rewrite holds over the\n");
log("reachable key range [0,S).\n");
log("\n");
log(" -max-slots N\n");
log(" maximum accumulator width to consider (default 16384).\n");
log("\n");
log(" -max-sources N\n");
log(" maximum number of chained sources to consider (default 256).\n");
log("\n");
log(" -strict\n");
log(" validate every rewrite over the full index range instead of\n");
log(" only the reachable slots [0,S). Rewrites that hold merely by\n");
log(" out-of-range don't-care freedom are then rejected (use this\n");
log(" under equiv_opt -assert / formal flows).\n");
log("\n");
log("This pass is not invoked by the default 'opt' script; users opt in.\n");
log("After rewriting, the dead accumulator chain is removed by the trailing\n");
log("'clean -purge'.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override {
log_header(design, "Executing OPT_PRIOKEY pass (priority-by-key dedup).\n");
int max_slots = 1 << 14;
int max_sources = 256;
bool strict = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-max-slots" && argidx + 1 < args.size()) {
max_slots = std::stoi(args[++argidx]); continue;
}
if (args[argidx] == "-max-sources" && argidx + 1 < args.size()) {
max_sources = std::stoi(args[++argidx]); continue;
}
if (args[argidx] == "-strict") {
strict = true; continue;
}
break;
}
extra_args(args, argidx, design);
int total_regions = 0, total_cells = 0;
for (auto module : design->selected_modules()) {
OptPrioKeyWorker worker(module);
worker.max_slots = max_slots;
worker.max_chain = max_sources;
worker.strict = strict;
worker.run();
total_regions += worker.regions_rewritten;
total_cells += worker.cells_added;
}
log("Rewrote %d dynamic key-read(s); emitted %d new cell(s).\n",
total_regions, total_cells);
if (total_regions)
Yosys::run_pass("clean -purge");
}
} OptPrioKeyPass;
PRIVATE_NAMESPACE_END

2
passes/opt/opt_priority_onehot.cc
View file

@ -256,7 +256,7 @@ struct OptPriorityOnehotWorker : CutRegionWorker {
bool fingerprint(const Candidate &cand, bool msb_first)
{
ConstEval ce(module);
ConstEval &ce = shared_ce();
SigSpec out_sig = sigmap(cand.out_sig);
SigSpec valid_sig = sigmap(cand.valid_sig);
SigSpec field_sig = sigmap(cand.field_sig);

126
passes/sat/async2sync.cc
View file

@ -95,27 +95,27 @@ struct Async2syncPass : public Pass {
if (trg_width == 0) {
if (initstate == State::S0)
initstate = module->Initstate(NEW_ID);
initstate = module->Initstate(NEW_ID2_SUFFIX("initstate")); // SILIMATE: Improve the naming
SigBit sig_en = cell->getPort(ID::EN);
cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate));
cell->setPort(ID::EN, module->And(NEW_ID2_SUFFIX("en_init"), sig_en, initstate)); // SILIMATE: Improve the naming
} else {
SigBit sig_en = cell->getPort(ID::EN);
SigSpec sig_args = cell->getPort(ID::ARGS);
bool trg_polarity = cell->getParam(ID(TRG_POLARITY)).as_bool();
SigBit sig_trg = cell->getPort(ID::TRG);
Wire *sig_en_q = module->addWire(NEW_ID);
Wire *sig_args_q = module->addWire(NEW_ID, GetSize(sig_args));
Wire *sig_en_q = module->addWire(NEW_ID2_SUFFIX("en_q")); // SILIMATE: Improve the naming
Wire *sig_args_q = module->addWire(NEW_ID2_SUFFIX("args_q"), GetSize(sig_args)); // SILIMATE: Improve the naming
sig_en_q->attributes.emplace(ID::init, State::S0);
module->addDff(NEW_ID, sig_trg, sig_en, sig_en_q, trg_polarity, cell->get_src_attribute());
module->addDff(NEW_ID, sig_trg, sig_args, sig_args_q, trg_polarity, cell->get_src_attribute());
module->addDff(NEW_ID2_SUFFIX("en_dff"), sig_trg, sig_en, sig_en_q, trg_polarity, cell->get_src_attribute()); // SILIMATE: Improve the naming
module->addDff(NEW_ID2_SUFFIX("args_dff"), sig_trg, sig_args, sig_args_q, trg_polarity, cell->get_src_attribute()); // SILIMATE: Improve the naming
cell->setPort(ID::EN, sig_en_q);
cell->setPort(ID::ARGS, sig_args_q);
if (cell->type == ID($check)) {
SigBit sig_a = cell->getPort(ID::A);
Wire *sig_a_q = module->addWire(NEW_ID);
Wire *sig_a_q = module->addWire(NEW_ID2_SUFFIX("a_q")); // SILIMATE: Improve the naming
sig_a_q->attributes.emplace(ID::init, State::S1);
module->addDff(NEW_ID, sig_trg, sig_a, sig_a_q, trg_polarity, cell->get_src_attribute());
module->addDff(NEW_ID2_SUFFIX("a_dff"), sig_trg, sig_a, sig_a_q, trg_polarity, cell->get_src_attribute()); // SILIMATE: Improve the naming
cell->setPort(ID::A, sig_a_q);
}
}
@ -152,8 +152,8 @@ struct Async2syncPass : public Pass {
initvals.remove_init(ff.sig_q);
Wire *new_d = module->addWire(NEW_ID, ff.width);
Wire *new_q = module->addWire(NEW_ID, ff.width);
Wire *new_d = module->addWire(NEW_ID2_SUFFIX("new_d"), ff.width); // SILIMATE: Improve the naming
Wire *new_q = module->addWire(NEW_ID2_SUFFIX("new_q"), ff.width); // SILIMATE: Improve the naming
SigSpec sig_set = ff.sig_set;
SigSpec sig_clr = ff.sig_clr;
@ -161,21 +161,21 @@ struct Async2syncPass : public Pass {
if (!ff.pol_set) {
if (!ff.is_fine)
sig_set = module->Not(NEW_ID, sig_set);
sig_set = module->Not(NEW_ID2_SUFFIX("set_hi"), sig_set); // SILIMATE: Improve the naming
else
sig_set = module->NotGate(NEW_ID, sig_set);
sig_set = module->NotGate(NEW_ID2_SUFFIX("set_hi"), sig_set); // SILIMATE: Improve the naming
}
if (ff.pol_clr) {
if (!ff.is_fine)
sig_clr_inv = module->Not(NEW_ID, sig_clr);
sig_clr_inv = module->Not(NEW_ID2_SUFFIX("clr_inv"), sig_clr); // SILIMATE: Improve the naming
else
sig_clr_inv = module->NotGate(NEW_ID, sig_clr);
sig_clr_inv = module->NotGate(NEW_ID2_SUFFIX("clr_inv"), sig_clr); // SILIMATE: Improve the naming
} else {
if (!ff.is_fine)
sig_clr = module->Not(NEW_ID, sig_clr);
sig_clr = module->Not(NEW_ID2_SUFFIX("clr_hi"), sig_clr); // SILIMATE: Improve the naming
else
sig_clr = module->NotGate(NEW_ID, sig_clr);
sig_clr = module->NotGate(NEW_ID2_SUFFIX("clr_hi"), sig_clr); // SILIMATE: Improve the naming
}
// At this point, sig_set and sig_clr are now unconditionally
@ -183,26 +183,26 @@ struct Async2syncPass : public Pass {
SigSpec set_and_clr;
if (!ff.is_fine)
set_and_clr = module->And(NEW_ID, sig_set, sig_clr);
set_and_clr = module->And(NEW_ID2_SUFFIX("set_and_clr"), sig_set, sig_clr); // SILIMATE: Improve the naming
else
set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr);
set_and_clr = module->AndGate(NEW_ID2_SUFFIX("set_and_clr"), sig_set, sig_clr); // SILIMATE: Improve the naming
if (!ff.is_fine) {
SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set);
tmp = module->And(NEW_ID, tmp, sig_clr_inv);
module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d);
SigSpec tmp = module->Or(NEW_ID2_SUFFIX("d_or_set"), ff.sig_d, sig_set); // SILIMATE: Improve the naming
tmp = module->And(NEW_ID2_SUFFIX("d_masked"), tmp, sig_clr_inv); // SILIMATE: Improve the naming
module->addBwmux(NEW_ID2_SUFFIX("d_bwmux"), tmp, Const(State::Sx, ff.width), set_and_clr, new_d); // SILIMATE: Improve the naming
tmp = module->Or(NEW_ID, new_q, sig_set);
tmp = module->And(NEW_ID, tmp, sig_clr_inv);
module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q);
tmp = module->Or(NEW_ID2_SUFFIX("q_or_set"), new_q, sig_set); // SILIMATE: Improve the naming
tmp = module->And(NEW_ID2_SUFFIX("q_masked"), tmp, sig_clr_inv); // SILIMATE: Improve the naming
module->addBwmux(NEW_ID2_SUFFIX("q_bwmux"), tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q); // SILIMATE: Improve the naming
} else {
SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set);
tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv);
module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, new_d);
SigSpec tmp = module->OrGate(NEW_ID2_SUFFIX("d_or_set"), ff.sig_d, sig_set); // SILIMATE: Improve the naming
tmp = module->AndGate(NEW_ID2_SUFFIX("d_masked"), tmp, sig_clr_inv); // SILIMATE: Improve the naming
module->addMuxGate(NEW_ID2_SUFFIX("d_mux"), tmp, State::Sx, set_and_clr, new_d); // SILIMATE: Improve the naming
tmp = module->OrGate(NEW_ID, new_q, sig_set);
tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv);
module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q);
tmp = module->OrGate(NEW_ID2_SUFFIX("q_or_set"), new_q, sig_set); // SILIMATE: Improve the naming
tmp = module->AndGate(NEW_ID2_SUFFIX("q_masked"), tmp, sig_clr_inv); // SILIMATE: Improve the naming
module->addMuxGate(NEW_ID2_SUFFIX("q_mux"), tmp, State::Sx, set_and_clr, ff.sig_q); // SILIMATE: Improve the naming
}
ff.sig_d = new_d;
@ -217,24 +217,24 @@ struct Async2syncPass : public Pass {
initvals.remove_init(ff.sig_q);
Wire *new_d = module->addWire(NEW_ID, ff.width);
Wire *new_q = module->addWire(NEW_ID, ff.width);
Wire *new_d = module->addWire(NEW_ID2_SUFFIX("new_d"), ff.width); // SILIMATE: Improve the naming
Wire *new_q = module->addWire(NEW_ID2_SUFFIX("new_q"), ff.width); // SILIMATE: Improve the naming
if (ff.pol_aload) {
if (!ff.is_fine) {
module->addMux(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, ff.sig_q);
module->addMux(NEW_ID, ff.sig_d, ff.sig_ad, ff.sig_aload, new_d);
module->addMux(NEW_ID2_SUFFIX("q_aload_mux"), new_q, ff.sig_ad, ff.sig_aload, ff.sig_q); // SILIMATE: Improve the naming
module->addMux(NEW_ID2_SUFFIX("d_aload_mux"), ff.sig_d, ff.sig_ad, ff.sig_aload, new_d); // SILIMATE: Improve the naming
} else {
module->addMuxGate(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, ff.sig_q);
module->addMuxGate(NEW_ID, ff.sig_d, ff.sig_ad, ff.sig_aload, new_d);
module->addMuxGate(NEW_ID2_SUFFIX("q_aload_mux"), new_q, ff.sig_ad, ff.sig_aload, ff.sig_q); // SILIMATE: Improve the naming
module->addMuxGate(NEW_ID2_SUFFIX("d_aload_mux"), ff.sig_d, ff.sig_ad, ff.sig_aload, new_d); // SILIMATE: Improve the naming
}
} else {
if (!ff.is_fine) {
module->addMux(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, ff.sig_q);
module->addMux(NEW_ID, ff.sig_ad, ff.sig_d, ff.sig_aload, new_d);
module->addMux(NEW_ID2_SUFFIX("q_aload_mux"), ff.sig_ad, new_q, ff.sig_aload, ff.sig_q); // SILIMATE: Improve the naming
module->addMux(NEW_ID2_SUFFIX("d_aload_mux"), ff.sig_ad, ff.sig_d, ff.sig_aload, new_d); // SILIMATE: Improve the naming
} else {
module->addMuxGate(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, ff.sig_q);
module->addMuxGate(NEW_ID, ff.sig_ad, ff.sig_d, ff.sig_aload, new_d);
module->addMuxGate(NEW_ID2_SUFFIX("q_aload_mux"), ff.sig_ad, new_q, ff.sig_aload, ff.sig_q); // SILIMATE: Improve the naming
module->addMuxGate(NEW_ID2_SUFFIX("d_aload_mux"), ff.sig_ad, ff.sig_d, ff.sig_aload, new_d); // SILIMATE: Improve the naming
}
}
@ -250,18 +250,18 @@ struct Async2syncPass : public Pass {
initvals.remove_init(ff.sig_q);
Wire *new_q = module->addWire(NEW_ID, ff.width);
Wire *new_q = module->addWire(NEW_ID2_SUFFIX("new_q"), ff.width); // SILIMATE: Improve the naming
if (ff.pol_arst) {
if (!ff.is_fine)
module->addMux(NEW_ID, new_q, ff.val_arst, ff.sig_arst, ff.sig_q);
module->addMux(NEW_ID2_SUFFIX("arst_mux"), new_q, ff.val_arst, ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
else
module->addMuxGate(NEW_ID, new_q, ff.val_arst[0], ff.sig_arst, ff.sig_q);
module->addMuxGate(NEW_ID2_SUFFIX("arst_mux"), new_q, ff.val_arst[0], ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
} else {
if (!ff.is_fine)
module->addMux(NEW_ID, ff.val_arst, new_q, ff.sig_arst, ff.sig_q);
module->addMux(NEW_ID2_SUFFIX("arst_mux"), ff.val_arst, new_q, ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
else
module->addMuxGate(NEW_ID, ff.val_arst[0], new_q, ff.sig_arst, ff.sig_q);
module->addMuxGate(NEW_ID2_SUFFIX("arst_mux"), ff.val_arst[0], new_q, ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
}
ff.sig_q = new_q;
@ -284,21 +284,21 @@ struct Async2syncPass : public Pass {
initvals.remove_init(ff.sig_q);
Wire *new_q = module->addWire(NEW_ID, ff.width);
Wire *new_q = module->addWire(NEW_ID2_SUFFIX("new_q"), ff.width); // SILIMATE: Improve the naming
Wire *new_d;
if (ff.has_aload) {
new_d = module->addWire(NEW_ID, ff.width);
new_d = module->addWire(NEW_ID2_SUFFIX("new_d"), ff.width); // SILIMATE: Improve the naming
if (ff.pol_aload) {
if (!ff.is_fine)
module->addMux(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, new_d);
module->addMux(NEW_ID2_SUFFIX("d_aload_mux"), new_q, ff.sig_ad, ff.sig_aload, new_d); // SILIMATE: Improve the naming
else
module->addMuxGate(NEW_ID, new_q, ff.sig_ad, ff.sig_aload, new_d);
module->addMuxGate(NEW_ID2_SUFFIX("d_aload_mux"), new_q, ff.sig_ad, ff.sig_aload, new_d); // SILIMATE: Improve the naming
} else {
if (!ff.is_fine)
module->addMux(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, new_d);
module->addMux(NEW_ID2_SUFFIX("d_aload_mux"), ff.sig_ad, new_q, ff.sig_aload, new_d); // SILIMATE: Improve the naming
else
module->addMuxGate(NEW_ID, ff.sig_ad, new_q, ff.sig_aload, new_d);
module->addMuxGate(NEW_ID2_SUFFIX("d_aload_mux"), ff.sig_ad, new_q, ff.sig_aload, new_d); // SILIMATE: Improve the naming
}
} else {
new_d = new_q;
@ -310,36 +310,36 @@ struct Async2syncPass : public Pass {
if (!ff.pol_set) {
if (!ff.is_fine)
sig_set = module->Not(NEW_ID, sig_set);
sig_set = module->Not(NEW_ID2_SUFFIX("set_hi"), sig_set); // SILIMATE: Improve the naming
else
sig_set = module->NotGate(NEW_ID, sig_set);
sig_set = module->NotGate(NEW_ID2_SUFFIX("set_hi"), sig_set); // SILIMATE: Improve the naming
}
if (ff.pol_clr) {
if (!ff.is_fine)
sig_clr = module->Not(NEW_ID, sig_clr);
sig_clr = module->Not(NEW_ID2_SUFFIX("clr_lo"), sig_clr); // SILIMATE: Improve the naming
else
sig_clr = module->NotGate(NEW_ID, sig_clr);
sig_clr = module->NotGate(NEW_ID2_SUFFIX("clr_lo"), sig_clr); // SILIMATE: Improve the naming
}
if (!ff.is_fine) {
SigSpec tmp = module->Or(NEW_ID, new_d, sig_set);
module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q);
SigSpec tmp = module->Or(NEW_ID2_SUFFIX("d_or_set"), new_d, sig_set); // SILIMATE: Improve the naming
module->addAnd(NEW_ID2_SUFFIX("q_sr"), tmp, sig_clr, ff.sig_q); // SILIMATE: Improve the naming
} else {
SigSpec tmp = module->OrGate(NEW_ID, new_d, sig_set);
module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q);
SigSpec tmp = module->OrGate(NEW_ID2_SUFFIX("d_or_set"), new_d, sig_set); // SILIMATE: Improve the naming
module->addAndGate(NEW_ID2_SUFFIX("q_sr"), tmp, sig_clr, ff.sig_q); // SILIMATE: Improve the naming
}
} else if (ff.has_arst) {
if (ff.pol_arst) {
if (!ff.is_fine)
module->addMux(NEW_ID, new_d, ff.val_arst, ff.sig_arst, ff.sig_q);
module->addMux(NEW_ID2_SUFFIX("arst_mux"), new_d, ff.val_arst, ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
else
module->addMuxGate(NEW_ID, new_d, ff.val_arst[0], ff.sig_arst, ff.sig_q);
module->addMuxGate(NEW_ID2_SUFFIX("arst_mux"), new_d, ff.val_arst[0], ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
} else {
if (!ff.is_fine)
module->addMux(NEW_ID, ff.val_arst, new_d, ff.sig_arst, ff.sig_q);
module->addMux(NEW_ID2_SUFFIX("arst_mux"), ff.val_arst, new_d, ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
else
module->addMuxGate(NEW_ID, ff.val_arst[0], new_d, ff.sig_arst, ff.sig_q);
module->addMuxGate(NEW_ID2_SUFFIX("arst_mux"), ff.val_arst[0], new_d, ff.sig_arst, ff.sig_q); // SILIMATE: Improve the naming
}
} else {
module->connect(ff.sig_q, new_d);

7
passes/sat/sim.cc
View file

@ -658,6 +658,13 @@ struct SimInstance
else if (has_a && has_b && !has_c && !has_d && has_s && has_y)
// (A,B,S -> Y) cells
eval_state = CellTypes::eval(cell, get_state(sig_a), get_state(sig_b), get_state(sig_s), &err);
else if (has_a && has_b && has_c && has_d && !has_s && has_y)
// (A,B,C,D -> Y) cells, e.g. $_AOI4_/$_OAI4_ (CellTypes::eval implements these);
// without this case every 4-input gate fell through to the "unsupported" warning
// below, flooding the log (millions of lines on AOI/OAI-dense designs like AES)
// and leaving the output stuck at X.
eval_state = CellTypes::eval(cell, get_state(sig_a), get_state(sig_b),
get_state(sig_c), get_state(sig_d), &err);
else
err = true;

3
passes/silimate/CMakeLists.txt
View file

@ -50,6 +50,9 @@ yosys_pass(splitlarge
yosys_pass(splitnetlist
splitnetlist.cc
)
yosys_pass(carvenetlist
carvenetlist.cc
)
yosys_pass(opt_timing_balance
opt_timing_balance.cc
)

1045
passes/silimate/carvenetlist.cc Normal file
View file

File diff suppressed because it is too large Load diff

61
passes/silimate/opt_compact_prefix.cc
View file

@ -236,7 +236,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
for (auto bit : en_cands)
cand_bits.push_back(bit);
ConstEval ce(module);
ConstEval &ce = shared_ce();
SigSpec out_s = sigmap(root_sig);
SigSpec data_s = sigmap(data_sig);
SigSpec cand_s;
@ -415,7 +415,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
{
if (width < 4)
return false;
ConstEval ce(module);
ConstEval &ce = shared_ce();
SigSpec in_s = sigmap(in_sig);
SigSpec out_s = sigmap(out_sig);
@ -511,7 +511,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
int wd = GetSize(dis_s);
int wt = GetSize(data_s);
bool self = sigmap(dis_s) == sigmap(data_s);
ConstEval ce(module);
ConstEval &ce = shared_ce();
for (int pol = 0; pol < 2; pol++) {
// A self-pair (data == disable bus) can only be probed with all
// lanes enabled AND data all-ones, i.e. enable-high polarity.
@ -546,7 +546,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
return false;
if (lw > wd || lw > wt || wd > 62 || wt > 62)
return false;
ConstEval ce(module);
ConstEval &ce = shared_ce();
SigSpec dis_s = sigmap(dis_sig);
SigSpec data_s = sigmap(data_sig);
SigSpec out_s = sigmap(out_sig);
@ -615,8 +615,14 @@ struct OptCompactPrefixWorker : CutRegionWorker
return mask;
}
// Evaluate the modulo vector set once and test all four
// (msb_first, offset) variants against the recorded outputs, in the
// original priority order with first-match tie-break. This replaces up
// to four full ConstEval sweeps (one per variant) with a single sweep;
// sets out_msb_first/out_offset on the first surviving variant.
bool fingerprint_modulo(const SigSpec &en_sig, const SigSpec &n_sig,
const SigSpec &mask_sig, int width, bool msb_first, int offset)
const SigSpec &mask_sig, int width,
bool &out_msb_first, int &out_offset)
{
if (width <= 0 || width > 62)
return false;
@ -624,7 +630,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
// also matches plain gating muxes; require a real counter range.
if (GetSize(n_sig) < 2)
return false;
ConstEval ce(module);
ConstEval &ce = shared_ce();
SigSpec en_s = sigmap(en_sig);
SigSpec n_s = sigmap(n_sig);
SigSpec mask_s = sigmap(mask_sig);
@ -653,6 +659,12 @@ struct OptCompactPrefixWorker : CutRegionWorker
envals.push_back(lfsr & full);
}
// Variants in the original check order (msb/lsb x offset 0/1).
static const struct { bool msb; int off; } variants[] = {
{true, 0}, {false, 0}, {false, 1}, {true, 1}
};
bool alive[4] = {true, true, true, true};
for (uint64_t nv : nvals)
for (uint64_t ev : envals) {
uint64_t actual;
@ -660,10 +672,27 @@ struct OptCompactPrefixWorker : CutRegionWorker
{n_s, const_u64(nv, nw)}},
mask_s, actual))
return false;
if (actual != expected_modulo_mask(ev, nv, width, msb_first, offset))
bool any = false;
for (int v = 0; v < 4; v++) {
if (!alive[v])
continue;
if (actual != expected_modulo_mask(ev, nv, width,
variants[v].msb, variants[v].off))
alive[v] = false;
else
any = true;
}
if (!any)
return false;
}
return true;
for (int v = 0; v < 4; v++)
if (alive[v]) {
out_msb_first = variants[v].msb;
out_offset = variants[v].off;
return true;
}
return false;
}
// --- Forward gather/compress: out[k] = data[i_k] where i_k is the
@ -693,7 +722,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
{
if (width < 4 || width > 62)
return false;
ConstEval ce(module);
ConstEval &ce = shared_ce();
SigSpec en_s = sigmap(en_sig);
SigSpec data_s = sigmap(data_sig);
SigSpec out_s = sigmap(out_sig);
@ -1397,19 +1426,7 @@ struct OptCompactPrefixWorker : CutRegionWorker
fp_attempts++;
bool msb_first = false;
int offset = -1;
if (fingerprint_modulo(en.sig, n.sig, root.sig, width, true, 0)) {
msb_first = true;
offset = 0;
} else if (fingerprint_modulo(en.sig, n.sig, root.sig, width, false, 0)) {
msb_first = false;
offset = 0;
} else if (fingerprint_modulo(en.sig, n.sig, root.sig, width, false, 1)) {
msb_first = false;
offset = 1;
} else if (fingerprint_modulo(en.sig, n.sig, root.sig, width, true, 1)) {
msb_first = true;
offset = 1;
} else {
if (!fingerprint_modulo(en.sig, n.sig, root.sig, width, msb_first, offset)) {
log_debug(" mod %s/%s: fingerprint mismatch\n", en.name.c_str(), n.name.c_str());
continue;
}

8
passes/techmap/bwmuxmap.cc
View file

@ -57,10 +57,10 @@ struct BwmuxmapPass : public Pass {
auto &sig_b = cell->getPort(ID::B);
auto &sig_s = cell->getPort(ID::S);
auto not_s = module->Not(NEW_ID, sig_s);
auto masked_b = module->And(NEW_ID, sig_s, sig_b);
auto masked_a = module->And(NEW_ID, not_s, sig_a);
module->addOr(NEW_ID, masked_a, masked_b, sig_y);
auto not_s = module->Not(NEW_ID2_SUFFIX("not_s"), sig_s); // SILIMATE: Improve the naming
auto masked_b = module->And(NEW_ID2_SUFFIX("masked_b"), sig_s, sig_b); // SILIMATE: Improve the naming
auto masked_a = module->And(NEW_ID2_SUFFIX("masked_a"), not_s, sig_a); // SILIMATE: Improve the naming
module->addOr(NEW_ID2_SUFFIX("y"), masked_a, masked_b, sig_y); // SILIMATE: Improve the naming
module->remove(cell);
}

1
silimate-shell.nix
View file

@ -29,7 +29,6 @@ pkgs.mkShell {
iverilog # tests
gtkwave # vcd2fst
(python3.withPackages(ps: with ps; [pip wheel pybind11 cxxheaderparser]))
gnu-ar
gtest
] ++ lib.optionals stdenv.isLinux [
elfutils # provides libdw.so (not to be confused with libdwarf.so)

89
tests/opt/opt_dff_eqbits.ys Normal file
View file

@ -0,0 +1,89 @@
# small test case
design -reset
read_verilog -sv opt_dff_eqbits_small.sv
hierarchy -top test_case
techmap
opt_dff -sat
synth
opt_dff -sat
opt_clean -purge
select -assert-count 2 t:$_SDFF_PN0_
# equivalence
design -reset
read_verilog -sv opt_dff_eqbits_small.sv
hierarchy -top test_case
prep
design -save gold
opt_dff -sat
design -save gate
design -copy-from gold -as gold test_case
design -copy-from gate -as gate test_case
equiv_make gold gate equiv
equiv_induct equiv
equiv_status -assert
# large test case
design -reset
read_verilog -sv opt_dff_eqbits_large.sv
hierarchy -top test_case
techmap
opt_dff -sat
synth
opt_dff -sat
opt_clean -purge
select -assert-count 6 t:$_SDFFE_PN0P_
# equivalence
design -reset
read_verilog -sv opt_dff_eqbits_large.sv
hierarchy -top test_case
prep
design -save gold
opt_dff -sat
design -save gate
design -copy-from gold -as gold test_case
design -copy-from gate -as gate test_case
equiv_make gold gate equiv
equiv_induct equiv
equiv_status -assert
# verify keepdc exclusivity
design -reset
read_verilog -sv <<EOT
module test_case(input clk, input d, output reg a, output reg b);
initial a = 1'b0;
initial b = 1'b0;
always @(posedge clk) a <= d;
always @(posedge clk) b <= d | 1'bx;
endmodule
EOT
hierarchy -top test_case
proc
techmap
opt_dff -sat
opt_clean -purge
select -assert-count 1 t:$_DFF_P_
design -reset
read_verilog -sv <<EOT
module test_case(input clk, input d, output reg a, output reg b);
initial a = 1'b0;
initial b = 1'b0;
always @(posedge clk) a <= d;
always @(posedge clk) b <= d | 1'bx;
endmodule
EOT
hierarchy -top test_case
proc
techmap
logger -expect error "The -sat and -keepdc options are mutually exclusive." 1
opt_dff -sat -keepdc

231
tests/opt/opt_dff_eqbits_large.sv Normal file
View file

@ -0,0 +1,231 @@
module test_case (
input wire clk,
input wire rst_n,
input wire [3:0] chan_0_data,
input wire chan_0_vld,
input wire chan_1_rdy,
output wire chan_0_rdy,
output wire [207:0] chan_1_data,
output wire chan_1_vld,
output wire idle
);
wire [12:0] state_init[0:15];
assign state_init[0] = 13'h0000;
assign state_init[1] = 13'h0000;
assign state_init[2] = 13'h0000;
assign state_init[3] = 13'h0000;
assign state_init[4] = 13'h0000;
assign state_init[5] = 13'h0000;
assign state_init[6] = 13'h0000;
assign state_init[7] = 13'h0000;
assign state_init[8] = 13'h0000;
assign state_init[9] = 13'h0000;
assign state_init[10] = 13'h0000;
assign state_init[11] = 13'h0000;
assign state_init[12] = 13'h0000;
assign state_init[13] = 13'h0000;
assign state_init[14] = 13'h0000;
assign state_init[15] = 13'h0000;
wire [12:0] ch1_init[0:15];
assign ch1_init[0] = 13'h0000;
assign ch1_init[1] = 13'h0000;
assign ch1_init[2] = 13'h0000;
assign ch1_init[3] = 13'h0000;
assign ch1_init[4] = 13'h0000;
assign ch1_init[5] = 13'h0000;
assign ch1_init[6] = 13'h0000;
assign ch1_init[7] = 13'h0000;
assign ch1_init[8] = 13'h0000;
assign ch1_init[9] = 13'h0000;
assign ch1_init[10] = 13'h0000;
assign ch1_init[11] = 13'h0000;
assign ch1_init[12] = 13'h0000;
assign ch1_init[13] = 13'h0000;
assign ch1_init[14] = 13'h0000;
assign ch1_init[15] = 13'h0000;
wire [12:0] mask_1fff[0:15];
assign mask_1fff[0] = 13'h1fff;
assign mask_1fff[1] = 13'h1fff;
assign mask_1fff[2] = 13'h1fff;
assign mask_1fff[3] = 13'h1fff;
assign mask_1fff[4] = 13'h1fff;
assign mask_1fff[5] = 13'h1fff;
assign mask_1fff[6] = 13'h1fff;
assign mask_1fff[7] = 13'h1fff;
assign mask_1fff[8] = 13'h1fff;
assign mask_1fff[9] = 13'h1fff;
assign mask_1fff[10] = 13'h1fff;
assign mask_1fff[11] = 13'h1fff;
assign mask_1fff[12] = 13'h1fff;
assign mask_1fff[13] = 13'h1fff;
assign mask_1fff[14] = 13'h1fff;
assign mask_1fff[15] = 13'h1fff;
reg [12:0] state_array[0:15];
reg [3:0] ch0_in_buf;
reg ch0_in_buf_vld;
reg [12:0] ch1_out_buf[0:15];
reg ch1_out_buf_vld;
reg stg1_vld;
wire ch1_not_vld;
wire [3:0] ch0_sel_data;
wire ch0_is_vld;
wire ch1_vld_we;
wire ch1_data_we;
wire stg0_vld_out;
wire ch0_buf_ready;
wire ch0_pipe_stall;
wire [1:0] sel_concat;
wire ch0_buf_data_we;
wire ch0_buf_vld_rst;
wire stg0_idle;
wire stg1_idle;
wire ch0_is_inactive;
wire ch1_is_inactive;
wire [12:0] next_state_val[0:15];
wire state_we;
wire ch0_buf_vld_we;
wire stg1_vld_we;
wire pipe_idle;
assign ch1_not_vld = ~ch1_out_buf_vld;
assign ch0_sel_data = ch0_in_buf_vld ? ch0_in_buf : chan_0_data;
assign ch0_is_vld = chan_0_vld | ch0_in_buf_vld;
assign ch1_vld_we = chan_1_rdy | ch1_not_vld;
assign ch1_data_we = ch0_is_vld & ch1_vld_we;
assign stg0_vld_out = ch0_is_vld & ch1_data_we;
assign ch0_buf_ready = ~ch0_in_buf_vld;
assign ch0_pipe_stall = ~stg0_vld_out;
assign sel_concat = {ch0_is_vld & ch0_sel_data[0], ch0_is_vld & ~ch0_sel_data[0]};
assign ch0_buf_data_we = chan_0_vld & ch0_buf_ready & ch0_pipe_stall;
assign ch0_buf_vld_rst = ch0_in_buf_vld & stg0_vld_out;
assign stg0_idle = ~ch0_is_vld;
assign stg1_idle = ~stg1_vld;
assign ch0_is_inactive = ~(chan_0_vld & ch0_buf_ready);
assign ch1_is_inactive = ~(ch1_out_buf_vld & chan_1_rdy);
assign next_state_val[0] = state_array[0] & {13{sel_concat[0]}} | mask_1fff[0] & {13{sel_concat[1]}};
assign next_state_val[1] = state_array[1] & {13{sel_concat[0]}} | mask_1fff[1] & {13{sel_concat[1]}};
assign next_state_val[2] = state_array[2] & {13{sel_concat[0]}} | mask_1fff[2] & {13{sel_concat[1]}};
assign next_state_val[3] = state_array[3] & {13{sel_concat[0]}} | mask_1fff[3] & {13{sel_concat[1]}};
assign next_state_val[4] = state_array[4] & {13{sel_concat[0]}} | mask_1fff[4] & {13{sel_concat[1]}};
assign next_state_val[5] = state_array[5] & {13{sel_concat[0]}} | mask_1fff[5] & {13{sel_concat[1]}};
assign next_state_val[6] = state_array[6] & {13{sel_concat[0]}} | mask_1fff[6] & {13{sel_concat[1]}};
assign next_state_val[7] = state_array[7] & {13{sel_concat[0]}} | mask_1fff[7] & {13{sel_concat[1]}};
assign next_state_val[8] = state_array[8] & {13{sel_concat[0]}} | mask_1fff[8] & {13{sel_concat[1]}};
assign next_state_val[9] = state_array[9] & {13{sel_concat[0]}} | mask_1fff[9] & {13{sel_concat[1]}};
assign next_state_val[10] = state_array[10] & {13{sel_concat[0]}} | mask_1fff[10] & {13{sel_concat[1]}};
assign next_state_val[11] = state_array[11] & {13{sel_concat[0]}} | mask_1fff[11] & {13{sel_concat[1]}};
assign next_state_val[12] = state_array[12] & {13{sel_concat[0]}} | mask_1fff[12] & {13{sel_concat[1]}};
assign next_state_val[13] = state_array[13] & {13{sel_concat[0]}} | mask_1fff[13] & {13{sel_concat[1]}};
assign next_state_val[14] = state_array[14] & {13{sel_concat[0]}} | mask_1fff[14] & {13{sel_concat[1]}};
assign next_state_val[15] = state_array[15] & {13{sel_concat[0]}} | mask_1fff[15] & {13{sel_concat[1]}};
assign state_we = stg0_vld_out & ch0_sel_data[0] | stg0_vld_out & ~ch0_sel_data[0];
assign ch0_buf_vld_we = ch0_buf_data_we | ch0_buf_vld_rst;
assign stg1_vld_we = stg0_vld_out | stg1_vld;
assign pipe_idle = stg0_idle & stg1_idle & ch0_is_inactive & ch1_is_inactive;
always @(posedge clk) begin
if (!rst_n) begin
state_array[0] <= state_init[0];
state_array[1] <= state_init[1];
state_array[2] <= state_init[2];
state_array[3] <= state_init[3];
state_array[4] <= state_init[4];
state_array[5] <= state_init[5];
state_array[6] <= state_init[6];
state_array[7] <= state_init[7];
state_array[8] <= state_init[8];
state_array[9] <= state_init[9];
state_array[10] <= state_init[10];
state_array[11] <= state_init[11];
state_array[12] <= state_init[12];
state_array[13] <= state_init[13];
state_array[14] <= state_init[14];
state_array[15] <= state_init[15];
ch0_in_buf <= 4'h0;
ch0_in_buf_vld <= 1'h0;
ch1_out_buf[0] <= ch1_init[0];
ch1_out_buf[1] <= ch1_init[1];
ch1_out_buf[2] <= ch1_init[2];
ch1_out_buf[3] <= ch1_init[3];
ch1_out_buf[4] <= ch1_init[4];
ch1_out_buf[5] <= ch1_init[5];
ch1_out_buf[6] <= ch1_init[6];
ch1_out_buf[7] <= ch1_init[7];
ch1_out_buf[8] <= ch1_init[8];
ch1_out_buf[9] <= ch1_init[9];
ch1_out_buf[10] <= ch1_init[10];
ch1_out_buf[11] <= ch1_init[11];
ch1_out_buf[12] <= ch1_init[12];
ch1_out_buf[13] <= ch1_init[13];
ch1_out_buf[14] <= ch1_init[14];
ch1_out_buf[15] <= ch1_init[15];
ch1_out_buf_vld <= 1'h0;
stg1_vld <= 1'h0;
end else begin
state_array[0] <= state_we ? next_state_val[0] : state_array[0];
state_array[1] <= state_we ? next_state_val[1] : state_array[1];
state_array[2] <= state_we ? next_state_val[2] : state_array[2];
state_array[3] <= state_we ? next_state_val[3] : state_array[3];
state_array[4] <= state_we ? next_state_val[4] : state_array[4];
state_array[5] <= state_we ? next_state_val[5] : state_array[5];
state_array[6] <= state_we ? next_state_val[6] : state_array[6];
state_array[7] <= state_we ? next_state_val[7] : state_array[7];
state_array[8] <= state_we ? next_state_val[8] : state_array[8];
state_array[9] <= state_we ? next_state_val[9] : state_array[9];
state_array[10] <= state_we ? next_state_val[10] : state_array[10];
state_array[11] <= state_we ? next_state_val[11] : state_array[11];
state_array[12] <= state_we ? next_state_val[12] : state_array[12];
state_array[13] <= state_we ? next_state_val[13] : state_array[13];
state_array[14] <= state_we ? next_state_val[14] : state_array[14];
state_array[15] <= state_we ? next_state_val[15] : state_array[15];
ch0_in_buf <= ch0_buf_data_we ? chan_0_data : ch0_in_buf;
ch0_in_buf_vld <= ch0_buf_vld_we ? ch0_buf_ready : ch0_in_buf_vld;
ch1_out_buf[0] <= ch1_data_we ? state_array[0] : ch1_out_buf[0];
ch1_out_buf[1] <= ch1_data_we ? state_array[1] : ch1_out_buf[1];
ch1_out_buf[2] <= ch1_data_we ? state_array[2] : ch1_out_buf[2];
ch1_out_buf[3] <= ch1_data_we ? state_array[3] : ch1_out_buf[3];
ch1_out_buf[4] <= ch1_data_we ? state_array[4] : ch1_out_buf[4];
ch1_out_buf[5] <= ch1_data_we ? state_array[5] : ch1_out_buf[5];
ch1_out_buf[6] <= ch1_data_we ? state_array[6] : ch1_out_buf[6];
ch1_out_buf[7] <= ch1_data_we ? state_array[7] : ch1_out_buf[7];
ch1_out_buf[8] <= ch1_data_we ? state_array[8] : ch1_out_buf[8];
ch1_out_buf[9] <= ch1_data_we ? state_array[9] : ch1_out_buf[9];
ch1_out_buf[10] <= ch1_data_we ? state_array[10] : ch1_out_buf[10];
ch1_out_buf[11] <= ch1_data_we ? state_array[11] : ch1_out_buf[11];
ch1_out_buf[12] <= ch1_data_we ? state_array[12] : ch1_out_buf[12];
ch1_out_buf[13] <= ch1_data_we ? state_array[13] : ch1_out_buf[13];
ch1_out_buf[14] <= ch1_data_we ? state_array[14] : ch1_out_buf[14];
ch1_out_buf[15] <= ch1_data_we ? state_array[15] : ch1_out_buf[15];
ch1_out_buf_vld <= ch1_vld_we ? ch0_is_vld : ch1_out_buf_vld;
stg1_vld <= stg1_vld_we ? stg0_vld_out : stg1_vld;
end
end
assign chan_0_rdy = ch0_buf_ready;
assign chan_1_data = {
ch1_out_buf[15],
ch1_out_buf[14],
ch1_out_buf[13],
ch1_out_buf[12],
ch1_out_buf[11],
ch1_out_buf[10],
ch1_out_buf[9],
ch1_out_buf[8],
ch1_out_buf[7],
ch1_out_buf[6],
ch1_out_buf[5],
ch1_out_buf[4],
ch1_out_buf[3],
ch1_out_buf[2],
ch1_out_buf[1],
ch1_out_buf[0]
};
assign chan_1_vld = ch1_out_buf_vld;
assign idle = pipe_idle;
endmodule

30
tests/opt/opt_dff_eqbits_small.sv Normal file
View file

@ -0,0 +1,30 @@
module test_case (
input wire clk,
input wire rst_n,
input wire in_val,
output wire out_a,
output wire out_b,
output wire out_c,
output wire out_d
);
reg a, b, c, d;
always @(posedge clk) begin
if (!rst_n) begin
a <= 1'b0;
b <= 1'b0;
c <= 1'b0;
d <= 1'b0;
end else begin
a <= c & in_val;
b <= d & in_val;
c <= b | in_val;
d <= a | in_val;
end
end
assign out_a = a;
assign out_b = b;
assign out_c = c;
assign out_d = d;
endmodule

267
tests/opt/opt_first_fit_alloc.ys
View file

@ -590,3 +590,270 @@ design -load postopt
select -assert-min 1 w:*ffa_*
design -reset
log -pop
# ============================================================================
# Group G: coalesce-matrix variant (precomputed same_cat[i][k], raw-input en)
# ============================================================================
#
# Some RTL precomputes a per-leader "same_cat[i][k]" mask (gated ONLY on the
# leader's enable) and forward-coalesces the leader's slot into lane k without
# re-checking en[k]. Disabled lanes after a same-category leader therefore
# inherit that leader's slot (rather than 0). The pass detects this as the
# enable-independent forward-coalescing variant. These modules also drive the
# scan straight from a top-level request port (lane_en), exercising the
# primary-input enable/broadcast candidate path.
# G1: coalesce-matrix dsel-only, raw-input enable, N=8 (equiv).
log -header "G1: coalesce-matrix allocator, raw-input enable, N=8 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module top #(parameter N=8, NB=4, C=2, W=2) (
input logic [N-1:0] lane_en,
input logic [N*C-1:0] cat_flat,
output logic [N*W-1:0] dsel_flat
);
logic [N-1:0] same_cat [0:N-1];
always_comb begin
for (int a=0;a<N;a++) begin
same_cat[a] = '0;
if (lane_en[a])
for (int b=a;b<N;b++)
if (cat_flat[a*C +: C]==cat_flat[b*C +: C]) same_cat[a][b] = 1'b1;
end
end
logic [W-1:0] dsel [0:N-1];
logic [NB-1:0] taken;
logic [N-1:0] done;
always_comb begin
for (int i=0;i<N;i++) dsel[i] = '0;
taken = '0; done = '0;
for (int i=0;i<N;i++)
if (lane_en[i])
for (int j=0;j<NB;j++)
if (!taken[j] && !done[i]) begin
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
for (int k=0;k<N;k++)
if (same_cat[i][k]) begin dsel[k] = W'(j); done[k] = 1'b1; end
end
end
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
endmodule
EOF
hierarchy -top top
proc
opt
check -assert
equiv_opt -assert opt_first_fit_alloc
design -load postopt
# The coalesce variant fired (log shows "coalesce").
select -assert-min 1 w:*ffa_*
design -reset
log -pop
# G2: coalesce-matrix dsel + xbar, N=16 -- structural. Both deep cones must
# collapse from the shared scan (dsel via the coalesce gather, xbar via the
# per-slot field gather); full equiv at N=16 is SAT-hard (see group C).
log -header "G2: coalesce-matrix dsel + xbar, N=16 structural"
log -push
design -reset
read_verilog -sv <<EOF
module top #(parameter N=16, NB=8, C=3, W=3, A=5) (
input logic [N-1:0] lane_en,
input logic [N*C-1:0] cat_flat,
input logic [N-1:0] swap_bit,
output logic [N*W-1:0] dsel_flat,
output logic [32*A-1:0] xbar_flat
);
logic [N-1:0] same_cat [0:N-1];
always_comb begin
for (int a=0;a<N;a++) begin
same_cat[a] = '0;
if (lane_en[a])
for (int b=a;b<N;b++)
if (cat_flat[a*C +: C]==cat_flat[b*C +: C]) same_cat[a][b] = 1'b1;
end
end
logic [NB-1:0] taken;
logic [N-1:0] done;
logic [W-1:0] dsel [0:N-1];
logic [A-1:0] xbar [0:31];
always_comb begin
for (int i=0;i<N;i++) dsel[i] = '0;
for (int i=0;i<32;i++) xbar[i] = '0;
taken = '0; done = '0;
for (int i=0;i<N;i++)
if (lane_en[i])
for (int j=0;j<NB;j++)
if (!taken[j] && !done[i]) begin
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
for (int l=0;l<4;l++)
xbar[(j*4)+l] = (A'(({2'b0,cat_flat[i*C +: C]}*4)+l)) ^ {3'b0, swap_bit[i], 1'b0};
for (int k=0;k<N;k++)
if (same_cat[i][k]) begin dsel[k] = W'(j); done[k] = 1'b1; end
end
end
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
for (genvar g=0;g<32;g++) assign xbar_flat[g*A +: A] = xbar[g];
endmodule
EOF
hierarchy -top top
proc
memory -nomap -norom -nordff
opt
select -assert-min 1000 t:$mux
opt_first_fit_alloc
opt_clean
select -assert-min 1 w:*ffa_*
# The deep mux chains collapse and the xbar emits $bmux table-lookups.
select -assert-max 200 t:$mux
select -assert-min 1 t:$bmux
design -reset
log -pop
# G3: coalesce-matrix but LAST-fit slot choice (scans free slots NB-1..0). The
# same_cat coalescing is present but the slot assignment is not first-fit, so
# neither the standard nor the coalesce fingerprint may match.
log -header "G3: coalesce-matrix last-fit near-miss -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module top #(parameter N=8, NB=4, C=2, W=2) (
input logic [N-1:0] lane_en,
input logic [N*C-1:0] cat_flat,
output logic [N*W-1:0] dsel_flat
);
logic [N-1:0] same_cat [0:N-1];
always_comb begin
for (int a=0;a<N;a++) begin
same_cat[a] = '0;
if (lane_en[a])
for (int b=a;b<N;b++)
if (cat_flat[a*C +: C]==cat_flat[b*C +: C]) same_cat[a][b] = 1'b1;
end
end
logic [W-1:0] dsel [0:N-1];
logic [NB-1:0] taken;
logic [N-1:0] done;
always_comb begin
for (int i=0;i<N;i++) dsel[i] = '0;
taken = '0; done = '0;
for (int i=0;i<N;i++)
if (lane_en[i])
for (int j=NB-1;j>=0;j--)
if (!taken[j] && !done[i]) begin
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
for (int k=0;k<N;k++)
if (same_cat[i][k]) begin dsel[k] = W'(j); done[k] = 1'b1; end
end
end
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
endmodule
EOF
hierarchy -top top
proc
opt
opt_first_fit_alloc
select -assert-count 0 w:*ffa_*
design -reset
log -pop
# ============================================================================
# Group H: coalesce generalization (spelling + shape variants)
# ============================================================================
#
# The coalesce variant is detected by functional fingerprinting of the dsel
# cone, so it should not depend on the exact way the same-category forwarding
# is written or on the specific N/NB/C shape. These cases vary both.
# H1: coalesce with the same-category forwarding written INLINE (no precomputed
# same_cat[i][k] matrix) -- the leader compares categories directly in its
# forward loop. Functionally identical to G1's matrix form; must still detect
# the enable-independent coalescing variant and prove equivalent.
log -header "H1: coalesce inline-compare spelling, N=8 (equiv + fires)"
log -push
design -reset
read_verilog -sv <<EOF
module top #(parameter N=8, NB=4, C=2, W=2) (
input logic [N-1:0] lane_en,
input logic [N*C-1:0] cat_flat,
output logic [N*W-1:0] dsel_flat
);
logic [W-1:0] dsel [0:N-1];
logic [NB-1:0] taken;
logic [N-1:0] done;
always_comb begin
for (int i=0;i<N;i++) dsel[i] = '0;
taken = '0; done = '0;
for (int i=0;i<N;i++)
if (lane_en[i])
for (int j=0;j<NB;j++)
if (!taken[j] && !done[i]) begin
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
for (int k=i;k<N;k++)
if (cat_flat[k*C +: C]==cat_flat[i*C +: C]) begin
dsel[k] = W'(j); done[k] = 1'b1;
end
end
end
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
endmodule
EOF
hierarchy -top top
proc
opt
check -assert
equiv_opt -assert opt_first_fit_alloc
design -load postopt
select -assert-min 1 w:*ffa_*
design -reset
log -pop
# H2: coalesce at a different shape -- N=8 lanes but NB=8 slots (twice G1's
# slot count, wider dsel W=3). Confirms the coalesce fingerprint generalizes
# across slot/field widths, not just the N=8/NB=4 shape of G1.
log -header "H2: coalesce shape N=8 NB=8 W=3 (equiv + fires)"
log -push
design -reset
read_verilog -sv <<EOF
module top #(parameter N=8, NB=8, C=2, W=3) (
input logic [N-1:0] lane_en,
input logic [N*C-1:0] cat_flat,
output logic [N*W-1:0] dsel_flat
);
logic [N-1:0] same_cat [0:N-1];
always_comb begin
for (int a=0;a<N;a++) begin
same_cat[a] = '0;
if (lane_en[a])
for (int b=a;b<N;b++)
if (cat_flat[a*C +: C]==cat_flat[b*C +: C]) same_cat[a][b] = 1'b1;
end
end
logic [W-1:0] dsel [0:N-1];
logic [NB-1:0] taken;
logic [N-1:0] done;
always_comb begin
for (int i=0;i<N;i++) dsel[i] = '0;
taken = '0; done = '0;
for (int i=0;i<N;i++)
if (lane_en[i])
for (int j=0;j<NB;j++)
if (!taken[j] && !done[i]) begin
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
for (int k=0;k<N;k++)
if (same_cat[i][k]) begin dsel[k] = W'(j); done[k] = 1'b1; end
end
end
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
endmodule
EOF
hierarchy -top top
proc
opt
check -assert
equiv_opt -assert opt_first_fit_alloc
design -load postopt
select -assert-min 1 w:*ffa_*
design -reset
log -pop

308
tests/opt/opt_prienc.ys
View file

@ -672,3 +672,311 @@ equiv_opt -assert opt_prienc
design -load postopt
design -reset
log -pop
# ============================================================================
# Group RR: round-robin (rotated priority) arbiters
# ============================================================================
#
# grant / idx_next = first set request bit scanning upward (wrapping) from
# just after a stored pointer idx_last. RTL spells this as a DEPTH-iteration
# idx-- loop over req[idx] that elaborates into a serial mux/shift chain; the
# pass replaces it with a log-depth threshold-mask + CTZ network.
# RR1: power-of-2 DEPTH -- full sequential equivalence. Both grant and
# idx_next collapse and every serial req[idx] $shiftx is removed.
log -header "RR1: round-robin arbiter, DEPTH=16 (sequential equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int DEPTH = 16) (
input logic clk,
input logic rst_n,
input logic [DEPTH-1:0] req,
output logic [$clog2(DEPTH)-1:0] grant
);
typedef logic [$clog2(DEPTH)-1:0] idx_t;
idx_t idx, idx_next, idx_last;
always_comb begin
idx = idx_last; idx_next = idx_last; grant = '0;
for (int i = 0; i < DEPTH; i++) begin
if (req[idx]) begin grant = idx; idx_next = idx; end
if (idx == 0) idx = idx_t'(DEPTH-1); else idx--;
end
end
always_ff @(posedge clk) begin
if (!rst_n) idx_last <= '0;
else if (idx_last != idx_next) idx_last <= idx_next;
end
endmodule
EOF
hierarchy -top test
proc
opt
equiv_opt -assert -multiclock opt_prienc
design -load postopt
select -assert-min 1 w:*rr*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# RR2: non-power-of-2 DEPTH -- combinational equivalence over the reachable
# pointer range (idx_last in [0,DEPTH)). We rewrite one copy of the arbiter,
# leave a reference copy untouched, and SAT-prove they agree once the pointer
# input is mapped into [0,DEPTH).
log -header "RR2: round-robin arbiter, DEPTH=13 (reachable-range equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module rr_dut #(parameter int N=13, parameter int W=4) (
input logic [N-1:0] req, input logic [W-1:0] s,
output logic [W-1:0] grant, output logic [W-1:0] idx_next
);
always_comb begin
logic [W-1:0] idx; idx=s; idx_next=s; grant='0;
for (int i=0;i<N;i++) begin
if (req[idx]) begin grant=idx; idx_next=idx; end
if (idx==0) idx=W'(N-1); else idx--;
end
end
endmodule
EOF
hierarchy -top rr_dut
proc
opt
design -save rr_gold
opt_prienc
# The serial chain collapsed into the log-depth network.
select -assert-min 1 w:*rr*
select -assert-count 0 t:$shiftx
design -save rr_gate
design -reset
design -copy-from rr_gold -as rr_ref rr_dut
design -copy-from rr_gate -as rr_dut rr_dut
read_verilog -sv <<EOF
module tb #(parameter int N=13, parameter int W=4)(input logic [N-1:0] req, input logic [W-1:0] si);
logic [W-1:0] s, g1,n1,g2,n2;
assign s = (si >= N) ? (si - N) : si;
rr_dut #(N,W) u1(.req(req),.s(s),.grant(g1),.idx_next(n1));
rr_ref #(N,W) u2(.req(req),.s(s),.grant(g2),.idx_next(n2));
always_comb begin
assert (g1 == g2);
assert (n1 == n2);
end
endmodule
EOF
hierarchy -top tb
flatten
chformal -lower
opt -full
sat -verify -prove-asserts -show-ports tb
design -reset
log -pop
# RR3: negative -- a downward-scanning arbiter (opposite rotation) is a
# different function and must not be rewritten as round-robin.
log -header "RR3: downward-scan arbiter -> no round-robin rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int N=13, parameter int W=4) (
input logic [N-1:0] req, input logic [W-1:0] s,
output logic [W-1:0] grant
);
always_comb begin
logic [W-1:0] idx; idx=s; grant='0;
for (int i=0;i<N;i++) begin
if (req[idx]) grant=idx;
if (idx==W'(N-1)) idx='0; else idx++; // scans the other way
end
end
endmodule
EOF
hierarchy -top test
proc
opt
opt_prienc
select -assert-count 0 w:*rr*
design -reset
log -pop
# RR4: DEPTH sweep, power-of-2 = 8 -- full sequential equivalence.
log -header "RR4: round-robin arbiter, DEPTH=8 (sequential equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int DEPTH = 8) (
input logic clk,
input logic rst_n,
input logic [DEPTH-1:0] req,
output logic [$clog2(DEPTH)-1:0] grant
);
typedef logic [$clog2(DEPTH)-1:0] idx_t;
idx_t idx, idx_next, idx_last;
always_comb begin
idx = idx_last; idx_next = idx_last; grant = '0;
for (int i = 0; i < DEPTH; i++) begin
if (req[idx]) begin grant = idx; idx_next = idx; end
if (idx == 0) idx = idx_t'(DEPTH-1); else idx--;
end
end
always_ff @(posedge clk) begin
if (!rst_n) idx_last <= '0;
else if (idx_last != idx_next) idx_last <= idx_next;
end
endmodule
EOF
hierarchy -top test
proc
opt
equiv_opt -assert -multiclock opt_prienc
design -load postopt
select -assert-min 1 w:*rr*
design -reset
log -pop
# RR5: DEPTH sweep, power-of-2 = 32 -- larger than any test case, full equiv.
log -header "RR5: round-robin arbiter, DEPTH=32 (sequential equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int DEPTH = 32) (
input logic clk,
input logic rst_n,
input logic [DEPTH-1:0] req,
output logic [$clog2(DEPTH)-1:0] grant
);
typedef logic [$clog2(DEPTH)-1:0] idx_t;
idx_t idx, idx_next, idx_last;
always_comb begin
idx = idx_last; idx_next = idx_last; grant = '0;
for (int i = 0; i < DEPTH; i++) begin
if (req[idx]) begin grant = idx; idx_next = idx; end
if (idx == 0) idx = idx_t'(DEPTH-1); else idx--;
end
end
always_ff @(posedge clk) begin
if (!rst_n) idx_last <= '0;
else if (idx_last != idx_next) idx_last <= idx_next;
end
endmodule
EOF
hierarchy -top test
proc
opt
equiv_opt -assert -multiclock opt_prienc
design -load postopt
select -assert-min 1 w:*rr*
design -reset
log -pop
# RR6: non-power-of-2 DEPTH=7 -- reachable-range equivalence via SAT miter,
# mirroring RR2 but at a different (odd) size to confirm the reachable-range
# handling generalizes across non-pow2 widths, not just DEPTH=13.
log -header "RR6: round-robin arbiter, DEPTH=7 (reachable-range equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module rr_dut #(parameter int N=7, parameter int W=3) (
input logic [N-1:0] req, input logic [W-1:0] s,
output logic [W-1:0] grant, output logic [W-1:0] idx_next
);
always_comb begin
logic [W-1:0] idx; idx=s; idx_next=s; grant='0;
for (int i=0;i<N;i++) begin
if (req[idx]) begin grant=idx; idx_next=idx; end
if (idx==0) idx=W'(N-1); else idx--;
end
end
endmodule
EOF
hierarchy -top rr_dut
proc
opt
design -save rr_gold
opt_prienc
select -assert-min 1 w:*rr*
design -save rr_gate
design -reset
design -copy-from rr_gold -as rr_ref rr_dut
design -copy-from rr_gate -as rr_dut rr_dut
read_verilog -sv <<EOF
module tb #(parameter int N=7, parameter int W=3)(input logic [N-1:0] req, input logic [W-1:0] si);
logic [W-1:0] s, g1,n1,g2,n2;
assign s = (si >= N) ? (si - N) : si;
rr_dut #(N,W) u1(.req(req),.s(s),.grant(g1),.idx_next(n1));
rr_ref #(N,W) u2(.req(req),.s(s),.grant(g2),.idx_next(n2));
always_comb begin
assert (g1 == g2);
assert (n1 == n2);
end
endmodule
EOF
hierarchy -top tb
flatten
chformal -lower
opt -full
sat -verify -prove-asserts -show-ports tb
design -reset
log -pop
# RR7: DIFFERENT RTL SPELLING of the same rotated-priority function. Instead of
# the customer's downward idx-- last-write-wins loop, scan UPWARD from s+1 with
# wraparound and keep the FIRST hit. This is a functionally identical arbiter
# written in an unrelated style; detection is functional so it must still fire
# and prove equivalent. (Combinational, pointer `s` an input -> full equiv at
# power-of-2 N over all pointer values.)
log -header "RR7: upward-scan spelling variant, N=16 (equiv + fires)"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int N=16, parameter int W=4) (
input logic [N-1:0] req, input logic [W-1:0] s,
output logic [W-1:0] grant
);
always_comb begin
logic [W-1:0] idx; logic found;
grant='0; found=1'b0;
for (int k=1;k<=N;k++) begin
idx = W'((s + k) % N);
if (req[idx] && !found) begin grant = idx; found = 1'b1; end
end
end
endmodule
EOF
hierarchy -top test
proc
opt
equiv_opt -assert opt_prienc
design -load postopt
select -assert-min 1 w:*rr*
design -reset
log -pop
# RR8: negative -- FIXED-priority arbiter (constant start, no rotating pointer).
# This is a plain priority encoder, not a round-robin, so no round_robin
# rewrite may fire (it may still be picked up by the ordinary PE/CTZ path,
# which is fine; we only forbid a spurious *rr* rewrite).
log -header "RR8: fixed-priority (no pointer) -> no round-robin rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module test #(parameter int N=13, parameter int W=4) (
input logic [N-1:0] req,
output logic [W-1:0] grant
);
always_comb begin
logic [W-1:0] idx; grant='0;
for (int i=0;i<N;i++) begin
idx = W'(N-1-i);
if (req[idx]) grant=idx; // last-write-wins over a fixed 0..N-1 order
end
end
endmodule
EOF
hierarchy -top test
proc
opt
opt_prienc
select -assert-count 0 w:*rr*
design -reset
log -pop

583
tests/opt/opt_priokey.ys Normal file
View file

@ -0,0 +1,583 @@
# Tests for opt_priokey
#
# The pass detects a serial "priority-by-key" set accumulator: several sources
# each carry a small key and claim it if no earlier source already did. This
# elaborates into a chain of dynamic-index reads/writes ($shiftx / $shift) into
# a wide one-hot "taken" vector, whose depth grows with both the number of
# sources P and the accumulator width S. Every dynamic read taken[key[j]] is
# provably equal to the pairwise reduction
#
# OR over i<j of ( set_guard[i] & key[i] == key[j] )
#
# so the pass replaces each read with that compare reduction and drops the wide
# dynamic indexing. Correctness of every rewrite is validated by an in-pass
# ConstEval fingerprint over the reachable key range [0,S).
#
# Each group exercises a specific facet:
# A: formal equivalence across (P,S) shapes (power-of-two S -> full equiv).
# B: structural win -- the $shiftx chain is gone after the rewrite.
# C: negative / no-op cases (no false rewrites).
#
# Convention: every object the pass emits is named with a `priokey_` suffix, so
# `select w:*priokey*` is a reliable "did the rewrite fire" probe.
# ============================================================================
# Group A: formal equivalence (equiv_opt -assert)
# ============================================================================
# A1: P=3 sources into a 64-slot accumulator (SW=6, all keys reachable).
log -header "A1: priority-by-key dedup P=3 S=64 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=3, parameter int S=64, parameter int SW=6)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
input logic [P-1:0] src,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1;
win[i] = src[i];
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# A2: P=4 sources into a 16-slot accumulator (SW=4).
log -header "A2: priority-by-key dedup P=4 S=16 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4, parameter int S=16, parameter int SW=4)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
input logic [P-1:0] src,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1;
win[i] = src[i];
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# A3: P=5 sources into an 8-slot accumulator (SW=3) -- deeper source chain.
log -header "A3: priority-by-key dedup P=5 S=8 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=5, parameter int S=8, parameter int SW=3)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
input logic [P-1:0] src,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1;
win[i] = src[i];
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
select -assert-count 0 t:$shiftx
design -reset
log -pop
# ============================================================================
# Group B: structural win (the dynamic-index chain disappears)
# ============================================================================
# B1: P=6 sources, 64-slot accumulator. Before the rewrite the serial scan uses
# per-source dynamic reads ($shiftx). After the rewrite those reads are gone,
# replaced by pairwise $eq comparisons -- the QoR (depth) win.
log -header "B1: priority-by-key structural, P=6 S=64"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=6, parameter int S=64, parameter int SW=6)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
input logic [P-1:0] src,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1;
win[i] = src[i];
end
end
endmodule
EOF
hierarchy -top t
proc
opt
# Serial baseline: the dynamic-index reads are present.
select -assert-min 1 t:$shiftx
opt_priokey
opt_clean
# The wide dynamic indexing is gone, replaced by pairwise key comparisons.
select -assert-count 0 t:$shiftx
select -assert-min 1 t:$eq
select -assert-min 1 w:*priokey*
design -reset
log -pop
# ============================================================================
# Group C: negative / no-op cases (no false rewrites)
# ============================================================================
# C1: the "taken" vector is a primary input, not a set accumulator rooted at 0.
# The dynamic read has no traceable set history, so the pass must not fire.
log -header "C1: non-accumulator dynamic read -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int S=64, parameter int SW=6)(
input logic [S-1:0] taken,
input logic [SW-1:0] sel,
output logic hit
);
assign hit = taken[sel];
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop
# C2: a plain per-lane passthrough -- no dynamic indexing at all.
log -header "C2: per-lane passthrough -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4)(
input logic [P-1:0] a,
input logic [P-1:0] b,
output logic [P-1:0] y
);
assign y = a & b;
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop
# C3: a dynamic write accumulator with NO conflict check -- every source
# unconditionally sets its key and reads are absent (win is a direct index).
# There is no taken[]-guarded read chain to rewrite.
log -header "C3: unconditional writes, no guarded read -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=3, parameter int S=16, parameter int SW=4)(
input logic [P-1:0][SW-1:0] sel,
output logic [S-1:0] taken
);
always_comb begin
taken = '0;
for (int i=0;i<P;i++)
taken[sel[i]] = 1'b1;
end
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop
# ============================================================================
# Group D: RTL-spelling variants (generalization across surface syntax)
# ============================================================================
#
# Detection is functional (the pass traces the set-accumulator structurally
# and then ConstEval-validates each read over the reachable key range), so it
# is independent of how the conflict scan is spelled. Each variant below is a
# DIFFERENT way to write the same "first source per key wins" resolution; for
# every one we require both that the rewrite fires (w:*priokey*) and that
# equiv_opt -assert proves it equivalent to the original elaboration. This is
# the core generalization claim: unseen but functionally-equivalent RTL is
# handled, not just the one spelling from the QoR case.
# D1: explicit `taken = taken | (1 << sel[i])` set (instead of the bit-select
# write taken[sel[i]]=1) and a separate `conflict` temporary for the guard.
log -header "D1: explicit shift-or set + temp guard (equiv + fires)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4, S=16, SW=4)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
output logic [P-1:0] win
);
logic [S-1:0] taken;
logic conflict;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++) begin
conflict = taken[sel[i]];
if (act[i] && !conflict) begin
win[i] = 1'b1;
taken = taken | (S'(1) << sel[i]);
end
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
design -reset
log -pop
# D2: compound guard (act[i] & en[i]) -- the per-step guard the pass keys off
# is a derived net, not a primary input. The fingerprint drives it as a free
# variable, so proving read == OR(guard & key==read_key) over free guards is
# strictly stronger than the real (correlated) guards need.
log -header "D2: compound derived guard (equiv + fires)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=5, S=32, SW=5)(
input logic [P-1:0] act,
input logic [P-1:0] en,
input logic [P-1:0][SW-1:0] sel,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if ((act[i] & en[i]) && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1;
win[i] = 1'b1;
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
design -reset
log -pop
# D3: the final accumulator state is ALSO a module output. Only the guarded
# dynamic reads are rewritten; the set-writes that build `taken` are left
# intact. equiv_opt must still prove the (untouched) taken output and the
# rewritten win outputs all match.
log -header "D3: accumulator also exported as output (equiv + fires)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4, S=16, SW=4)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
output logic [P-1:0] win,
output logic [S-1:0] taken_o
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1;
win[i] = 1'b1;
end
taken_o = taken;
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
design -reset
log -pop
# ============================================================================
# Group E: parameter sweep + non-power-of-two accumulator width
# ============================================================================
# E1: tiny shape P=2 S=4 -- lower edge of the pattern.
log -header "E1: P=2 S=4 (equiv, edge)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=2, S=4, SW=2)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
input logic [P-1:0] src,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1; win[i] = src[i];
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
design -reset
log -pop
# E2: deep shape P=8 S=32 -- more sources than any QoR case, longer chain.
log -header "E2: P=8 S=32 (equiv, deep chain)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=8, S=32, SW=5)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
input logic [P-1:0] src,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1; win[i] = src[i];
end
end
endmodule
EOF
hierarchy -top t
proc
opt
check -assert
equiv_opt -assert opt_priokey
design -load postopt
select -assert-min 1 w:*priokey*
design -reset
log -pop
# E3: NON-power-of-two accumulator S=12 (SW=4, so the key bus spans [0,16) but
# only [0,12) are valid slots). The default (non-strict) rewrite is guaranteed
# only over the REACHABLE key range [0,S); it is NOT unconditionally equivalent
# (reads for keys in [12,16) index out of range). We prove the reachable-range
# guarantee rigorously with a SAT miter that clamps every key into [0,S) and
# compares the rewritten copy against an untouched reference (cf. RR2). The
# rewrite must fire AND agree with the reference for all in-range keys.
log -header "E3: non-pow2 S=12 reachable-range equivalence (SAT miter)"
log -push
design -reset
read_verilog -sv <<EOF
module pk_dut #(parameter int P=4, S=12, SW=4)(
input logic [P-1:0] act,
input logic [P*SW-1:0] sel_flat,
output logic [P-1:0] win
);
logic [SW-1:0] sel [0:P-1];
for (genvar g=0; g<P; g++) assign sel[g] = sel_flat[g*SW +: SW];
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1; win[i] = 1'b1;
end
end
endmodule
EOF
hierarchy -top pk_dut
proc
opt
design -save pk_gold
opt_priokey
select -assert-min 1 w:*priokey*
opt_clean
design -save pk_gate
design -reset
design -copy-from pk_gold -as pk_ref pk_dut
design -copy-from pk_gate -as pk_dut pk_dut
read_verilog -sv <<EOF
module tb #(parameter int P=4, S=12, SW=4)(
input logic [P-1:0] act, input logic [P*SW-1:0] sel_raw
);
logic [P*SW-1:0] sel_c;
for (genvar g=0; g<P; g++) begin : clamp
wire [SW-1:0] k = sel_raw[g*SW +: SW];
assign sel_c[g*SW +: SW] = (k >= SW'(S)) ? (k - SW'(S)) : k; // into [0,S)
end
logic [P-1:0] w1, w2;
pk_dut #(P,S,SW) u1(.act(act), .sel_flat(sel_c), .win(w1));
pk_ref #(P,S,SW) u2(.act(act), .sel_flat(sel_c), .win(w2));
always_comb assert (w1 == w2);
endmodule
EOF
hierarchy -top tb
flatten
chformal -lower
opt -full
sat -verify -prove-asserts -show-ports tb
design -reset
log -pop
# E4: SAME non-pow2 S=12 under -strict. Strict validation sweeps the FULL key
# range and rejects rewrites that only hold via out-of-range don't-cares, so
# the pass must decline to rewrite. This is the safety mode used by formal
# synthesis flows: no reliance on out-of-range freedom.
log -header "E4: non-pow2 S=12 -strict -> no rewrite (safety)"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4, S=12, SW=4)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken[sel[i]] = 1'b1; win[i] = 1'b1;
end
end
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey -strict
select -assert-count 0 w:*priokey*
design -reset
log -pop
# ============================================================================
# Group F: additional near-miss negatives (no false rewrites)
# ============================================================================
# F1: CLEAR accumulator -- `avail` starts all-ones and bits are cleared. The
# read cone does not bottom out at constant zero, so the accumulator trace
# fails and nothing is rewritten.
log -header "F1: clear-accumulator (rooted at all-ones) -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=4, S=16, SW=4)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
output logic [P-1:0] win
);
logic [S-1:0] avail;
always_comb begin
avail = '1; win = '0;
for (int i=0;i<P;i++)
if (act[i] && avail[sel[i]]) begin
avail[sel[i]] = 1'b0; win[i] = 1'b1;
end
end
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop
# F2: MULTI-hot set mask -- each source sets two adjacent slots (3 << sel).
# The set arm is not a single one-hot (1 << key), so decode_onehot_key fails
# and the accumulator is not recognized as a priority-by-key set chain.
log -header "F2: multi-hot set mask -> no rewrite"
log -push
design -reset
read_verilog -sv <<EOF
module t #(parameter int P=3, S=16, SW=4)(
input logic [P-1:0] act,
input logic [P-1:0][SW-1:0] sel,
output logic [P-1:0] win
);
logic [S-1:0] taken;
always_comb begin
taken = '0; win = '0;
for (int i=0;i<P;i++)
if (act[i] && !taken[sel[i]]) begin
taken = taken | (S'(3) << sel[i]);
win[i] = 1'b1;
end
end
endmodule
EOF
hierarchy -top t
proc
opt
opt_priokey
select -assert-count 0 w:*priokey*
design -reset
log -pop

457
tests/silimate/carvenetlist.ys Normal file
View file

@ -0,0 +1,457 @@
# =============================================================================
# carvenetlist: carve surround-with-flops cells into per-cell modules.
#
# Each "train" below is one flat cell-under-test surrounded by launch/capture
# flops (ml.dataset.surround_with_flops form): every data input is a launch
# flop's Q (named <base>_<pin>__pqi) and every data output feeds a capture flop's
# D (named <base>_<pin>__pqo), with a shared fast_clk/slow_clk. carvenetlist must
# carve the logic between the flops into module `cell` with a clean input port
# fast_cell_A and a clean output port fast_cell_Y (never inout), preserving
# feed-throughs (output bit = input bit, or = constant) as plain assigns.
# =============================================================================
# -----------------------------------------------------------------------------
# Test 1: feed-through output bit (Y[0] = A[0]).
# Regression: the bare alias used to fuse the launch-side input net with the
# capture-side output net, leaving Y[0] undriven and dragging the Y bus to inout.
# -----------------------------------------------------------------------------
log -header "Feed-through output bit (Y[0] = A[0])"
log -push
design -reset
read_rtlil <<EOF
autoidx 1
module \train
wire input 1 \fast_clk
wire input 2 \slow_clk
wire width 3 input 3 \fast_cell_A
wire width 3 output 4 \fast_cell_Y
wire width 3 \fast_cell_A__pqi
wire width 3 \fast_cell_Y__pqo
cell $_DFF_P_ \linff0
connect \C \fast_clk
connect \D \fast_cell_A [0]
connect \Q \fast_cell_A__pqi [0]
end
cell $_DFF_P_ \linff1
connect \C \fast_clk
connect \D \fast_cell_A [1]
connect \Q \fast_cell_A__pqi [1]
end
cell $_DFF_P_ \linff2
connect \C \fast_clk
connect \D \fast_cell_A [2]
connect \Q \fast_cell_A__pqi [2]
end
cell $_NOT_ \g_not
connect \A \fast_cell_A__pqi [1]
connect \Y \fast_cell_Y__pqo [1]
end
cell $_AND_ \g_and
connect \A \fast_cell_A__pqi [1]
connect \B \fast_cell_A__pqi [2]
connect \Y \fast_cell_Y__pqo [2]
end
connect \fast_cell_Y__pqo [0] \fast_cell_A__pqi [0]
cell $_DFF_P_ \coutff0
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [0]
connect \Q \fast_cell_Y [0]
end
cell $_DFF_P_ \coutff1
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [1]
connect \Q \fast_cell_Y [1]
end
cell $_DFF_P_ \coutff2
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [2]
connect \Q \fast_cell_Y [2]
end
end
EOF
flatten -noscopeinfo
carvenetlist
# carved cell exists, flops are gone, no temporary buffers survive
select -assert-none cell/t:$_DFF_P_
select -assert-none cell/t:$_BUF_
# fast_cell_A is a pure input, fast_cell_Y a pure output (never inout)
select -assert-count 1 cell/i:fast_cell_A
select -assert-none cell/o:fast_cell_A
select -assert-count 1 cell/o:fast_cell_Y
select -assert-none cell/i:fast_cell_Y
# no boundary marker (__pqi/__pqo) survives on any net, port or internal
select -assert-none cell/w:*__pqo*
select -assert-none cell/w:*__pqi*
# the carved cell is functionally correct (feed-through preserved)
read_verilog <<EOF
module golden(fast_cell_A, fast_cell_Y);
input [2:0] fast_cell_A;
output [2:0] fast_cell_Y;
assign fast_cell_Y[0] = fast_cell_A[0];
assign fast_cell_Y[1] = ~fast_cell_A[1];
assign fast_cell_Y[2] = fast_cell_A[1] & fast_cell_A[2];
endmodule
EOF
miter -equiv -flatten -make_assert golden cell miter
sat -verify -prove-asserts -enable_undef miter
design -reset
log -pop
# -----------------------------------------------------------------------------
# Test 2: constant output bit (Y[0] = 1'b0) preserved as an assign.
# -----------------------------------------------------------------------------
log -header "Constant output bit (Y[0] = 1'b0)"
log -push
design -reset
read_rtlil <<EOF
autoidx 1
module \train
wire input 1 \fast_clk
wire input 2 \slow_clk
wire width 3 input 3 \fast_cell_A
wire width 3 output 4 \fast_cell_Y
wire width 3 \fast_cell_A__pqi
wire width 3 \fast_cell_Y__pqo
cell $_DFF_P_ \linff0
connect \C \fast_clk
connect \D \fast_cell_A [0]
connect \Q \fast_cell_A__pqi [0]
end
cell $_DFF_P_ \linff1
connect \C \fast_clk
connect \D \fast_cell_A [1]
connect \Q \fast_cell_A__pqi [1]
end
cell $_DFF_P_ \linff2
connect \C \fast_clk
connect \D \fast_cell_A [2]
connect \Q \fast_cell_A__pqi [2]
end
cell $_NOT_ \g_not
connect \A \fast_cell_A__pqi [1]
connect \Y \fast_cell_Y__pqo [1]
end
cell $_AND_ \g_and
connect \A \fast_cell_A__pqi [1]
connect \B \fast_cell_A__pqi [2]
connect \Y \fast_cell_Y__pqo [2]
end
connect \fast_cell_Y__pqo [0] 1'0
cell $_DFF_P_ \coutff0
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [0]
connect \Q \fast_cell_Y [0]
end
cell $_DFF_P_ \coutff1
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [1]
connect \Q \fast_cell_Y [1]
end
cell $_DFF_P_ \coutff2
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [2]
connect \Q \fast_cell_Y [2]
end
end
EOF
flatten -noscopeinfo
carvenetlist
select -assert-none cell/t:$_BUF_
select -assert-count 1 cell/o:fast_cell_Y
select -assert-none cell/i:fast_cell_Y
read_verilog <<EOF
module golden(fast_cell_A, fast_cell_Y);
input [2:0] fast_cell_A;
output [2:0] fast_cell_Y;
assign fast_cell_Y[0] = 1'b0;
assign fast_cell_Y[1] = ~fast_cell_A[1];
assign fast_cell_Y[2] = fast_cell_A[1] & fast_cell_A[2];
endmodule
EOF
miter -equiv -flatten -make_assert golden cell miter
sat -verify -prove-asserts -enable_undef miter
design -reset
log -pop
# -----------------------------------------------------------------------------
# Test 3: no feed-through (every output bit driven by logic) still carves clean.
# -----------------------------------------------------------------------------
log -header "No feed-through (all outputs from logic)"
log -push
design -reset
read_rtlil <<EOF
autoidx 1
module \train
wire input 1 \fast_clk
wire input 2 \slow_clk
wire width 3 input 3 \fast_cell_A
wire width 3 output 4 \fast_cell_Y
wire width 3 \fast_cell_A__pqi
wire width 3 \fast_cell_Y__pqo
cell $_DFF_P_ \linff0
connect \C \fast_clk
connect \D \fast_cell_A [0]
connect \Q \fast_cell_A__pqi [0]
end
cell $_DFF_P_ \linff1
connect \C \fast_clk
connect \D \fast_cell_A [1]
connect \Q \fast_cell_A__pqi [1]
end
cell $_DFF_P_ \linff2
connect \C \fast_clk
connect \D \fast_cell_A [2]
connect \Q \fast_cell_A__pqi [2]
end
cell $_NOT_ \g_not0
connect \A \fast_cell_A__pqi [0]
connect \Y \fast_cell_Y__pqo [0]
end
cell $_NOT_ \g_not1
connect \A \fast_cell_A__pqi [1]
connect \Y \fast_cell_Y__pqo [1]
end
cell $_AND_ \g_and
connect \A \fast_cell_A__pqi [1]
connect \B \fast_cell_A__pqi [2]
connect \Y \fast_cell_Y__pqo [2]
end
cell $_DFF_P_ \coutff0
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [0]
connect \Q \fast_cell_Y [0]
end
cell $_DFF_P_ \coutff1
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [1]
connect \Q \fast_cell_Y [1]
end
cell $_DFF_P_ \coutff2
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [2]
connect \Q \fast_cell_Y [2]
end
end
EOF
flatten -noscopeinfo
carvenetlist
select -assert-none cell/t:$_BUF_
select -assert-count 1 cell/i:fast_cell_A
select -assert-none cell/o:fast_cell_A
select -assert-count 1 cell/o:fast_cell_Y
select -assert-none cell/i:fast_cell_Y
read_verilog <<EOF
module golden(fast_cell_A, fast_cell_Y);
input [2:0] fast_cell_A;
output [2:0] fast_cell_Y;
assign fast_cell_Y[0] = ~fast_cell_A[0];
assign fast_cell_Y[1] = ~fast_cell_A[1];
assign fast_cell_Y[2] = fast_cell_A[1] & fast_cell_A[2];
endmodule
EOF
miter -equiv -flatten -make_assert golden cell miter
sat -verify -prove-asserts -enable_undef miter
design -reset
log -pop
# -----------------------------------------------------------------------------
# Test 4: flatten-scope-prefixed boundary net (dotted name "fast_cell.fast_cell_Y__pqo").
# After flatten -noscopeinfo, an output-boundary net carried up from an inner
# instance keeps a dotted scope prefix. A constant/feed-through bit on that net is
# bufferized but NOT re-tagged by the cone walk, so the submodule tag is derived
# straight from the net name. Regression: the tag used to retain the scope prefix,
# producing an invalid carved module name "cell.fast_cell" (a separate, broken
# module) instead of folding the bit into module `cell`.
# -----------------------------------------------------------------------------
log -header "Flatten-scope-prefixed boundary net (dotted Y__pqo)"
log -push
design -reset
read_rtlil <<EOF
autoidx 1
module \train
wire input 1 \fast_clk
wire width 2 input 2 \fast_cell_A
wire width 2 output 3 \fast_cell_Y
wire width 2 \fast_cell_A__pqi
wire width 2 \fast_cell.fast_cell_Y__pqo
cell $_DFF_P_ \linff0
connect \C \fast_clk
connect \D \fast_cell_A [0]
connect \Q \fast_cell_A__pqi [0]
end
cell $_DFF_P_ \linff1
connect \C \fast_clk
connect \D \fast_cell_A [1]
connect \Q \fast_cell_A__pqi [1]
end
cell $_AND_ \g_and
connect \A \fast_cell_A__pqi [0]
connect \B \fast_cell_A__pqi [1]
connect \Y \fast_cell.fast_cell_Y__pqo [1]
end
connect \fast_cell.fast_cell_Y__pqo [0] 1'0
cell $_DFF_P_ \coutff0
connect \C \fast_clk
connect \D \fast_cell.fast_cell_Y__pqo [0]
connect \Q \fast_cell_Y [0]
end
cell $_DFF_P_ \coutff1
connect \C \fast_clk
connect \D \fast_cell.fast_cell_Y__pqo [1]
connect \Q \fast_cell_Y [1]
end
end
EOF
flatten -noscopeinfo
carvenetlist
# the carved module is named `cell` (no scope dot) with a clean pure-output port
select -assert-none cell/t:$_BUF_
select -assert-count 1 cell/o:fast_cell_Y
select -assert-none cell/i:fast_cell_Y
read_verilog <<EOF
module golden(fast_cell_A, fast_cell_Y);
input [1:0] fast_cell_A;
output [1:0] fast_cell_Y;
assign fast_cell_Y[0] = 1'b0;
assign fast_cell_Y[1] = fast_cell_A[0] & fast_cell_A[1];
endmodule
EOF
miter -equiv -flatten -make_assert golden cell miter
sat -verify -prove-asserts -enable_undef miter
design -reset
log -pop
# -----------------------------------------------------------------------------
# Test 5: full pass-through cell (Y = A, no logic at all) -- div/mod/shift in a
# degenerate mode where synthesis collapses every output bit into a bare copy of
# an input. The capture flops then read the launch-flop nets directly: there is
# no in-cone net to export, so without the capture-flop-boundary buffer the whole
# Y bus has no internal driver and the carved cell has no output port at all.
# carvenetlist must still produce a clean input fast_cell_A and output fast_cell_Y
# with assign Y = A.
# -----------------------------------------------------------------------------
log -header "Full pass-through cell (Y = A, no logic)"
log -push
design -reset
read_rtlil <<EOF
autoidx 1
module \train
wire input 1 \fast_clk
wire width 2 input 2 \fast_cell_A
wire width 2 output 3 \fast_cell_Y
wire width 2 \fast_cell_A__pqi
wire width 2 \fast_cell_Y__pqo
cell $_DFF_P_ \linff0
connect \C \fast_clk
connect \D \fast_cell_A [0]
connect \Q \fast_cell_A__pqi [0]
end
cell $_DFF_P_ \linff1
connect \C \fast_clk
connect \D \fast_cell_A [1]
connect \Q \fast_cell_A__pqi [1]
end
connect \fast_cell_Y__pqo \fast_cell_A__pqi
cell $_DFF_P_ \coutff0
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [0]
connect \Q \fast_cell_Y [0]
end
cell $_DFF_P_ \coutff1
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [1]
connect \Q \fast_cell_Y [1]
end
end
EOF
flatten -noscopeinfo
carvenetlist
select -assert-none cell/t:$_BUF_
select -assert-count 1 cell/i:fast_cell_A
select -assert-none cell/o:fast_cell_A
select -assert-count 1 cell/o:fast_cell_Y
select -assert-none cell/i:fast_cell_Y
select -assert-none cell/w:*__pqo*
select -assert-none cell/w:*__pqi*
read_verilog <<EOF
module golden(fast_cell_A, fast_cell_Y);
input [1:0] fast_cell_A;
output [1:0] fast_cell_Y;
assign fast_cell_Y = fast_cell_A;
endmodule
EOF
miter -equiv -flatten -make_assert golden cell miter
sat -verify -prove-asserts -enable_undef miter
design -reset
log -pop
# -----------------------------------------------------------------------------
# Test 6: constant output bit driven by a zero-input source cell (a "tie"), not a
# 1'b0 connection. abc maps a constant output to a TIEHI/TIELO standard cell; the
# tie has no inputs so the forward cone walk can never reach it, and it would be
# stranded in the deleted train module, leaving the output bit undriven. A $lut
# with WIDTH=0 models such a zero-input constant source. carvenetlist must clone
# the tie into the carved cell so the output bit keeps an in-cone driver. Here
# Y[0] is real logic and Y[1] is the tie constant, on the same Y bus.
# -----------------------------------------------------------------------------
log -header "Constant output from a zero-input tie cell (cloned into cell)"
log -push
design -reset
read_rtlil <<EOF
autoidx 1
module \train
wire input 1 \fast_clk
wire width 1 input 2 \fast_cell_A
wire width 2 output 3 \fast_cell_Y
wire width 1 \fast_cell_A__pqi
wire width 2 \fast_cell_Y__pqo
cell $_DFF_P_ \linff0
connect \C \fast_clk
connect \D \fast_cell_A [0]
connect \Q \fast_cell_A__pqi [0]
end
cell $_NOT_ \g_not
connect \A \fast_cell_A__pqi [0]
connect \Y \fast_cell_Y__pqo [0]
end
cell $lut \tie
parameter \WIDTH 0
parameter \LUT 1'1
connect \A {}
connect \Y \fast_cell_Y__pqo [1]
end
cell $_DFF_P_ \coutff0
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [0]
connect \Q \fast_cell_Y [0]
end
cell $_DFF_P_ \coutff1
connect \C \fast_clk
connect \D \fast_cell_Y__pqo [1]
connect \Q \fast_cell_Y [1]
end
end
EOF
flatten -noscopeinfo
carvenetlist
# the tie was cloned into the carved cell (so the constant bit has an in-cone driver)
select -assert-count 1 cell/t:$lut
select -assert-none cell/t:$_BUF_
select -assert-count 1 cell/i:fast_cell_A
select -assert-none cell/o:fast_cell_A
select -assert-count 1 cell/o:fast_cell_Y
select -assert-none cell/i:fast_cell_Y
select -assert-none cell/w:*__pqo*
select -assert-none cell/w:*__pqi*
read_verilog <<EOF
module golden(fast_cell_A, fast_cell_Y);
input [0:0] fast_cell_A;
output [1:0] fast_cell_Y;
assign fast_cell_Y[0] = ~fast_cell_A[0];
assign fast_cell_Y[1] = 1'b1;
endmodule
EOF
miter -equiv -flatten -make_assert golden cell miter
sat -verify -prove-asserts -enable_undef miter
design -reset
log -pop

4
tests/various/test_splitnets.tcl
View file

@ -7,10 +7,10 @@ proc read_stats { file } {
set ports 0
set nets 0
foreach line [split $result "\n"] {
if [regexp {Number of wires:[ \t]+([0-9]+)} $line tmp n] {
if [regexp {\s([0-9]+) wires} $line tmp n] {
set nets [expr $nets + $n]
}
if [regexp {Number of ports:[ \t]+([0-9]+)} $line tmp n] {
if [regexp {(\s[0-9]+) ports} $line tmp n] {
set ports [expr $ports + $n]
}
}

2
verific

@ -1 +1 @@
Subproject commit cee2b14fdace74e89b699027a6e8f28fb86613c5
Subproject commit 324ed5d92aa63128bd0382c7f013d63719e08079