1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#pragma once
8
9#include <config.h>
10#include <types.h>
11#include <arch/model/statedata.h>
12
13static inline CONST uint64_t div64(uint64_t numerator, uint32_t denominator)
14{
15    uint64_t quotient = 0llu;
16    uint64_t long_denom = (uint64_t) denominator;
17
18    if (unlikely(denominator > numerator)) {
19        return 0;
20    }
21
22    assert(numerator > 0);
23    assert(denominator > 0);
24
25    /* align denominator to numerator */
26    uint64_t c = ((uint64_t) 32u + clzl(denominator)) - clzll(numerator);
27    long_denom = long_denom << c;
28
29    /* perform binary long division */
30    while (c < UINT64_MAX) {
31        if (numerator >= long_denom) {
32            numerator -= long_denom;
33            quotient |= (1llu << c);
34        }
35        c--;
36        long_denom = long_denom >> 1llu;
37    }
38
39    return quotient;
40}
41
42