зеркало из https://github.com/microsoft/ivy.git
1518 строки
60 KiB
XML
1518 строки
60 KiB
XML
#lang ivy1.7
|
|
################################################################################
|
|
|
|
isolate proc = {
|
|
type this
|
|
|
|
object impl = {
|
|
interpret proc->bv[2]
|
|
}
|
|
|
|
attribute test=impl
|
|
}
|
|
|
|
isolate mem_type = {
|
|
type this
|
|
|
|
object impl = {
|
|
interpret mem_type->bv[2]
|
|
}
|
|
|
|
attribute test=impl
|
|
}
|
|
|
|
#ISSUE0
|
|
type data_type = {0,1,2}
|
|
|
|
# isolate data_type = {
|
|
# type this
|
|
|
|
# object impl = {
|
|
# interpret data_type->bv[1]
|
|
# }
|
|
|
|
# attribute test=impl
|
|
# }
|
|
|
|
isolate addr_type = {
|
|
type this
|
|
|
|
object impl = {
|
|
interpret addr_type->bv[1]
|
|
}
|
|
|
|
attribute test=impl
|
|
|
|
}
|
|
|
|
isolate dcs_type = {
|
|
type this
|
|
|
|
object impl = {
|
|
interpret dcs_type->bv[1]
|
|
}
|
|
|
|
attribute test=impl
|
|
}
|
|
|
|
isolate lclock = {
|
|
type this
|
|
alias t = this
|
|
|
|
relation (X:t < Y:t)
|
|
action incr(inp:t) returns (out:t)
|
|
|
|
object spec = {
|
|
axiom [transitivity] X:t < Y & Y < Z -> X < Z
|
|
axiom [antisymmetry] ~(X:t < Y & Y < X)
|
|
axiom [totality] X:t < Y | X = Y | Y < X
|
|
|
|
after incr {
|
|
assume inp < out
|
|
}
|
|
}
|
|
|
|
object impl = {
|
|
interpret lclock->bv[10]
|
|
|
|
implement incr {
|
|
out := inp+1;
|
|
}
|
|
}
|
|
attribute test=impl
|
|
}
|
|
|
|
type op_type = {nop,write,read,rrsp}
|
|
|
|
type loc_type = {init_l,acc_l,afc_l,amcc_l,dcs_l}
|
|
type agt_type = {init_agt,arm_agt}
|
|
|
|
type ch_type = {llt,bulk}
|
|
|
|
module evs_type = {
|
|
individual p : proc
|
|
individual m : mem_type
|
|
individual a : addr_type
|
|
|
|
individual io : bool # device memory
|
|
|
|
individual dcs : mem_type
|
|
|
|
individual agt : agt_type
|
|
|
|
individual op : op_type
|
|
|
|
individual ch : ch_type
|
|
|
|
individual sub : bool
|
|
individual ro : bool
|
|
individual rspro : bool
|
|
individual post : bool
|
|
|
|
individual data : data_type
|
|
|
|
individual l : loc_type
|
|
|
|
individual serialized : bool
|
|
individual time : lclock
|
|
}
|
|
|
|
################################################################################
|
|
# Memory access reference model
|
|
|
|
object ref = {
|
|
|
|
instantiate evs(T:lclock) : evs_type
|
|
|
|
################################################################################
|
|
# current local time
|
|
|
|
individual lt : lclock
|
|
|
|
################################################################################
|
|
# current global time
|
|
|
|
individual gt : lclock
|
|
|
|
################################################################################
|
|
# global memory state
|
|
|
|
individual mem(M:mem_type,A:addr_type) : data_type
|
|
|
|
relation prevents(T0:lclock,T1:lclock)
|
|
relation pio_exception(T0:lclock,T1:lclock)
|
|
|
|
definition pio_exception(T0,T1) = evs(T0).io & evs(T1).io & ~evs(T0).post & ~evs(T1).post & (
|
|
evs(T1).op=read & evs(T0).op=rrsp | # PIO read response leading pio read
|
|
evs(T1).op=write & evs(T0).op=rrsp # PIO read response leading pio write
|
|
)
|
|
|
|
definition prevents(T0,T1) = evs(T0).op~=nop & ~evs(T0).serialized # older op not globally visible
|
|
& (T0 < T1)
|
|
& evs(T0).p = evs(T1).p # two opearations issued from same initiator (ARM or EP)
|
|
& evs(T0).agt = evs(T1).agt
|
|
& evs(T0).io = evs(T1).io # PIO vis-a-vis PIO and mem vis-a-vis mem (PIO not ordered vis-a-vis mem)
|
|
& ~pio_exception(T0,T1)
|
|
& (evs(T0).m=evs(T1).m & evs(T0).a=evs(T1).a | ~evs(T0).ro | ~evs(T1).ro) # same address or one operation is barrier
|
|
|
|
action create(p:proc,agt:agt_type,sub:bool,op:op_type,ro:bool,post:bool,m:mem_type,a:addr_type,io:bool,d:data_type,l:loc_type,ch:ch_type) = {
|
|
|
|
evs(lt).p := p;
|
|
evs(lt).agt := agt;
|
|
evs(lt).sub := sub;
|
|
evs(lt).op := op;
|
|
evs(lt).ro := ro;
|
|
evs(lt).rspro := true;
|
|
evs(lt).post := post;
|
|
|
|
evs(lt).m := m;
|
|
evs(lt).a := a;
|
|
evs(lt).io := io;
|
|
evs(lt).ch := ch;
|
|
evs(lt).data := d;
|
|
evs(lt).serialized := false;
|
|
evs(lt).time := 0;
|
|
|
|
evs(lt).l := l;
|
|
|
|
lt := lt.incr();
|
|
}
|
|
|
|
action perform(p:proc, lt:lclock) = {
|
|
var a : addr_type;
|
|
var d : data_type;
|
|
var m : mem_type;
|
|
|
|
# serialization must be appropriately ordered
|
|
|
|
assert ~prevents(T,lt);
|
|
|
|
# serialize at current global time
|
|
evs(lt).serialized := true;
|
|
|
|
if evs(lt).op = write {
|
|
evs(lt).time := gt;
|
|
};
|
|
|
|
# advance global time
|
|
if evs(lt).op = write {
|
|
gt := gt.incr();
|
|
};
|
|
|
|
# update the global memory state
|
|
|
|
a := evs(lt).a;
|
|
d := evs(lt).data;
|
|
m := evs(lt).m;
|
|
|
|
if evs(lt).op = write {
|
|
mem(m,a) := d;
|
|
};
|
|
|
|
evs(lt).l := init_l;
|
|
}
|
|
|
|
action perform_grd(lt:lclock) = {
|
|
var a : addr_type;
|
|
var m : mem_type;
|
|
|
|
# serialize at current global time
|
|
evs(lt).time := gt;
|
|
|
|
# serialization must be appropriately ordered
|
|
|
|
assert ~prevents(T,lt);
|
|
|
|
# advance global time
|
|
gt := gt.incr();
|
|
|
|
# update the global memory state
|
|
|
|
a := evs(lt).a;
|
|
m := evs(lt).m;
|
|
|
|
if evs(lt).op = read {
|
|
evs(lt).data := mem(m,a);
|
|
evs(lt).op := rrsp;
|
|
}
|
|
}
|
|
|
|
}
|
|
|
|
################################################################################
|
|
# Request buffers used by all agents
|
|
#
|
|
|
|
object isd = {
|
|
relation isd_wr0(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
relation isd_wr1(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
relation isd_rd0(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
relation isd_rd1(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
|
|
relation isd_rsp0(P:proc,M:mem_type,A:addr_type)
|
|
relation isd_rsp1(P:proc,M:mem_type,A:addr_type)
|
|
|
|
relation isd_wr(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
relation isd_rd(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
|
|
definition isd_wr(P:proc,M:mem_type,A:addr_type,T:lclock) = isd_wr0(P:proc,M:mem_type,A:addr_type,T:lclock) | isd_wr1(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
definition isd_rd(P:proc,M:mem_type,A:addr_type,T:lclock) = isd_rd0(P:proc,M:mem_type,A:addr_type,T:lclock) | isd_rd1(P:proc,M:mem_type,A:addr_type,T:lclock)
|
|
}
|
|
|
|
################################################################################
|
|
# arm
|
|
#
|
|
type ep_ph_type = {ep_nop_ph, ep_wr0_ph, ep_wr1_ph, ep_rd0_ph, ep_rd1_ph, ep_rsp0_ph, ep_rsp1_ph}
|
|
|
|
module arm_ref(p) = {
|
|
|
|
alias lclock_type = lclock
|
|
|
|
individual data(M:mem_type, A:addr_type) : data_type
|
|
|
|
action step(ph:ep_ph_type, a:addr_type,io_arg:bool, d:data_type,post:bool,ro:bool,m_arg:mem_type,ch:ch_type) = {
|
|
|
|
var agt : agt_type;
|
|
var sub : bool;
|
|
|
|
var ro_isd : bool;
|
|
var nro_isd : bool;
|
|
|
|
var ord : bool;
|
|
|
|
var io : bool;
|
|
var m : mem_type;
|
|
|
|
# make sure all uses of address 'a' agree on io attribute (address is either an io address or regular address)
|
|
# make sure all uses of address 'a' agree on m attribute (the amcc that routes to the address))
|
|
|
|
if some t:lclock_type. ref.evs(t).op~=nop & ~ref.evs(t).serialized & ref.evs(t).a=a {
|
|
io := ref.evs(t).io;
|
|
m := ref.evs(t).m;
|
|
} else {
|
|
io := io_arg;
|
|
m := m_arg;
|
|
};
|
|
|
|
if io {
|
|
ch := bulk;
|
|
} else {
|
|
ch := ch;
|
|
};
|
|
|
|
# ro request has been issued
|
|
# nro request has been issued
|
|
|
|
nro_isd := exists M,A,T. (isd.isd_wr(p,M,A,T) | isd.isd_rd(p,M,A,T)) & ref.evs(T).agt=arm_agt & ~ref.evs(T).ro;
|
|
ro_isd := exists M,A,T. (isd.isd_wr(p,M,A,T) | isd.isd_rd(p,M,A,T)) & ref.evs(T).agt=arm_agt & ref.evs(T).ro;
|
|
|
|
# from arm
|
|
agt := arm_agt;
|
|
|
|
# 1 don't issue ~ro request, barrier, if ro request issued
|
|
# 2 don't issue ro request if barrier instruction issued
|
|
# 3 don't issue barrier instruction if barrier instruction issued
|
|
|
|
if ph=ep_wr0_ph & ~post & ~(ro_isd & ~ro | nro_isd & ro | nro_isd & ~ro | ro & io) {
|
|
|
|
if forall T. ~isd.isd_wr0(p,m,a,T) & acc.wr0(m,a).cmd=nop {
|
|
isd.isd_wr0(p,m,a,ref.lt) := true;
|
|
|
|
acc.wr0(m,a).cmd := write;
|
|
acc.wr0(m,a).p := p;
|
|
acc.wr0(m,a).data := d;
|
|
|
|
sub := false;
|
|
|
|
call ref.create(p,agt,sub,write,ro,post,m,a,io,d,acc_l,ch);
|
|
|
|
data(m,a) := d;
|
|
}
|
|
} else if ph=ep_wr1_ph & ~post & ~(ro_isd & ~ro | nro_isd & ro | nro_isd & ~ro | ro & io) {
|
|
|
|
if forall T. ~isd.isd_wr1(p,m,a,T) & acc.wr1(m,a).cmd=nop {
|
|
isd.isd_wr1(p,m,a,ref.lt) := true;
|
|
|
|
acc.wr1(m,a).cmd := write;
|
|
acc.wr1(m,a).p := p;
|
|
acc.wr1(m,a).data := d;
|
|
|
|
sub := true;
|
|
|
|
call ref.create(p,agt,sub,write,ro,post,m,a,io,d,acc_l,ch);
|
|
|
|
data(m,a) := d;
|
|
}
|
|
} else if ph=ep_rd0_ph & ~post & ~(ro_isd & ~ro | nro_isd & ro | nro_isd & ~ro | ro & io) & acc.rd0(m,a).cmd=nop {
|
|
|
|
if forall T. ~isd.isd_rd0(p,m,a,T) {
|
|
isd.isd_rd0(p,m,a,ref.lt) := true;
|
|
isd.isd_rsp0(p,m,a) := false;
|
|
|
|
acc.rd0(m,a).cmd := read;
|
|
acc.rd0(m,a).p := p;
|
|
|
|
sub := false;
|
|
|
|
call ref.create(p,agt,sub,read,ro,post,m,a,io,d,acc_l,ch);
|
|
}
|
|
} else if ph=ep_rd1_ph & ~post & ~(ro_isd & ~ro | nro_isd & ro | nro_isd & ~ro | ro & io) & acc.rd1(m,a).cmd=nop {
|
|
|
|
if forall T. ~isd.isd_rd1(p,m,a,T) {
|
|
isd.isd_rd1(p,m,a,ref.lt) := true;
|
|
isd.isd_rsp1(p,m,a) := false;
|
|
|
|
acc.rd1(m,a).cmd := read;
|
|
acc.rd1(m,a).p := p;
|
|
|
|
sub := true;
|
|
|
|
call ref.create(p,agt,sub,read,ro,post,m,a,io,d,acc_l,ch);
|
|
}
|
|
}
|
|
}
|
|
|
|
action arm_recv(ph:ep_ph_type,m:mem_type,a:addr_type) = {
|
|
var ordrob : bool;
|
|
|
|
##ISSUE1 var a:addr_type;
|
|
|
|
if ph=ep_rsp0_ph & acc.rsp0(m,a).cmd=rrsp & acc.rsp0(m,a).p=p {
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).agt=arm_agt & ref.evs(t).l=acc_l {
|
|
|
|
ordrob := ref.evs(t).io & exists T. ref.evs(T).op=rrsp & ~ref.evs(t).serialized & ref.evs(T).p=p & ref.evs(T).agt=arm_agt & ref.evs(T).io & T < t;
|
|
|
|
if ~ordrob {
|
|
data(m,a) := acc.rsp0(m,a).data;
|
|
|
|
assert data(m,a) = ref.evs(t).data;
|
|
|
|
acc.rsp0(m,a).cmd := nop;
|
|
|
|
call ref.perform(p,t);
|
|
|
|
isd.isd_rsp0(p,m,a) := false;
|
|
isd.isd_rd0(p,m,a,t) := false;
|
|
}
|
|
}
|
|
} else if ph=ep_rsp1_ph & acc.rsp1(m,a).cmd=rrsp & acc.rsp1(m,a).p=p {
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).agt=arm_agt & ref.evs(t).l=acc_l {
|
|
|
|
ordrob := ref.evs(t).io & exists T. ref.evs(T).op=rrsp & ~ref.evs(t).serialized & ref.evs(T).p=p & ref.evs(T).agt=arm_agt & ref.evs(T).io & T < t;
|
|
|
|
if ~ordrob {
|
|
data(m,a) := acc.rsp1(m,a).data;
|
|
|
|
assert data(m,a) = ref.evs(t).data;
|
|
|
|
acc.rsp1(m,a).cmd := nop;
|
|
|
|
call ref.perform(p,t);
|
|
|
|
isd.isd_rsp1(p,m,a) := false;
|
|
isd.isd_rd1(p,m,a,t) := false;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
################################################################################
|
|
# acc
|
|
#
|
|
|
|
type acc_ph_type = {acc_nop_ph, acc_wr0_ph, acc_wr1_ph, acc_rd0_ph,acc_rd1_ph, acc_rsp0_ph, acc_rsp1_ph}
|
|
|
|
module cmd_type = {
|
|
individual cmd : op_type
|
|
individual data : data_type
|
|
individual p : proc
|
|
}
|
|
|
|
object acc = {
|
|
instantiate wr0(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate wr1(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate rd0(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate rd1(M:mem_type,A:addr_type) : cmd_type
|
|
|
|
instantiate rsp0(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate rsp1(M:mem_type,A:addr_type) : cmd_type
|
|
|
|
alias lclock_type = lclock
|
|
|
|
# issue write/read if ordering requirements met
|
|
|
|
action send(ph:acc_ph_type, m:mem_type,a:addr_type) = {
|
|
|
|
var ordser : bool;
|
|
var ordser0 : bool;
|
|
var ordser1 : bool;
|
|
var ordser2 : bool;
|
|
var ordser3 : bool;
|
|
var ordpip : bool;
|
|
var ordspec : bool;
|
|
|
|
var ordser_blk : bool;
|
|
var ordpip_blk : bool;
|
|
var ordspec_blk : bool;
|
|
|
|
var tt : lclock_type;
|
|
|
|
var p : proc;
|
|
|
|
if ph=acc_wr0_ph & wr0(m,a).cmd=write & afc.wr0(m,a).cmd=nop {
|
|
p := wr0(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_wr0(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
tt := t;
|
|
|
|
ordser0 := exists M,A,T. isd.isd_wr(p,M,A,T) & (T < t) & ~(M=m & A=a) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
ordser1 := exists M,A,T. isd.isd_rd(p,M,A,T) & (T < t) & ref.evs(T).agt=arm_agt & ref.evs(t).io;
|
|
ordser2 := exists T. isd.isd_wr(p,m,a,T) & (T < t) & ref.evs(T).agt=arm_agt & ~ref.evs(T).io & ~ref.evs(t).io;
|
|
|
|
ordser := ordser0 | ordser1 | ordser2;
|
|
|
|
ordpip := exists T. isd.isd_wr(p,m,a,T) & ref.evs(T).l=acc_l & (T < t) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
|
|
ordspec := exists T. isd.isd_rd(p,m,a,T) & T < t & ref.evs(T).agt=arm_agt & ~ref.evs(t).io;
|
|
|
|
if ~(ordser | ordpip | ordspec) {
|
|
|
|
afc.wr0(m,a).cmd := wr0(m,a).cmd;
|
|
afc.wr0(m,a).p := wr0(m,a).p;
|
|
afc.wr0(m,a).data := wr0(m,a).data;
|
|
|
|
ref.evs(t).l := afc_l;
|
|
|
|
wr0(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=acc_wr1_ph & wr1(m,a).cmd=write & afc.wr1(m,a).cmd=nop {
|
|
p := wr1(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_wr1(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
|
|
ordser0 := exists M,A,T. isd.isd_wr(p,M,A,T) & (T < t) & ~(M=m & A=a) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
ordser1 := exists M,A,T. isd.isd_rd(p,M,A,T) & (T < t) & ref.evs(T).agt=arm_agt & ref.evs(t).io;
|
|
ordser2 := exists T. isd.isd_wr(p,m,a,T) & (T < t) & ref.evs(T).agt=arm_agt & ~ref.evs(T).io & ~ref.evs(t).io;
|
|
|
|
ordser := ordser0 | ordser1 | ordser2;
|
|
|
|
ordpip := exists T. isd.isd_wr(p,m,a,T) & ref.evs(T).l=acc_l & (T < t) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
|
|
ordspec := exists T. isd.isd_rd(p,m,a,T) & T < t & ref.evs(T).agt=arm_agt & ~ref.evs(t).io;
|
|
|
|
if ~(ordser | ordpip | ordspec) {
|
|
|
|
afc.wr1(m,a).cmd := write;
|
|
afc.wr1(m,a).p := wr1(m,a).p;
|
|
afc.wr1(m,a).data := wr1(m,a).data;
|
|
|
|
ref.evs(t).l := afc_l;
|
|
|
|
wr1(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=acc_rd0_ph & rd0(m,a).cmd=read & afc.rd0(m,a).cmd=nop {
|
|
p := rd0(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
tt := t;
|
|
|
|
ordser0 := exists M,A,T. isd.isd_wr(p,M,A,T) & (T < t) & ~(M=m & A=a) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
ordser1 := exists M,A,T. isd.isd_rd(p,M,A,T) & (T < t) & ~(M=m & A=a) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
ordser2 := exists T. isd.isd_wr(p,m,a,T) & (T < t) & ref.evs(T).agt=arm_agt & ~ref.evs(T).io & ~ref.evs(t).io;
|
|
ordser3 := exists T. isd.isd_rd(p,m,a,T) & (T < t) & ref.evs(T).agt=arm_agt & ~ref.evs(T).io & ~ref.evs(t).io;
|
|
|
|
ordser := ordser0 | ordser1 | ordser2 | ordser3;
|
|
|
|
ordpip := exists T. (isd.isd_rd(p,m,a,T) | isd.isd_wr(p,m,a,T)) & ref.evs(T).l=acc_l & T < t & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
|
|
ordspec := false;
|
|
|
|
if ~(ordser | ordpip | ordspec) {
|
|
|
|
afc.rd0(m,a).cmd := read;
|
|
afc.rd0(m,a).p := rd0(m,a).p;
|
|
afc.rd0(m,a).data := rd0(m,a).data;
|
|
|
|
ref.evs(t).l := afc_l;
|
|
|
|
rd0(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=acc_rd1_ph & rd1(m,a).cmd=read & afc.rd1(m,a).cmd=nop {
|
|
p := rd1(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
tt := t;
|
|
|
|
ordser0 := exists M,A,T. isd.isd_wr(p,M,A,T) & (T < t) & ~(M=m & A=a) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
ordser1 := exists M,A,T. isd.isd_rd(p,M,A,T) & (T < t) & ~(M=m & A=a) & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
ordser2 := exists T. isd.isd_wr(p,m,a,T) & (T < t) & ref.evs(T).agt=arm_agt & ~ref.evs(T).io & ~ref.evs(t).io;
|
|
ordser3 := exists T. isd.isd_rd(p,m,a,T) & (T < t) & ref.evs(T).agt=arm_agt & ~ref.evs(T).io & ~ref.evs(t).io;
|
|
|
|
ordser := ordser0 | ordser1 | ordser2 | ordser3;
|
|
|
|
ordpip := exists T. (isd.isd_rd(p,m,a,T) | isd.isd_wr(p,m,a,T)) & ref.evs(T).l=acc_l & T < t & ref.evs(T).agt=arm_agt & ref.evs(T).io & ref.evs(t).io;
|
|
|
|
ordspec := false;
|
|
|
|
if ~(ordser | ordpip | ordspec) {
|
|
|
|
afc.rd1(m,a).cmd := read;
|
|
afc.rd1(m,a).p := rd1(m,a).p;
|
|
afc.rd1(m,a).data := rd1(m,a).data;
|
|
|
|
ref.evs(t).l := afc_l;
|
|
|
|
rd1(m,a).cmd := nop;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
# receive read response
|
|
|
|
action recv(ph:acc_ph_type, m:mem_type, a:addr_type) = {
|
|
var p : proc;
|
|
|
|
if ph=acc_rsp0_ph & rsp0(m,a).cmd=nop & afc.rsp0(m,a).cmd = rrsp {
|
|
|
|
p := afc.rsp0(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).op=rrsp & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=afc_l {
|
|
rsp0(m,a).cmd := rrsp;
|
|
rsp0(m,a).p := afc.rsp0(m,a).p;
|
|
rsp0(m,a).data := afc.rsp0(m,a).data;
|
|
|
|
ref.evs(t).l := acc_l;
|
|
|
|
afc.rsp0(m,a).cmd := nop;
|
|
}
|
|
} else if ph=acc_rsp1_ph & rsp1(m,a).cmd=nop & afc.rsp1(m,a).cmd = rrsp {
|
|
|
|
p := afc.rsp1(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).op=rrsp & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=afc_l {
|
|
rsp1(m,a).cmd := rrsp;
|
|
rsp1(m,a).p := afc.rsp1(m,a).p;
|
|
rsp1(m,a).data := afc.rsp1(m,a).data;
|
|
|
|
ref.evs(t).l := acc_l;
|
|
|
|
afc.rsp1(m,a).cmd := nop;
|
|
}
|
|
}
|
|
}
|
|
|
|
# issue read/write to AFC/AFC for non-determinstic address a
|
|
|
|
action step(p:proc, ph : acc_ph_type,m:mem_type,a:addr_type) = {
|
|
|
|
if ph=acc_rsp0_ph {
|
|
call arm(p).arm_recv(ep_rsp0_ph,m,a)
|
|
} else if ph=acc_rsp1_ph {
|
|
call arm(p).arm_recv(ep_rsp1_ph,m,a)
|
|
} else {
|
|
call send(ph,m,a)
|
|
}
|
|
}
|
|
|
|
}
|
|
|
|
################################################################################
|
|
# afc fabric
|
|
#
|
|
#
|
|
|
|
type ph_type = {acc_recv, mem_recv_wr0, mem_recv_wr1, mem_recv_rd0, mem_recv_rd1, mem_resp0, mem_resp1}
|
|
|
|
object afc = {
|
|
instantiate wr0(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate wr1(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate rd0(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate rd1(M:mem_type,A:addr_type) : cmd_type
|
|
|
|
instantiate rsp0(M:mem_type,A:addr_type) : cmd_type
|
|
instantiate rsp1(M:mem_type,A:addr_type) : cmd_type
|
|
|
|
alias lclock_type = lclock
|
|
|
|
action step(ph:ph_type,m:mem_type, a:addr_type) = {
|
|
var ordpip : bool;
|
|
|
|
var p : proc;
|
|
|
|
if ph=mem_recv_rd0 & rd0(m,a).cmd=read {
|
|
p := rd0(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
|
|
ordpip := exists T. (isd.isd_rd0(p,m,a,T) & rd0(m,a).cmd=read |
|
|
isd.isd_rd1(p,m,a,T) & rd1(m,a).cmd=read |
|
|
isd.isd_wr0(p,m,a,T) & wr0(m,a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(m,a).cmd=write) & (T<t) & ref.evs(T).ch=ref.evs(t).ch & ref.evs(T).agt=arm_agt;
|
|
|
|
if ~ordpip & amcc(m).rd0(a).cmd=nop {
|
|
call amcc(m).recv(amcc_rd0_ph,a,rd0(m,a).data,rd0(m,a).p);
|
|
|
|
ref.evs(t).l := amcc_l;
|
|
|
|
rd0(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=mem_recv_rd1 & rd1(m,a).cmd=read {
|
|
p := rd1(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
|
|
ordpip := exists T. (isd.isd_rd0(p,m,a,T) & rd0(m,a).cmd=read |
|
|
isd.isd_rd1(p,m,a,T) & rd1(m,a).cmd=read |
|
|
isd.isd_wr0(p,m,a,T) & wr0(m,a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(m,a).cmd=write) & (T<t) & ref.evs(T).ch=ref.evs(t).ch & ref.evs(T).agt=arm_agt;
|
|
|
|
if ~ordpip & amcc(m).rd1(a).cmd=nop {
|
|
call amcc(m).recv(amcc_rd1_ph,a,rd1(m,a).data,rd1(m,a).p);
|
|
|
|
ref.evs(t).l := amcc_l;
|
|
|
|
rd1(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=mem_recv_wr0 & wr0(m,a).cmd=write {
|
|
p := wr0(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_wr0(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
|
|
ordpip := exists T. (isd.isd_rd0(p,m,a,T) & rd0(m,a).cmd=read |
|
|
isd.isd_rd1(p,m,a,T) & rd1(m,a).cmd=read |
|
|
isd.isd_wr0(p,m,a,T) & wr0(m,a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(m,a).cmd=write) & (T<t) & ref.evs(T).ch=ref.evs(t).ch & ref.evs(T).agt=arm_agt;
|
|
|
|
if ~ordpip & amcc(m).wr0(a).cmd=nop {
|
|
call amcc(m).recv(amcc_wr0_ph,a,wr0(m,a).data,wr0(m,a).p);
|
|
|
|
ref.evs(t).l := amcc_l;
|
|
|
|
wr0(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=mem_recv_wr1 & wr1(m,a).cmd=write {
|
|
p := wr1(m,a).p;
|
|
|
|
if some t:lclock_type. isd.isd_wr1(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt {
|
|
|
|
ordpip := exists T. (isd.isd_rd0(p,m,a,T) & rd0(m,a).cmd=read |
|
|
isd.isd_rd1(p,m,a,T) & rd1(m,a).cmd=read |
|
|
isd.isd_wr0(p,m,a,T) & wr0(m,a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(m,a).cmd=write) & (T<t) & ref.evs(T).ch=ref.evs(t).ch & ref.evs(T).agt=arm_agt;
|
|
|
|
if ~ordpip & amcc(m).wr1(a).cmd=nop {
|
|
call amcc(m).recv(amcc_wr1_ph,a,wr1(m,a).data,wr1(m,a).p);
|
|
|
|
ref.evs(t).l := amcc_l;
|
|
|
|
wr1(m,a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=mem_resp0 {
|
|
call acc.recv(acc_rsp0_ph,m,a)
|
|
} else if ph=mem_resp1 {
|
|
call acc.recv(acc_rsp1_ph,m,a)
|
|
}
|
|
}
|
|
}
|
|
|
|
################################################################################
|
|
# AMCC
|
|
################################################################################
|
|
|
|
type amcc_ph_type = {amcc_rd0_ph,amcc_rd1_ph,amcc_wr0_ph,amcc_wr1_ph,amcc_rsp0_ph,amcc_rsp1_ph}
|
|
|
|
module amcc_ref(m) = {
|
|
instantiate wr0(A:addr_type) : cmd_type
|
|
instantiate wr1(A:addr_type) : cmd_type
|
|
instantiate rd0(A:addr_type) : cmd_type
|
|
instantiate rd1(A:addr_type) : cmd_type
|
|
|
|
instantiate rsp0(A:addr_type) : cmd_type
|
|
instantiate rsp1(A:addr_type) : cmd_type
|
|
|
|
# receive write/read from AFC
|
|
|
|
action recv(ph:amcc_ph_type,a:addr_type,data:data_type,p:proc) = {
|
|
if ph=amcc_rd0_ph {
|
|
rd0(a).cmd := read;
|
|
rd0(a).p := p;
|
|
} else if ph=amcc_rd1_ph {
|
|
rd1(a).cmd := read;
|
|
rd1(a).p := p;
|
|
} else if ph=amcc_wr0_ph {
|
|
wr0(a).cmd := write;
|
|
wr0(a).p := p;
|
|
wr0(a).data := data;
|
|
} else if ph=amcc_wr1_ph {
|
|
wr1(a).cmd := write;
|
|
wr1(a).p := p;
|
|
wr1(a).data := data;
|
|
}
|
|
}
|
|
|
|
alias lclock_type = lclock
|
|
|
|
action step(ph:amcc_ph_type, a:addr_type) = {
|
|
var ordpip : bool;
|
|
var ordpip_ro : bool;
|
|
var ordpip_nro : bool;
|
|
|
|
var p : proc;
|
|
|
|
var tt : lclock;
|
|
|
|
if ph=amcc_rd0_ph & rd0(a).cmd=read {
|
|
|
|
p := rd0(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=amcc_l { # originates from ARM Table 61
|
|
|
|
ordpip_nro := ~ref.evs(t).ro & exists M,A,T. (isd.isd_wr0(p,M,A,T) & wr0(A).cmd=write |
|
|
isd.isd_wr1(p,M,A,T) & wr1(A).cmd=write |
|
|
isd.isd_rd0(p,M,A,T) & rd0(A).cmd=read |
|
|
isd.isd_rd1(p,M,A,T) & rd1(A).cmd=read) & ~ref.evs(T).ro & T < t & ref.evs(T).agt=arm_agt & ref.evs(T).m=m & ref.evs(T).l=amcc_l;
|
|
ordpip_ro := false;
|
|
|
|
ordpip := ordpip_ro | ordpip_nro;
|
|
|
|
if ~ordpip & dcs(m).rd0(a).cmd=nop {
|
|
dcs(m).rd0(a).cmd := read;
|
|
dcs(m).rd0(a).p := rd0(a).p;
|
|
|
|
ref.evs(t).l := dcs_l;
|
|
|
|
rd0(a).cmd := nop;
|
|
}
|
|
};
|
|
|
|
} else if ph=amcc_rd1_ph & rd1(a).cmd=read {
|
|
|
|
p := rd1(a).p;
|
|
|
|
ordpip_nro := true;
|
|
ordpip_ro := true;
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=amcc_l { # originates from ARM Table 61
|
|
ordpip_nro := ~ref.evs(t).ro & exists M,A,T. (isd.isd_wr0(p,M,A,T) & wr0(A).cmd=write |
|
|
isd.isd_wr1(p,M,A,T) & wr1(A).cmd=write |
|
|
isd.isd_rd0(p,M,A,T) & rd0(A).cmd=read |
|
|
isd.isd_rd1(p,M,A,T) & rd1(A).cmd=read) & ~ref.evs(T).ro & T < t & ref.evs(T).agt=arm_agt & ref.evs(T).m=m & ref.evs(T).l=amcc_l;
|
|
ordpip_ro := false;
|
|
|
|
ordpip := ordpip_ro | ordpip_nro;
|
|
|
|
if ~ordpip & dcs(m).rd1(a).cmd=nop {
|
|
dcs(m).rd1(a).cmd := read;
|
|
dcs(m).rd1(a).p := rd1(a).p;
|
|
|
|
ref.evs(t).l := dcs_l;
|
|
|
|
rd1(a).cmd := nop;
|
|
}
|
|
};
|
|
|
|
} else if ph=amcc_wr0_ph & wr0(a).cmd=write {
|
|
p := wr0(a).p;
|
|
|
|
ordpip_nro := true;
|
|
ordpip_ro := true;
|
|
|
|
if some t:lclock_type. isd.isd_wr0(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=amcc_l { # originates from ARM Table 61
|
|
|
|
tt := t;
|
|
|
|
ordpip_nro := ~ref.evs(t).ro & exists M,A,T. (isd.isd_wr0(p,M,A,T) & wr0(A).cmd=write |
|
|
isd.isd_wr1(p,M,A,T) & wr1(A).cmd=write |
|
|
isd.isd_rd0(p,M,A,T) & rd0(A).cmd=read |
|
|
isd.isd_rd1(p,M,A,T) & rd1(A).cmd=read) & ~ref.evs(T).ro & T < t & ref.evs(T).agt=arm_agt & ref.evs(T).m=m & ref.evs(T).l=amcc_l;
|
|
ordpip_ro := false;
|
|
};
|
|
|
|
ordpip := ordpip_ro | ordpip_nro;
|
|
|
|
if ~ordpip & dcs(m).wr0(a).cmd=nop {
|
|
dcs(m).wr0(a).cmd := write;
|
|
dcs(m).wr0(a).p := wr0(a).p;
|
|
dcs(m).wr0(a).data := wr0(a).data;
|
|
|
|
ref.evs(tt).l := dcs_l;
|
|
|
|
wr0(a).cmd := nop;
|
|
}
|
|
} else if ph=amcc_wr1_ph & wr1(a).cmd=write {
|
|
p := wr1(a).p;
|
|
|
|
ordpip_nro := true;
|
|
ordpip_ro := true;
|
|
|
|
if some t:lclock_type. isd.isd_wr1(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=amcc_l { # originates from ARM Table 61
|
|
|
|
tt := t;
|
|
|
|
ordpip_nro := ~ref.evs(t).ro & exists M,A,T. (isd.isd_wr0(p,M,A,T) & wr0(A).cmd=write |
|
|
isd.isd_wr1(p,M,A,T) & wr1(A).cmd=write |
|
|
isd.isd_rd0(p,M,A,T) & rd0(A).cmd=read |
|
|
isd.isd_rd1(p,M,A,T) & rd1(A).cmd=read) & ~ref.evs(T).ro & T < t & ref.evs(T).agt=arm_agt & ref.evs(T).m=m & ref.evs(T).l=amcc_l;
|
|
ordpip_ro := false;
|
|
};
|
|
|
|
ordpip := ordpip_ro | ordpip_nro;
|
|
|
|
if ~ordpip & dcs(m).wr1(a).cmd=nop {
|
|
|
|
dcs(m).wr1(a).cmd := write;
|
|
dcs(m).wr1(a).p := wr1(a).p;
|
|
dcs(m).wr1(a).data := wr1(a).data;
|
|
|
|
ref.evs(tt).l := dcs_l;
|
|
|
|
wr1(a).cmd := nop;
|
|
}
|
|
} else if ph=amcc_rsp0_ph & rsp0(a).cmd = rrsp {
|
|
|
|
p := rsp0(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).op=rrsp & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=amcc_l & ref.evs(t).m=m {
|
|
if afc.rsp0(m,a).cmd=nop {
|
|
|
|
afc.rsp0(m,a).cmd := rsp0(a).cmd;
|
|
afc.rsp0(m,a).p := rsp0(a).p;
|
|
afc.rsp0(m,a).data := rsp0(a).data;
|
|
|
|
ref.evs(t).l := afc_l;
|
|
|
|
rsp0(a).cmd := nop;
|
|
}
|
|
}
|
|
} else if ph=amcc_rsp1_ph & rsp1(a).cmd = rrsp {
|
|
|
|
p := rsp1(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).op=rrsp & ~ref.evs(t).serialized & ref.evs(t).agt=arm_agt & ref.evs(t).l=amcc_l & ref.evs(t).m=m {
|
|
if afc.rsp1(m,a).cmd=nop {
|
|
|
|
afc.rsp1(m,a).cmd := rsp1(a).cmd;
|
|
afc.rsp1(m,a).p := rsp1(a).p;
|
|
afc.rsp1(m,a).data := rsp1(a).data;
|
|
|
|
ref.evs(t).l := afc_l;
|
|
|
|
rsp1(a).cmd := nop;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
################################################################################
|
|
# DCS+DRAM
|
|
#
|
|
|
|
type dram_ph_type = {dram_rd0_ph,dram_rd1_ph,dram_wr0_ph,dram_wr1_ph}
|
|
|
|
module dcs_ref(m) = {
|
|
instantiate wr0(A:addr_type) : cmd_type
|
|
instantiate wr1(A:addr_type) : cmd_type
|
|
instantiate rd0(A:addr_type) : cmd_type
|
|
instantiate rd1(A:addr_type) : cmd_type
|
|
|
|
individual data(A:addr_type) : data_type
|
|
|
|
alias lclock_type = lclock
|
|
|
|
action dcs_step(ph:dram_ph_type,a:addr_type) = {
|
|
|
|
var ordpip : bool;
|
|
|
|
var p : proc;
|
|
|
|
if ph=dram_rd0_ph & rd0(a).cmd = read {
|
|
p := rd0(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd0(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).l=dcs_l & ref.evs(t).m=m {
|
|
|
|
ordpip := exists T. (isd.isd_wr0(p,m,a,T) & wr0(a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(a).cmd=write |
|
|
isd.isd_rd0(p,m,a,T) & rd0(a).cmd=read & ref.evs(T).io & ref.evs(t).io |
|
|
isd.isd_rd1(p,m,a,T) & rd1(a).cmd=read & ref.evs(T).io & ref.evs(t).io) & T < t & ref.evs(T).m=m & ref.evs(T).l=dcs_l;
|
|
|
|
if ~ordpip & amcc(m).rsp0(a).cmd=nop {
|
|
amcc(m).rsp0(a).cmd := rrsp;
|
|
amcc(m).rsp0(a).p := rd0(a).p;
|
|
amcc(m).rsp0(a).data := data(a);
|
|
|
|
ref.evs(t).l := amcc_l;
|
|
|
|
rd0(a).cmd := nop;
|
|
|
|
isd.isd_rsp0(p,m,a) := true;
|
|
|
|
assert data(a) = ref.mem(m,a);
|
|
|
|
call ref.perform_grd(t);
|
|
}
|
|
}
|
|
} else if ph=dram_rd1_ph & rd1(a).cmd = read {
|
|
p := rd1(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_rd1(p,m,a,t) & ref.evs(t).op=read & ~ref.evs(t).serialized & ref.evs(t).l=dcs_l & ref.evs(t).m=m {
|
|
|
|
ordpip := exists T. (isd.isd_wr0(p,m,a,T) & wr0(a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(a).cmd=write |
|
|
isd.isd_rd0(p,m,a,T) & rd0(a).cmd=read & ref.evs(T).io & ref.evs(t).io |
|
|
isd.isd_rd1(p,m,a,T) & rd1(a).cmd=read & ref.evs(T).io & ref.evs(t).io) & T < t & ref.evs(T).m=m & ref.evs(T).l=dcs_l;
|
|
|
|
if rd1(a).cmd=read & ~ordpip & amcc(m).rsp1(a).cmd=nop {
|
|
amcc(m).rsp1(a).cmd := rrsp;
|
|
amcc(m).rsp1(a).p := rd1(a).p;
|
|
amcc(m).rsp1(a).data := data(a);
|
|
|
|
ref.evs(t).l := amcc_l;
|
|
|
|
rd1(a).cmd := nop;
|
|
|
|
isd.isd_rsp1(p,m,a) := true;
|
|
|
|
assert data(a) = ref.mem(m,a);
|
|
|
|
assert ~ref.prevents(T,t);
|
|
|
|
call ref.perform_grd(t);
|
|
}
|
|
}
|
|
} else if ph=dram_wr0_ph & wr0(a).cmd = write {
|
|
p := wr0(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_wr0(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).l=dcs_l & ref.evs(t).m=m {
|
|
|
|
ordpip := exists T. (isd.isd_wr0(p,m,a,T) & wr0(a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(a).cmd=write |
|
|
isd.isd_rd0(p,m,a,T) & rd0(a).cmd=read & ref.evs(T).io & ref.evs(t).io |
|
|
isd.isd_rd1(p,m,a,T) & rd1(a).cmd=read & ref.evs(T).io & ref.evs(t).io) & T < t & ref.evs(T).m=m & ref.evs(T).l=dcs_l;
|
|
|
|
if wr0(a).cmd=write & ~ordpip {
|
|
data(a) := wr0(a).data;
|
|
|
|
wr0(a).cmd := nop;
|
|
|
|
call ref.perform(p,t);
|
|
|
|
isd.isd_wr0(p,m,a,t) := false;
|
|
}
|
|
}
|
|
} else if ph=dram_wr1_ph & wr1(a).cmd = write {
|
|
p := wr1(a).p;
|
|
|
|
if some t:lclock_type. isd.isd_wr1(p,m,a,t) & ref.evs(t).op=write & ~ref.evs(t).serialized & ref.evs(t).l=dcs_l & ref.evs(t).m=m {
|
|
|
|
ordpip := exists T. (isd.isd_wr0(p,m,a,T) & wr0(a).cmd=write |
|
|
isd.isd_wr1(p,m,a,T) & wr1(a).cmd=write |
|
|
isd.isd_rd0(p,m,a,T) & rd0(a).cmd=read & ref.evs(T).io & ref.evs(t).io |
|
|
isd.isd_rd1(p,m,a,T) & rd1(a).cmd=read & ref.evs(T).io & ref.evs(t).io) & T < t & ref.evs(T).m=m & ref.evs(T).l=dcs_l;
|
|
|
|
if wr1(a).cmd=write & ~ordpip {
|
|
data(a) := wr1(a).data;
|
|
|
|
wr1(a).cmd := nop;
|
|
|
|
call ref.perform(p,t);
|
|
|
|
isd.isd_wr1(p,m,a,t) := false;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
################################################################################
|
|
# initialize the state to nothing outstanding and the memory state of the ref
|
|
# model is the same as the state of the dcs memory
|
|
#
|
|
|
|
after init {
|
|
isd.isd_wr0(P,M,A,T) := false;
|
|
isd.isd_wr1(P,M,A,T) := false;
|
|
isd.isd_rd0(P,M,A,T) := false;
|
|
isd.isd_rd1(P,M,A,T) := false;
|
|
|
|
isd.isd_rsp0(P,M,A) := false;
|
|
isd.isd_rsp1(P,M,A) := false;
|
|
|
|
acc.wr0(M,A).cmd := nop;
|
|
acc.wr1(M,A).cmd := nop;
|
|
acc.rd0(M,A).cmd := nop;
|
|
acc.rd1(M,A).cmd := nop;
|
|
acc.rsp0(M,A).cmd := nop;
|
|
acc.rsp1(M,A).cmd := nop;
|
|
|
|
afc.wr0(M,A).cmd := nop;
|
|
afc.wr1(M,A).cmd := nop;
|
|
afc.rd0(M,A).cmd := nop;
|
|
afc.rd1(M,A).cmd := nop;
|
|
|
|
amcc(M).wr0(A).cmd := nop;
|
|
amcc(M).wr1(A).cmd := nop;
|
|
amcc(M).rd0(A).cmd := nop;
|
|
amcc(M).rd1(A).cmd := nop;
|
|
amcc(M).rsp0(A).cmd := nop;
|
|
amcc(M).rsp1(A).cmd := nop;
|
|
|
|
dcs(M).wr0(A).cmd := nop;
|
|
dcs(M).wr1(A).cmd := nop;
|
|
dcs(M).rd0(A).cmd := nop;
|
|
dcs(M).rd1(A).cmd := nop;
|
|
|
|
ref.lt := 0;
|
|
ref.gt := 0;
|
|
|
|
# initialize memory
|
|
|
|
dcs(M).data(A) := 0;
|
|
ref.mem(M,A) := 0;
|
|
|
|
ref.evs(T).op := nop;
|
|
ref.evs(T).serialized := true;
|
|
ref.evs(T).l := init_l;
|
|
ref.evs(T).agt := init_agt;
|
|
ref.evs(T).time := 0;
|
|
|
|
afc.rsp0(M,A).cmd := nop;
|
|
afc.rsp1(M,A).cmd := nop;
|
|
}
|
|
|
|
# instantiate
|
|
|
|
instantiate arm(P:proc) : arm_ref(P)
|
|
|
|
instantiate amcc(M:mem_type) : amcc_ref(M)
|
|
instantiate dcs(M:mem_type) : dcs_ref(M)
|
|
|
|
# "zero out" cmd that do not occur (otherwise assume/guarantee might start with these cmd)
|
|
#
|
|
# - an alternative is to have more cmd types
|
|
|
|
###
|
|
|
|
conjecture (forall T. ~isd.isd_wr0(P,M,A,T)) -> ~(acc.wr0(M,A).cmd=write & acc.wr0(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_wr0(P,M,A,T)) -> ~(afc.wr0(M,A).cmd=write & afc.wr0(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_wr0(P,M,A,T)) -> ~(amcc(M).wr0(A).cmd=write & amcc(M).wr0(A).p=P)
|
|
conjecture (forall T. ~isd.isd_wr0(P,M,A,T)) -> ~(dcs(M).wr0(A).cmd=write & dcs(M).wr0(A).p=P)
|
|
|
|
conjecture (forall T. ~isd.isd_wr1(P,M,A,T)) -> ~(acc.wr1(M,A).cmd=write & acc.wr1(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_wr1(P,M,A,T)) -> ~(afc.wr1(M,A).cmd=write & afc.wr1(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_wr1(P,M,A,T)) -> ~(amcc(M).wr1(A).cmd=write & amcc(M).wr1(A).p=P)
|
|
conjecture (forall T. ~isd.isd_wr1(P,M,A,T)) -> ~(dcs(M).wr1(A).cmd=write & dcs(M).wr1(A).p=P)
|
|
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(acc.rd0(M,A).cmd=read & acc.rd0(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(afc.rd0(M,A).cmd=read & afc.rd0(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(amcc(M).rd0(A).cmd=read & amcc(M).rd0(A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(dcs(M).rd0(A).cmd=read & dcs(M).rd0(A).p=P)
|
|
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(acc.rsp0(M,A).cmd=rrsp & acc.rsp0(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(afc.rsp0(M,A).cmd=rrsp & afc.rsp0(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd0(P,M,A,T)) -> ~(amcc(M).rsp0(A).cmd=rrsp & amcc(M).rsp0(A).p=P)
|
|
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(acc.rd1(M,A).cmd=read & acc.rd1(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(afc.rd1(M,A).cmd=read & afc.rd1(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(amcc(M).rd1(A).cmd=read & amcc(M).rd1(A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(dcs(M).rd1(A).cmd=read & dcs(M).rd1(A).p=P)
|
|
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(acc.rsp1(M,A).cmd=rrsp & acc.rsp1(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(afc.rsp1(M,A).cmd=rrsp & afc.rsp1(M,A).p=P)
|
|
conjecture (forall T. ~isd.isd_rd1(P,M,A,T)) -> ~(amcc(M).rsp1(A).cmd=rrsp & amcc(M).rsp1(A).p=P)
|
|
|
|
##
|
|
|
|
conjecture acc.rsp0(M,A).cmd~=write
|
|
conjecture acc.rsp0(M,A).cmd~=read
|
|
|
|
conjecture acc.rsp1(M,A).cmd~=write
|
|
conjecture acc.rsp1(M,A).cmd~=read
|
|
|
|
conjecture acc.wr0(M,A).cmd~=rrsp
|
|
conjecture acc.wr0(M,A).cmd~=read
|
|
|
|
conjecture acc.wr1(M,A).cmd~=rrsp
|
|
conjecture acc.wr1(M,A).cmd~=read
|
|
|
|
conjecture acc.rd0(M,A).cmd~=rrsp
|
|
conjecture acc.rd0(M,A).cmd~=write
|
|
|
|
conjecture acc.rd1(M,A).cmd~=rrsp
|
|
conjecture acc.rd1(M,A).cmd~=write
|
|
|
|
conjecture afc.rsp0(M,A).cmd~=write
|
|
conjecture afc.rsp0(M,A).cmd~=read
|
|
|
|
conjecture afc.rsp1(M,A).cmd~=write
|
|
conjecture afc.rsp1(M,A).cmd~=read
|
|
|
|
conjecture afc.wr0(M,A).cmd~=rrsp
|
|
conjecture afc.wr0(M,A).cmd~=read
|
|
|
|
conjecture afc.wr1(M,A).cmd~=rrsp
|
|
conjecture afc.wr1(M,A).cmd~=read
|
|
|
|
conjecture afc.rd0(M,A).cmd~=rrsp
|
|
conjecture afc.rd0(M,A).cmd~=write
|
|
|
|
conjecture afc.rd1(M,A).cmd~=rrsp
|
|
conjecture afc.rd1(M,A).cmd~=write
|
|
|
|
conjecture amcc(M).wr0(A).cmd~=read
|
|
conjecture amcc(M).wr0(A).cmd~=rrsp
|
|
|
|
conjecture amcc(M).wr1(A).cmd~=read
|
|
conjecture amcc(M).wr1(A).cmd~=rrsp
|
|
|
|
conjecture amcc(M).rd0(A).cmd~=write
|
|
conjecture amcc(M).rd1(A).cmd~=write
|
|
|
|
conjecture amcc(M).rd0(A).cmd~=rrsp
|
|
conjecture amcc(M).rd1(A).cmd~=rrsp
|
|
|
|
conjecture amcc(M).rsp0(A).cmd~=read
|
|
conjecture amcc(M).rsp0(A).cmd~=write
|
|
|
|
conjecture amcc(M).rsp1(A).cmd~=read
|
|
conjecture amcc(M).rsp1(A).cmd~=write
|
|
|
|
conjecture dcs(M).wr0(A).cmd~=read
|
|
conjecture dcs(M).wr0(A).cmd~=rrsp
|
|
conjecture dcs(M).wr1(A).cmd~=read
|
|
conjecture dcs(M).wr1(A).cmd~=rrsp
|
|
|
|
conjecture dcs(M).rd0(A).cmd~=write
|
|
conjecture dcs(M).rd0(A).cmd~=rrsp
|
|
conjecture dcs(M).rd1(A).cmd~=write
|
|
conjecture dcs(M).rd1(A).cmd~=rrsp
|
|
|
|
# various pending request invariants (required to keep assume/guarantee on right path)
|
|
|
|
conjecture (isd.isd_wr0(P,M,A,T1) & isd.isd_wr0(P,M,A,T2)) -> T1=T2
|
|
conjecture (isd.isd_wr1(P,M,A,T1) & isd.isd_wr1(P,M,A,T2)) -> T1=T2
|
|
|
|
conjecture (isd.isd_rd0(P,M,A,T1) & isd.isd_rd0(P,M,A,T2)) -> T1=T2
|
|
conjecture (isd.isd_rd1(P,M,A,T1) & isd.isd_rd1(P,M,A,T2)) -> T1=T2
|
|
|
|
####
|
|
|
|
conjecture (isd.isd_wr0(P0,M0,A0,T0) & isd.isd_wr1(P1,M1,A1,T1)) -> (T0~=T1)
|
|
conjecture (isd.isd_wr0(P0,M0,A0,T0) & isd.isd_rd0(P1,M1,A1,T1)) -> (T0~=T1)
|
|
conjecture (isd.isd_wr0(P0,M0,A0,T0) & isd.isd_rd1(P1,M1,A1,T1)) -> (T0~=T1)
|
|
conjecture (isd.isd_wr1(P0,M0,A0,T0) & isd.isd_rd0(P1,M1,A1,T1)) -> (T0~=T1)
|
|
conjecture (isd.isd_wr1(P0,M0,A0,T0) & isd.isd_rd1(P1,M1,A1,T1)) -> (T0~=T1)
|
|
conjecture (isd.isd_rd0(P0,M0,A0,T0) & isd.isd_rd1(P1,M1,A1,T1)) -> (T0~=T1)
|
|
|
|
###
|
|
|
|
### there's a 1-to-1 relationship between ref(T) and pnd
|
|
|
|
conjecture (~ref.evs(T).serialized & (ref.evs(T).op=read | ref.evs(T).op=rrsp) & ref.evs(T).m=M & ref.evs(T).a=A & ref.evs(T).p=P & ~ref.evs(T).sub) -> isd.isd_rd0(P,M,A,T)
|
|
conjecture (~ref.evs(T).serialized & (ref.evs(T).op=read | ref.evs(T).op=rrsp) & ref.evs(T).m=M & ref.evs(T).a=A & ref.evs(T).p=P & ref.evs(T).sub) -> isd.isd_rd1(P,M,A,T)
|
|
|
|
conjecture (~ref.evs(T).serialized & ref.evs(T).op=write & ref.evs(T).m=M & ref.evs(T).a=A & ref.evs(T).p=P & ~ref.evs(T).sub) -> isd.isd_wr0(P,M,A,T)
|
|
conjecture (~ref.evs(T).serialized & ref.evs(T).op=write & ref.evs(T).m=M & ref.evs(T).a=A & ref.evs(T).p=P & ref.evs(T).sub) -> isd.isd_wr1(P,M,A,T)
|
|
|
|
conjecture ref.evs(T).serialized
|
|
->
|
|
~(
|
|
isd.isd_wr0(P,M,A,T) | isd.isd_wr1(P,M,A,T) | isd.isd_rd0(P,M,A,T) & ~isd.isd_rsp0(P,M,A) | isd.isd_rd1(P,M,A,T) & ~isd.isd_rsp1(P,M,A)
|
|
)
|
|
|
|
### Table 23
|
|
|
|
### same A
|
|
|
|
conjecture (isd.isd_wr0(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_rd0(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.rd0(M,A).cmd=read & acc.rd0(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
conjecture (isd.isd_wr0(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_rd1(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.rd1(M,A).cmd=read & acc.rd1(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
conjecture (isd.isd_wr0(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_wr1(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.wr1(M,A).cmd=write & acc.wr1(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
|
|
conjecture (isd.isd_wr1(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_rd0(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.rd0(M,A).cmd=read & acc.rd0(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
conjecture (isd.isd_wr1(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_rd1(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.rd1(M,A).cmd=read & acc.rd1(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
conjecture (isd.isd_wr1(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_wr0(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.wr0(M,A).cmd=write & acc.wr0(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
|
|
conjecture (isd.isd_rd0(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_rd1(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.rd1(M,A).cmd=read & acc.rd1(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
conjecture (isd.isd_rd0(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_wr0(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.wr0(M,A).cmd=write & acc.wr0(M,A).p=P)
|
|
conjecture (isd.isd_rd0(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_wr1(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.wr1(M,A).cmd=write & acc.wr1(M,A).p=P)
|
|
|
|
conjecture (isd.isd_rd1(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_rd0(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.rd0(M,A).cmd=read & acc.rd0(M,A).p=P | ref.evs(T1).io & ref.evs(T0).io | ref.evs(T1).io & ~ref.evs(T0).io | ~ref.evs(T1).io & ref.evs(T0).io)
|
|
conjecture (isd.isd_rd1(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_wr0(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.wr0(M,A).cmd=write & acc.wr0(M,A).p=P)
|
|
conjecture (isd.isd_rd1(P,M,A,T0) & ref.evs(T0).agt=arm_agt & isd.isd_wr1(P,M,A,T1) & ref.evs(T1).agt=arm_agt & T0 < T1) -> (acc.wr1(M,A).cmd=write & acc.wr1(M,A).p=P)
|
|
|
|
###
|
|
|
|
conjecture (isd.isd_rd0(P,M,A,T) | isd.isd_rd1(P,M,A,T)) -> ~ref.evs(T).post
|
|
|
|
conjecture (ref.evs(T0).op~=nop & ~ref.evs(T0).serialized & ref.evs(T1).op~=nop & ~ref.evs(T1).serialized & ref.evs(T0).a=ref.evs(T1).a) -> ref.evs(T0).io=ref.evs(T1).io
|
|
|
|
|
|
conjecture (ref.evs(T).l = acc_l | ref.evs(T).l = afc_l) -> ref.evs(T).agt=arm_agt
|
|
|
|
###
|
|
|
|
###
|
|
|
|
conjecture ref.mem(M,A) = dcs(M).data(A)
|
|
|
|
###
|
|
|
|
conjecture ~(T<ref.lt) -> (ref.evs(T).op=nop & ref.evs(T).serialized)
|
|
|
|
conjecture (isd.isd_rd0(P,M,A,T) & isd.isd_rsp0(P,M,A) | isd.isd_rd1(P,M,A,T) & isd.isd_rsp1(P,M,A)) <-> (ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A & T<ref.lt)
|
|
|
|
conjecture isd.isd_wr(P,M,A,T) <-> (ref.evs(T).op=write & ~ref.evs(T).serialized & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A & T<ref.lt)
|
|
|
|
###
|
|
|
|
conjecture (ref.evs(T0).op~=nop & ~ref.evs(T0).serialized & ref.evs(T0).agt=arm_agt & ref.evs(T0).p=P & ref.evs(T0).ro)
|
|
->
|
|
~(ref.evs(T1).op~=nop & ~ref.evs(T1).serialized & ref.evs(T1).agt=arm_agt & ref.evs(T1).p=P & ~ref.evs(T1).ro)
|
|
|
|
conjecture (ref.evs(T0).op~=nop & ~ref.evs(T0).serialized & ref.evs(T0).agt=arm_agt & ref.evs(T0).p=P & ~ref.evs(T0).ro & ~ref.evs(T0).io)
|
|
->
|
|
~(ref.evs(T1).op~=nop & ~ref.evs(T1).serialized & ref.evs(T1).agt=arm_agt & ref.evs(T1).p=P & ~ref.evs(T1).ro & ~ref.evs(T1).io & T0~=T1)
|
|
|
|
###
|
|
|
|
conjecture (isd.isd_rd0(P,M,A,T) & ~isd.isd_rsp0(P,M,A) | isd.isd_rd1(P,M,A,T) & ~isd.isd_rsp1(P,M,A))
|
|
<->
|
|
(ref.evs(T).op=read & ~ref.evs(T).serialized & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A)
|
|
|
|
conjecture (isd.isd_rd0(P,M,A,T) & isd.isd_rsp0(P,M,A) | isd.isd_rd1(P,M,A,T) & isd.isd_rsp1(P,M,A))
|
|
<->
|
|
(ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A)
|
|
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ref.evs(T).io) -> ~ref.evs(T).ro
|
|
conjecture (ref.evs(T).op=write & ~ref.evs(T).serialized & ref.evs(T).io) -> ~ref.evs(T).ro
|
|
conjecture (ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ref.evs(T).io) -> ~ref.evs(T).ro
|
|
conjecture (ref.evs(T).op~=nop & ~ref.evs(T).serialized & ref.evs(T).agt=arm_agt) -> ~ref.evs(T).post # write modeled where ARM post has been turned into non-post
|
|
|
|
#
|
|
|
|
conjecture (
|
|
ref.evs(T0).op=rrsp & ~ref.evs(T0).serialized & (ref.evs(T1).op=read & ~ref.evs(T1).serialized | ref.evs(T1).op=write & ~ref.evs(T1).serialized & ~ref.evs(T1).post) & ref.evs(T0).p=ref.evs(T1).p & ref.evs(T0).agt=ref.evs(T1).agt & ~ref.evs(T0).ro & ~ref.evs(T1).ro &
|
|
ref.evs(T0).io=ref.evs(T1).io &
|
|
(ref.evs(T0).agt=arm_agt -> ref.evs(T0).io)
|
|
)
|
|
-> T0 < T1
|
|
|
|
#
|
|
|
|
conjecture (ref.evs(T0).op~=nop & ~ref.evs(T0).serialized & ref.evs(T1).op~=nop & ~ref.evs(T1).serialized & ref.evs(T0).p=ref.evs(T1).p & ref.evs(T0).agt=arm_agt & ref.evs(T1).agt=arm_agt & ref.evs(T0).io & ref.evs(T1).io & ref.evs(T0).a~=ref.evs(T1).a & T0<T1)
|
|
->
|
|
(
|
|
((ref.evs(T1).op=write & ~ref.evs(T1).sub) -> (acc.wr0(ref.evs(T1).m,ref.evs(T1).a).cmd=write & acc.wr0(ref.evs(T1).m,ref.evs(T1).a).p=ref.evs(T1).p)) &
|
|
((ref.evs(T1).op=write & ref.evs(T1).sub) -> (acc.wr1(ref.evs(T1).m,ref.evs(T1).a).cmd=write & acc.wr1(ref.evs(T1).m,ref.evs(T1).a).p=ref.evs(T1).p)) &
|
|
((ref.evs(T1).op=read & ~ref.evs(T1).sub) -> (acc.rd0(ref.evs(T1).m,ref.evs(T1).a).cmd=read & acc.rd0(ref.evs(T1).m,ref.evs(T1).a).p=ref.evs(T1).p)) &
|
|
((ref.evs(T1).op=read & ref.evs(T1).sub) -> (acc.rd1(ref.evs(T1).m,ref.evs(T1).a).cmd=read & acc.rd1(ref.evs(T1).m,ref.evs(T1).a).p=ref.evs(T1).p))
|
|
)
|
|
|
|
###
|
|
|
|
conjecture (ref.evs(T).op~=nop & ~ref.evs(T).serialized) <-> ref.evs(T).l~=init_l
|
|
#conjecture (ref.evs(T).op~=nop & ~ref.evs(T).serialized) <-> ref.evs(T).agt~=init_agt
|
|
conjecture (ref.evs(T).op~=nop & ~ref.evs(T).serialized) -> ref.evs(T).agt~=init_agt
|
|
conjecture ref.evs(T).op=nop <-> ref.evs(T).agt=init_agt
|
|
|
|
conjecture (ref.evs(T).op=write & ~ref.evs(T).serialized & ~ref.evs(T).sub & (isd.isd_wr0(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
(ref.evs(T).l=acc_l <-> (acc.wr0(ref.evs(T).m,ref.evs(T).a).cmd=write & acc.wr0(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=afc_l <-> (afc.wr0(ref.evs(T).m,ref.evs(T).a).cmd=write & afc.wr0(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=amcc_l <-> (amcc(ref.evs(T).m).wr0(ref.evs(T).a).cmd=write & amcc(ref.evs(T).m).wr0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=dcs_l <-> (dcs(ref.evs(T).m).wr0(ref.evs(T).a).cmd=write & dcs(ref.evs(T).m).wr0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l=acc_l -> acc.wr0(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=afc_l -> afc.wr0(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=amcc_l -> amcc(ref.evs(T).m).wr0(ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=dcs_l -> dcs(ref.evs(T).m).wr0(ref.evs(T).a).data=ref.evs(T).data) &
|
|
|
|
(ref.evs(T).l~=acc_l -> ~(acc.wr0(M,ref.evs(T).a).cmd=write & acc.wr0(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=afc_l -> ~(afc.wr0(M,ref.evs(T).a).cmd=write & afc.wr0(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=amcc_l -> ~(amcc(M).wr0(ref.evs(T).a).cmd=write & amcc(M).wr0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=dcs_l -> ~(dcs(M).wr0(ref.evs(T).a).cmd=write & dcs(M).wr0(ref.evs(T).a).p=ref.evs(T).p))
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=write & ~ref.evs(T).serialized & ref.evs(T).sub & (isd.isd_wr1(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
(ref.evs(T).l=acc_l <-> (acc.wr1(ref.evs(T).m,ref.evs(T).a).cmd=write & acc.wr1(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=afc_l <-> (afc.wr1(ref.evs(T).m,ref.evs(T).a).cmd=write & afc.wr1(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=amcc_l <-> (amcc(ref.evs(T).m).wr1(ref.evs(T).a).cmd=write & amcc(ref.evs(T).m).wr1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=dcs_l <-> (dcs(ref.evs(T).m).wr1(ref.evs(T).a).cmd=write & dcs(ref.evs(T).m).wr1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l=acc_l -> acc.wr1(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=afc_l -> afc.wr1(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=amcc_l -> amcc(ref.evs(T).m).wr1(ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=dcs_l -> dcs(ref.evs(T).m).wr1(ref.evs(T).a).data=ref.evs(T).data) &
|
|
|
|
(ref.evs(T).l~=acc_l -> ~(acc.wr1(M,ref.evs(T).a).cmd=write & acc.wr1(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=afc_l -> ~(afc.wr1(M,ref.evs(T).a).cmd=write & afc.wr1(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=amcc_l -> ~(amcc(M).wr1(ref.evs(T).a).cmd=write & amcc(M).wr1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=dcs_l -> ~(dcs(M).wr1(ref.evs(T).a).cmd=write & dcs(M).wr1(ref.evs(T).a).p=ref.evs(T).p))
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ~ref.evs(T).sub & (isd.isd_rd0(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
(ref.evs(T).l=acc_l <-> (acc.rd0(ref.evs(T).m,ref.evs(T).a).cmd=read & acc.rd0(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=afc_l <-> (afc.rd0(ref.evs(T).m,ref.evs(T).a).cmd=read & afc.rd0(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=amcc_l <-> (amcc(ref.evs(T).m).rd0(ref.evs(T).a).cmd=read & amcc(ref.evs(T).m).rd0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=dcs_l <-> (dcs(ref.evs(T).m).rd0(ref.evs(T).a).cmd=read & dcs(ref.evs(T).m).rd0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l~=acc_l -> ~(acc.rd0(M,ref.evs(T).a).cmd=read & acc.rd0(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=afc_l -> ~(afc.rd0(M,ref.evs(T).a).cmd=read & afc.rd0(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=amcc_l -> ~(amcc(M).rd0(ref.evs(T).a).cmd=read & amcc(M).rd0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=dcs_l -> ~(dcs(M).rd0(ref.evs(T).a).cmd=read & dcs(M).rd0(ref.evs(T).a).p=ref.evs(T).p))
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ~ref.evs(T).sub & (isd.isd_rd0(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
~(acc.rsp0(M,ref.evs(T).a).cmd=rrsp & acc.rsp0(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(afc.rsp0(M,ref.evs(T).a).cmd=rrsp & afc.rsp0(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(amcc(M).rsp0(ref.evs(T).a).cmd=rrsp & amcc(M).rsp0(ref.evs(T).a).p=ref.evs(T).p)
|
|
)
|
|
|
|
conjecture (ref.evs(T0).op~=nop & ~ref.evs(T0).serialized & ref.evs(T1).op~=nop & ~ref.evs(T1).serialized & ref.evs(T0).a=ref.evs(T1).a) -> ref.evs(T0).m=ref.evs(T1).m
|
|
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ref.evs(T).sub & (isd.isd_rd1(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
(ref.evs(T).l=acc_l <-> (acc.rd1(ref.evs(T).m,ref.evs(T).a).cmd=read & acc.rd1(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=afc_l <-> (afc.rd1(ref.evs(T).m,ref.evs(T).a).cmd=read & afc.rd1(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=amcc_l <-> (amcc(ref.evs(T).m).rd1(ref.evs(T).a).cmd=read & amcc(ref.evs(T).m).rd1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=dcs_l <-> (dcs(ref.evs(T).m).rd1(ref.evs(T).a).cmd=read & dcs(ref.evs(T).m).rd1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l~=acc_l -> ~(acc.rd1(M,ref.evs(T).a).cmd=read & acc.rd1(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=afc_l -> ~(afc.rd1(M,ref.evs(T).a).cmd=read & afc.rd1(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=amcc_l -> ~(amcc(M).rd1(ref.evs(T).a).cmd=read & amcc(M).rd1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=dcs_l -> ~(dcs(M).rd1(ref.evs(T).a).cmd=read & dcs(M).rd1(ref.evs(T).a).p=ref.evs(T).p))
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ref.evs(T).sub & (isd.isd_rd1(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
~(acc.rsp1(M,ref.evs(T).a).cmd=rrsp & acc.rsp1(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(afc.rsp1(M,ref.evs(T).a).cmd=rrsp & afc.rsp1(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(amcc(M).rsp1(ref.evs(T).a).cmd=rrsp & amcc(M).rsp1(ref.evs(T).a).p=ref.evs(T).p)
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=rrsp & ~ref.evs(T).serialized) -> ref.evs(T).l ~= dcs_l
|
|
|
|
conjecture (ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ~ref.evs(T).sub & (isd.isd_rd0(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
(ref.evs(T).l=acc_l <-> (acc.rsp0(ref.evs(T).m,ref.evs(T).a).cmd=rrsp & acc.rsp0(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=afc_l <-> (afc.rsp0(ref.evs(T).m,ref.evs(T).a).cmd=rrsp & afc.rsp0(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=amcc_l <-> (amcc(ref.evs(T).m).rsp0(ref.evs(T).a).cmd=rrsp & amcc(ref.evs(T).m).rsp0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l~=acc_l -> ~(acc.rsp0(M,ref.evs(T).a).cmd=rrsp & acc.rsp0(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=afc_l -> ~(afc.rsp0(M,ref.evs(T).a).cmd=rrsp & afc.rsp0(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=amcc_l -> ~(amcc(M).rsp0(ref.evs(T).a).cmd=rrsp & amcc(M).rsp0(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l=acc_l -> acc.rsp0(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=afc_l -> afc.rsp0(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=amcc_l -> amcc(ref.evs(T).m).rsp0(ref.evs(T).a).data=ref.evs(T).data)
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ~ref.evs(T).sub & (isd.isd_rd0(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
~(acc.rd0(M,ref.evs(T).a).cmd=read & acc.rd0(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(afc.rd0(M,ref.evs(T).a).cmd=read & afc.rd0(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
|
|
~(amcc(M).rd0(ref.evs(T).a).cmd=read & amcc(M).rd0(ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(dcs(M).rd0(ref.evs(T).a).cmd=read & dcs(M).rd0(ref.evs(T).a).p=ref.evs(T).p)
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ref.evs(T).sub & (isd.isd_rd1(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
(ref.evs(T).l=acc_l <-> (acc.rsp1(ref.evs(T).m,ref.evs(T).a).cmd=rrsp & acc.rsp1(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=afc_l <-> (afc.rsp1(ref.evs(T).m,ref.evs(T).a).cmd=rrsp & afc.rsp1(ref.evs(T).m,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l=amcc_l <-> (amcc(ref.evs(T).m).rsp1(ref.evs(T).a).cmd=rrsp & amcc(ref.evs(T).m).rsp1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l~=acc_l -> ~(acc.rsp1(M,ref.evs(T).a).cmd=rrsp & acc.rsp1(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=afc_l -> ~(afc.rsp1(M,ref.evs(T).a).cmd=rrsp & afc.rsp1(M,ref.evs(T).a).p=ref.evs(T).p)) &
|
|
(ref.evs(T).l~=amcc_l -> ~(amcc(M).rsp1(ref.evs(T).a).cmd=rrsp & amcc(M).rsp1(ref.evs(T).a).p=ref.evs(T).p)) &
|
|
|
|
(ref.evs(T).l=acc_l -> acc.rsp1(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=afc_l -> afc.rsp1(ref.evs(T).m,ref.evs(T).a).data=ref.evs(T).data) &
|
|
(ref.evs(T).l=amcc_l -> amcc(ref.evs(T).m).rsp1(ref.evs(T).a).data=ref.evs(T).data)
|
|
)
|
|
|
|
conjecture (ref.evs(T).op=rrsp & ~ref.evs(T).serialized & ref.evs(T).sub & (isd.isd_rd1(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T)))
|
|
-> (
|
|
~(acc.rd1(M,ref.evs(T).a).cmd=read & acc.rd1(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(afc.rd1(M,ref.evs(T).a).cmd=read & afc.rd1(M,ref.evs(T).a).p=ref.evs(T).p) &
|
|
|
|
~(amcc(M).rd1(ref.evs(T).a).cmd=read & amcc(M).rd1(ref.evs(T).a).p=ref.evs(T).p) &
|
|
~(dcs(M).rd1(ref.evs(T).a).cmd=read & dcs(M).rd1(ref.evs(T).a).p=ref.evs(T).p)
|
|
)
|
|
|
|
### PIO from the same source to the same dest stay in order, if both are non-posted or both are posted
|
|
|
|
conjecture (
|
|
(ref.evs(T0).op=read & ~ref.evs(T0).serialized | ref.evs(T0).op=write & ~ref.evs(T0).serialized) &
|
|
(ref.evs(T1).op=read & ~ref.evs(T1).serialized | ref.evs(T1).op=write & ~ref.evs(T1).serialized) &
|
|
ref.evs(T0).p=ref.evs(T1).p & ref.evs(T0).a=ref.evs(T1).a & ref.evs(T0).agt=ref.evs(T1).agt &
|
|
ref.evs(T0).io & ref.evs(T1).io & T0<T1 & ref.evs(T0).post=ref.evs(T1).post
|
|
)
|
|
-> (
|
|
(ref.evs(T0).l=acc_l -> ref.evs(T1).l=acc_l) &
|
|
(ref.evs(T0).l=afc_l -> (ref.evs(T1).l=acc_l | ref.evs(T1).l=afc_l)) &
|
|
(ref.evs(T0).l=amcc_l -> (ref.evs(T1).l=acc_l | ref.evs(T1).l=afc_l | ref.evs(T1).l=amcc_l)) &
|
|
(ref.evs(T0).l=dcs_l -> (ref.evs(T1).l=acc_l | ref.evs(T1).l=afc_l | ref.evs(T1).l=amcc_l | ref.evs(T1).l=dcs_l))
|
|
)
|
|
|
|
###
|
|
|
|
conjecture ref.evs(T).op~=nop -> ref.evs(T).rspro
|
|
|
|
###
|
|
|
|
conjecture (amcc(M0).wr0(A).cmd=write & amcc(M1).wr0(A).cmd=write) -> M0=M1
|
|
conjecture (amcc(M0).wr1(A).cmd=write & amcc(M1).wr1(A).cmd=write) -> M0=M1
|
|
|
|
conjecture (amcc(M0).rd0(A).cmd=read & amcc(M1).rd0(A).cmd=read) -> M0=M1
|
|
conjecture (amcc(M0).rd1(A).cmd=read & amcc(M1).rd1(A).cmd=read) -> M0=M1
|
|
|
|
conjecture (amcc(M0).rsp0(A).cmd=rrsp & amcc(M1).rsp0(A).cmd=rrsp) -> M0=M1
|
|
conjecture (amcc(M0).rsp1(A).cmd=rrsp & amcc(M1).rsp1(A).cmd=rrsp) -> M0=M1
|
|
|
|
###
|
|
|
|
conjecture (ref.evs(T).op~=nop & ~ref.evs(T).serialized & ref.evs(T).io) -> ~ref.evs(T).ro
|
|
|
|
###
|
|
|
|
####
|
|
|
|
conjecture (ref.evs(T).op~=nop & ~ref.evs(T).serialized & ref.evs(T).io & ref.evs(T).agt=arm_agt) -> ref.evs(T).ch=bulk
|
|
|
|
####
|
|
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ref.evs(T).agt=arm_agt & ref.evs(T).l=amcc_l & ref.evs(T).sub) -> amcc(ref.evs(T).m).rd1(ref.evs(T).a).cmd=read
|
|
conjecture (ref.evs(T).op=read & ~ref.evs(T).serialized & ref.evs(T).agt=arm_agt & ref.evs(T).l=amcc_l & ~ref.evs(T).sub) -> amcc(ref.evs(T).m).rd0(ref.evs(T).a).cmd=read
|
|
|
|
###
|
|
|
|
conjecture ref.evs(T).op=read -> ~ref.evs(T).serialized
|
|
conjecture ref.evs(T).op=read -> ref.evs(T).time=0
|
|
|
|
#ISSUE2
|
|
conjecture ref.evs(T).op=rrsp -> ~(ref.gt=0)
|
|
|
|
export arm.step
|
|
export acc.step
|
|
export afc.step
|
|
export amcc.step
|
|
export dcs.dcs_step
|
|
|
|
|
|
|