blob: b949a545509fb7b151b5f973d0eb7237040a360a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
default Order dec
$include <prelude.sail>
val lzcnt = "count_leading_zeros" : forall 'w, 'w >= 1. bits('w) -> range(0, 'w)
$property
function prop(bv: bits(5)) -> bool = {
let x = unsigned(bv);
if x > 0 then {
let z = sail_zeros(x);
let p1 = lzcnt(z) == x;
let p2 = lzcnt(z @ 0xF) == x;
let p3 = lzcnt(0x0 @ z) == 4 + x;
p1 & p2
} else true
}
|
