isla 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

default Order dec

$include <prelude.sail>

register R: bits(8)

function prop(u: bits(4)) -> bool = {
    R = [R with 3 .. 0 = 0xF];
    assert(R[3 .. 0] == 0xF);
    assert(R[0] == bitone);
    R = [R with 4 .. 1 = u];
    assert(R[0] == bitone);
    assert(R[3 .. 0] == u[2 .. 0] @ 0b1);
    true
}