machine-check 0.7.1

Formal verification tool for digital systems
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69

//! Example of some supported array manipulations.
//!
//! Arrays can be newly created by new_filled, written to, read from, and be cloned.
//! They are stored sparsely, so we can represent even an array with 64-bit
//! indices as long as only a part of the array has distinct values.

#[machine_check::machine_description]
mod machine_module {
    use ::machine_check::Bitvector;
    use ::machine_check::BitvectorArray;
    use ::std::{
        clone::Clone,
        cmp::{Eq, PartialEq},
        fmt::Debug,
        hash::Hash,
        panic,
    };

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct Input {
        value: Bitvector<16>,
        array: BitvectorArray<64, 16>,
    }

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct Param {}

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct State {
        array: BitvectorArray<64, 16>,
    }

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct System {}

    impl ::machine_check::Machine for System {
        type Input = Input;
        type Param = Param;
        type State = State;

        fn init(&self, _input: &Input, _param: &Param) -> State {
            let mut array = BitvectorArray::<64, 16>::new_filled(Bitvector::<16>::new(0xCAFE));
            let baba_index = Bitvector::<64>::new(0xBABA);
            array[baba_index] = Bitvector::<16>::new(0xDEDA);
            State { array }
        }

        fn next(&self, state: &State, input: &Input, _param: &Param) -> State {
            let max_index = Bitvector::<64>::new(0xFFFF_FFFF_FFFF_FFFF);
            if state.array[max_index] != Bitvector::<16>::new(0xCAFE) {
                panic!("Array element 0xFFFF_FFFF_FFFF_FFFF not 0xCAFE as expected");
            }
            let baba_index = Bitvector::<64>::new(0xBABA);
            if state.array[baba_index] != Bitvector::<16>::new(0xDEDA) {
                panic!("Array element 0xBABA not 0xDEDA as expected");
            }
            let mut array = BitvectorArray::<64, 16>::new_filled(input.value);
            array[baba_index] = Bitvector::<16>::new(0xDEDA);
            array[max_index] = Bitvector::<16>::new(0xCAFE);

            State { array }
        }
    }
}

fn main() {
    let system = machine_module::System {};
    machine_check::run(system);
}