google / xls

XLS: Accelerated HW Synthesis
http://google.github.io/xls/
Apache License 2.0
1.16k stars 165 forks source link

[DSLX] quickcheck support for parametric functions #81

Open cdleary opened 3 years ago

cdleary commented 3 years ago

cc @hmontero1205

In #70 support for quickchecking non-parametric functions is introduced -- we'll want a way to let the quickcheck "driver" instantiate parametric functions with the ability to put constraints on the parametric values. One nice aspect of this is the quickcheck driver can use normal functions to test properties of normal values (e.g. filtering via is_even as a predicate on a given parametric N: u32) and then use that value to drive the instantiation. This will make the quickcheck less vectorizable, but we can vector-test some number of samples for any given parametric N chosen to get some batch efficiency.

cdleary commented 2 years ago

Not currently on the "implement soon" radar so marking as long-term enhancement.

proppy commented 1 year ago

It seems at least possible to quickcheck parametric function by instanciating them explicitly:

fn func1<N: u32>(a: uN[N], b: uN[N]) -> uN[N] {
    a + b
}

fn func2<N: u32>(a: uN[N], b: uN[N]) -> uN[N] {
    b + a
}

#[quickcheck(test_count=50000)]
fn prop_func1_equal_func2(a: u32, b: u32) -> bool {
    func1<u32:32>(a, b) == func2<u32:32>(a, b)
}
[ RUN QUICKCHECK        ] prop_func1_equal_func2 count: 50000
[                    OK ] prop_func1_equal_func2