blob: bb35c6f7e76c5d3cb84289fc8ce67d50f208a897 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
default Order dec
$include <prelude.sail>
$include "test/arch.sail"
/* Default memory model is as weak as possible, so this is not true */
$counterexample
function prop() -> bool = {
let _ = arch_load(0b00, 0b01);
let _ = arch_store(0b10, 0b00);
X(0b01) == X(0b10)
}
|
