simple_risc/
simple_risc.rs

1//! An example system of an extremely simplified RISC
2//! (Reduced Instruction Set Computer) microcontroller
3//! with toy machine code, forming a system that
4//! can be verified by machine-check.
5//!
6//! Only the things specific to the microcontroller will
7//! be commented here. See the example "counter"
8//! for a basic description of a machine-check system.
9//!
10//! Some of the properties that hold and are verifiable:
11//!  - Register 1 is set to 1 before reaching the start
12//!    of the main loop:
13//!    `AF![reg[1] == 1 && as_unsigned(pc) < 3]`
14//!  - It is always possible to reach program location 9:
15//!    `AG![EF![pc == 9]]`
16//!    (use the decay strategy when verifying this)
17//!  - Program locations above 9 are never reached.
18//!    `AG![as_unsigned(pc) <= 9]`
19//!    (use the decay strategy when verifying this)
20
21#[machine_check::machine_description]
22mod machine_module {
23    use ::machine_check::{Bitvector, BitvectorArray};
24    use ::std::{
25        clone::Clone,
26        cmp::{Eq, PartialEq},
27        fmt::Debug,
28        hash::Hash,
29    };
30
31    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
32    pub struct Input {
33        // Proper inputs to this microcontroller
34        // are addresses that can be read.
35        gpio_read: BitvectorArray<4, 8>,
36        // Registers and data are uninitialized
37        // at microcontroller reset, which corresponds to
38        // finite-state machine init.
39        uninit_reg: BitvectorArray<2, 8>,
40        uninit_data: BitvectorArray<8, 8>,
41    }
42    impl ::machine_check::Input for Input {}
43
44    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
45    pub struct State {
46        // Microcontroller program counter.
47        // Stores the address of instruction
48        // in program memory that will be executed next.
49        pc: Bitvector<7>,
50        // Four (2^2) 8-bit working registers.
51        reg: BitvectorArray<2, 8>,
52        // 256 (2^8) 8-bit data cells.
53        data: BitvectorArray<8, 8>,
54    }
55    impl ::machine_check::State for State {}
56    #[derive(Clone, PartialEq, Eq, Hash, Debug)]
57    pub struct System {
58        // 128 (2^7) 12-bit program memory instructions.
59        pub progmem: BitvectorArray<7, 12>,
60    }
61    impl ::machine_check::Machine for System {
62        type Input = Input;
63        type State = State;
64
65        fn init(&self, input: &Input) -> State {
66            // Only initialize Program Counter to 0 at reset.
67            // Leave working registers and data uninitialized.
68            State {
69                pc: Bitvector::<7>::new(0),
70                reg: Clone::clone(&input.uninit_reg),
71                data: Clone::clone(&input.uninit_data),
72            }
73        }
74        fn next(&self, state: &State, input: &Input) -> State {
75            // Fetch the instruction to execute from program memory.
76            let instruction = self.progmem[state.pc];
77            // Increment the program counter.
78            let mut pc = state.pc + Bitvector::<7>::new(1);
79            // Clone registers and data.
80            let mut reg = Clone::clone(&state.reg);
81            let mut data = Clone::clone(&state.data);
82
83            // Perform instruction-specific behaviour.
84            ::machine_check::bitmask_switch!(instruction {
85                "00dd_00--_aabb" => { // add
86                    reg[d] = reg[a] + reg[b];
87                }
88                "00dd_01--_gggg" => { // read input
89                    reg[d] = input.gpio_read[g];
90                }
91                "00rr_1kkk_kkkk" => { // jump if bit 0 is set
92                    if reg[r] & Bitvector::<8>::new(1)
93                        == Bitvector::<8>::new(1) {
94                        pc = k;
95                    };
96                }
97                "01dd_kkkk_kkkk" => { // load immediate
98                    reg[d] = k;
99                }
100                "10dd_nnnn_nnnn" => { // load direct
101                    reg[d] = data[n];
102                }
103                "11ss_nnnn_nnnn" => { // store direct
104                    data[n] = reg[s];
105                }
106            });
107
108            // Return the state.
109            State { pc, reg, data }
110        }
111    }
112}
113
114use machine_check::{Bitvector, BitvectorArray};
115
116fn main() {
117    let toy_program = [
118        // (0) set r0 to zero
119        Bitvector::new(0b0100_0000_0000),
120        // (1) set r1 to one
121        Bitvector::new(0b0101_0000_0001),
122        // (2) set r2 to zero
123        Bitvector::new(0b0110_0000_0000),
124        // --- main loop ---
125        // (3) store r1 content to data location 0
126        Bitvector::new(0b1100_0000_0000),
127        // (4) store r2 content to data location 1
128        Bitvector::new(0b1100_0000_0001),
129        // (5) read input location 0 to r3
130        Bitvector::new(0b0011_0100_0000),
131        // (6) jump to (3) if r3 bit 0 is set
132        Bitvector::new(0b0011_1000_0011),
133        // (7) increment r2
134        Bitvector::new(0b0010_0000_1001),
135        // (8) store r2 content to data location 1
136        Bitvector::new(0b1110_0000_0001),
137        // (9) jump to (3)
138        Bitvector::new(0b0001_1000_0011),
139    ];
140
141    // load toy program to program memory, filling unused locations with 0
142    let mut progmem = BitvectorArray::new_filled(Bitvector::new(0));
143    for (index, instruction) in toy_program.into_iter().enumerate() {
144        progmem[Bitvector::new(index as u64)] = instruction;
145    }
146    let system = machine_module::System { progmem };
147    machine_check::run(system);
148}
simple_risc/simple_risc.rs

simple_risc/
simple_risc.rs
