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

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

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

    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
    pub struct State {
        arr: BitvectorArray<5, 32>,
    }

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

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

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

        fn init(&self, _input: &Input, _param: &Param) -> State {
            State {
                arr: BitvectorArray::<5, 32>::new_filled(Bitvector::<32>::new(0)),
            }
        }

        fn next(&self, state: &State, _input: &Input, _param: &Param) -> State {
            let mut arr = Clone::clone(&state.arr);

            if Bitvector::<2>::new(0) == Bitvector::<2>::new(1) {
                if Bitvector::<2>::new(0) == Bitvector::<2>::new(1) {
                    arr[Bitvector::<5>::new(0)] = Bitvector::<32>::new(0xDEDA);
                };
            };

            State { arr }
        }
    }
}

fn main() {}