|
| 1 | +// ======================================================================================= |
| 2 | +// This Sail RISC-V architecture model, comprising all files and |
| 3 | +// directories except where otherwise noted is subject the BSD |
| 4 | +// two-clause license in the LICENSE file. |
| 5 | +// |
| 6 | +// SPDX-License-Identifier: BSD-2-Clause |
| 7 | +// ======================================================================================= |
| 8 | + |
| 9 | +// Return true if the right-open range `a` is a subset of `b` (or equal to it). |
| 10 | +// Ranges wrap around the end. The 64 bit limit is just so Sail generates more |
| 11 | +// efficient C code. |
| 12 | +function range_subset forall 'n, 0 <= 'n <= 64 . ( |
| 13 | + a_begin : bits('n), |
| 14 | + a_size : bits('n), |
| 15 | + b_begin : bits('n), |
| 16 | + b_size : bits('n), |
| 17 | +) -> bool = { |
| 18 | + // Rotate so that be starts at 0. |
| 19 | + let a_end = (a_begin + a_size) - b_begin; |
| 20 | + let b_end = (b_begin + b_size) - b_begin; |
| 21 | + let a_begin = a_begin - b_begin; |
| 22 | + a_begin <=_u b_end & a_end <=_u b_end & a_begin <=_u a_end |
| 23 | +} |
| 24 | + |
| 25 | +$[test] |
| 26 | +function test_range_subset() -> unit = { |
| 27 | + assert(range_subset(0x0, 0x0, 0x0, 0x0)); |
| 28 | + assert(range_subset(0x1, 0x0, 0x1, 0x0)); |
| 29 | + assert(range_subset(0x0, 0x0, 0x0, 0x1)); |
| 30 | + assert(range_subset(0x1, 0x0, 0x0, 0x1)); |
| 31 | + assert(range_subset(0x8, 0xc, 0x8, 0xc)); |
| 32 | + assert(not(range_subset(0x8, 0xc, 0x9, 0xc))); |
| 33 | + assert(not(range_subset(0x8, 0xc, 0x8, 0xb))); |
| 34 | + assert(not(range_subset(0x3e, 0xe0, 0xc1, 0x9f))); |
| 35 | + assert(not(range_subset(0xc1, 0x9f, 0x3e, 0xe0))); |
| 36 | +} |
| 37 | + |
| 38 | +// Check if two ranges are subsets of each other they must be equal. |
| 39 | +$[property] |
| 40 | +function range_subset_equals(a_begin : bits(8), a_size : bits(8), b_begin : bits(8), b_size : bits(8)) -> bool = |
| 41 | + range_subset(a_begin, a_size, b_begin, b_size) & range_subset(b_begin, b_size, a_begin, a_size) |
| 42 | + ==> (a_begin == b_begin & a_size == b_size) |
| 43 | + |
| 44 | +// Check that if A is a subset of B, then all indices in A must be in B. |
| 45 | +// Also check that an index exists that is in A but not B then A cannot be a subset of B. |
| 46 | +$[property] |
| 47 | +function range_subset_precise(a_begin : bits(8), a_size : bits(8), b_begin : bits(8), b_size : bits(8), index : bits(8)) -> bool = { |
| 48 | + let index_in_a = (index - a_begin) <_u a_size; |
| 49 | + let index_in_b = (index - b_begin) <_u b_size; |
| 50 | + let is_subset = range_subset(a_begin, a_size, b_begin, b_size); |
| 51 | + |
| 52 | + (is_subset & index_in_a ==> index_in_b) & ((index_in_a & not(index_in_b)) ==> not(is_subset)) |
| 53 | +} |
0 commit comments