Skip to main content

litex/builtin_code/
common_functions.rs

1pub const BUILTIN_ENV_CODE_FOR_COMMON_FUNCTIONS: &str = r#"
2know:
3    forall x R:
4        0 <= abs(x)
5        abs(x) = x or abs(x) = -x
6
7    forall x, y R:
8        abs(x * y) = abs(x) * abs(y)
9
10know:
11    forall x, y R:
12        x <= max(x, y)
13        y <= max(x, y)
14
15know:
16    forall x, y R:
17        min(x, y) <= x
18        min(x, y) <= y
19"#;