include "ctrl.cat"
let data = [R]; dd-restrict; [DATA]; intrinsic; [W]
let addr = [R]; dd-restrict; [NDATA]; intrinsic; [M]
let sim = (same-instr & ((EXEC*SPEC) | (SPEC*EXEC))) \ id
let co-step =
let ww-loc = [W];po-loc;[W]
in
ww-loc\(ww-loc;ww-loc)
let dep = (iico_data|iico_ctrl|rf-reg-restrict|rfi|co-step)^-1
let diffw =(loc & (W * W)) \ id
let diff = ((rfe^-1;diffw;rf)|(rf^-1;diffw;rfe))
let bisim = bisimulation(dep,same-static\diff)\id
let equiv = (W*W) & bisim
let ctrl = ctrlequiv equiv
let AE = always-exec equiv
let DW = zyva equiv Dmins
let rf-mem = rf \ rf-reg
show rf-reg
show rf-mem
as rf
show co|fr
as ca