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
16
17
18
19
20
21
22
23
24
25
26
27
28

default Order dec

$include <prelude.sail>

val "eq_anything" : forall ('a : Type). ('a, 'a) -> bool
overload operator == = {eq_anything}

register R: bool

function lin() -> (bits(1), bits(1)) = {
  if R then {
    (0b0, 0b1)
  } else {
    (0b1, 0b0)
  }
}

function f() -> (bits(1), bits(1)) = {
  if R then {
    (0b0, 0b1)
  } else {
    (0b1, 0b0)
  }
}

function prop() -> bool = {
  f() == lin()
}