Copyright 2023, Apple, Inc.

This file is provided under the terms of the MIT license as part of the Ivy tool. For license terms, see the file license.txt.

Purpose

ordering model consisting of arm (aka arm), cfabric, ifabric, memc, and dramc

 arm - ARM agent that issues write/read with  various address attributes,
       to a PIO register in memc, or DRAM memory
       conntected to dramc

 cfabric  - fabric interconnect for DRAM memory traffic
 ifabric  - fabric interconnect for PIO traffic
 memc     - memory controller
 dramc    - dram controller

 There are multiple arm modules, connected logically to a single cfabric,
 and ifabric which in turn connect to multiple memc, which are each connected
 to a dramc

 The ordering specification for the arm module is based on ARM Architecture
 Reference Manual, Chapter B.2

include order

instance lclock : unbounded_sequence

finite type proc
finite type mem_type
finite type addr_type

Need to record write->wr_cmp and read->rrsp termination time, i.e. when write data becomes visible, and when read data is read at target/destination

instance tar_clock    : unbounded_sequence

instance tar_cf_clock : unbounded_sequence

write, read, read response rrsp and write completions wr_cmp op

type op_type      = {nop,write,read,rrsp,wr_cmp}

an op has a location corresponding to one of the module types

type loc_type     = {init_l,cf_mem_l,cf_pio_l,cf_cmp_l,if_l,memc_l,dramc_l,arm_l}

this model issues op to dram mem_memc, or memc pio register pio_memc

type mem_loc_type = {mem_loc_init,mem_memc,pio_memc}

memory attribute: Gather (G), non-Gather (nG), Relaxed (R), non-Relaxed (nR), Early completion (E), non-Early (nE) ARM Architecture Reference Manual, Chapter B.2

type op_ack_type  = {nGnRnE,nGnRE,nGRE,_GRE,normal}

non-determinsitic choice write, read, completion (cpl) - process messages in a module in all possible orders

type ph_type      = {nop_ph, wr_ph, rd_ph, cpl_ph}

Event structure (original version from FMCAD2016 Tilelink paper)

module evs_type = {
    individual p          : proc
    individual m          : mem_type
    individual a          : addr_type

    individual mem_loc    : mem_loc_type

    individual req        : op_type
    individual cmp        : op_type

    individual op_ack     : op_ack_type

    individual l_req      : loc_type # location request
    individual l_cmp      : loc_type # location completion

    individual serialized : bool     # wr_cmp reaches destination/rrsp reaches originator

    individual lt_tar    : tar_clock # lt when reaches target: write->wr_cmp or read->rrsp
    individual lt_arr    : tar_clock # lt when write/read enter memc going to mem_memc

    individual lt_arr_cf : tar_cf_clock # lt when write/read enter memc going to mem_memc
}

Request and response buffers used by arm agent

object isd = {
    after init {
     wr(P,M,A,T)         := false;
     rd(P,M,A,T)         := false;

     rsp(P,M,A,T)        := false;
    }

    relation wr(P:proc,M:mem_type,A:addr_type,T:lclock)
    relation rd(P:proc,M:mem_type,A:addr_type,T:lclock)

    relation rsp(P:proc,M:mem_type,A:addr_type,T:lclock)
}

Memory access reference model

object ref = {

    instantiate evs(T:lclock) : evs_type

current request time

    individual  lt  : lclock

current arrival time

    individual  lt_tar(M:mem_type) : tar_clock

    individual  lt_tar_cf  : tar_cf_clock

    relation   dev(T:lclock)

mem read leading second mem read and older read response past ioa

    relation both_nGnR(T0:lclock,T1:lclock)
    relation both_nGR(T0:lclock,T1:lclock)

    relation same_addr(T0:lclock,T1:lclock)
    relation same_attr(T0:lclock,T1:lclock)

event T0 prevents T1 if it must come before (become globally visible before) T1 according to the ordering conditions, but is not yet serialized. There is an ordering requirement on reads and writes from the same instance, and for the same type of address. And then only for reads and writes that are non-relaxed ordered, or are to/from the same address

For writes the prevents method is called when the data is written i.e. when the operation reaches its destination

For reads the prevents method is called when the data is read

For reads the prevents method is called when the read response, is returned to the requesting instance of the requesting agent

    relation   prevents(T0:lclock,T1:lclock)

    relation   mem_memc_exception(T0:lclock,T1:lclock)

    relation pio(T:lclock)

    definition prevents(T0:lclock,T1:lclock) =
                                 ((evs(T0).req~=nop | evs(T0).cmp~=nop) & ((~evs(T0).serialized & evs(T1).serialized | evs(T0).l_cmp~=init_l & evs(T1).l_cmp=init_l)
                                     & (T0<T1) |
                     evs(T1).l_req~=init_l & evs(T0).serialized & (T1<T0)
                                 ))
                   & evs(T0).p=evs(T1).p
                   & (evs(T0).m=evs(T1).m & evs(T0).a=evs(T1).a & same_attr(T0,T1))
                   & ~mem_memc_exception(T0,T1)

    definition mem_memc_exception(T0:lclock,T1:lclock) = evs(T0).cmp=rrsp & evs(T1).cmp=rrsp &
                                                         evs(T0).m=evs(T1).m & evs(T0).a=evs(T1).a & same_attr(T0,T1) &
                                                         evs(T0).mem_loc=mem_memc & evs(T1).mem_loc=mem_memc

    relation both_normal(T0:lclock,T1:lclock)
    relation nGR(OP_ACK:op_ack_type)
    relation nGnR(OP_ACK:op_ack_type)

    definition pio(T:lclock)           =  dev(T) & evs(T).mem_loc=pio_memc

    definition same_addr(T0:lclock,T1:lclock)   = evs(T0).m=evs(T1).m & evs(T0).a=evs(T1).a
    definition same_attr(T0:lclock,T1:lclock)   = both_nGnR(T0,T1) | both_nGR(T0,T1) | both_normal(T0,T1)

    definition both_normal(T0:lclock,T1:lclock) = evs(T0).op_ack=normal & evs(T1).op_ack=normal
    definition both_nGnR(T0:lclock,T1:lclock)   = (evs(T0).op_ack=nGnRnE | evs(T0).op_ack=nGnRE) & (evs(T1).op_ack=nGnRnE | evs(T1).op_ack=nGnRE)
    definition both_nGR(T0:lclock,T1:lclock)    = (evs(T0).op_ack=nGRE   | evs(T0).op_ack=_GRE)  & (evs(T1).op_ack=nGRE   | evs(T1).op_ack=_GRE)
    definition nGR(OP_ACK:op_ack_type)        = (OP_ACK=nGRE    | OP_ACK=_GRE)
    definition nGnR(OP_ACK:op_ack_type)       = (OP_ACK=nGnRE   | OP_ACK=nGnRnE)

    definition dev(T:lclock)  = nGR(evs(T).op_ack) | nGnR(evs(T).op_ack)

relation   pnd_or_ser_wr(P:proc,M:mem_type,A:addr_type,T:lclock)
relation   pnd_or_ser_rd(P:proc,M:mem_type,A:addr_type,T:lclock)

definition pnd_or_ser_wr(P:proc,M:mem_type,A:addr_type,T:lclock) = isd.wr(P,M,A,T) | evs(T).cmp=wr_cmp & evs(T).p=P & evs(T).m=M & evs(T).a=A & evs(T).serialized
definition pnd_or_ser_rd(P:proc,M:mem_type,A:addr_type,T:lclock) = isd.rd(P,M,A,T) | evs(T).cmp=rrsp & evs(T).p=P & evs(T).m=M & evs(T).a=A & evs(T).serialized

    after init {
    lt                  := 0;
    lt_tar(M)           := 0;
    lt_tar_cf           := 0;

    evs(T).req          := nop;
    evs(T).cmp          := nop;
    evs(T).op_ack       := normal;
    evs(T).serialized   := true;
    evs(T).l_req        := init_l;
    evs(T).l_cmp        := init_l;
    evs(T).mem_loc      := mem_loc_init;
    evs(T).lt_arr       := 0;
    evs(T).lt_arr_cf    := 0;
    }

create a new evs structure when read/write are issued by an arm instance

    action create(p:proc,op:op_type,op_ack:op_ack_type,m:mem_type,a:addr_type,mem_loc:mem_loc_type,l:loc_type) = {

    evs(lt).p          := p;
    evs(lt).req        := op;
    evs(lt).cmp        := nop;
    evs(lt).op_ack     := op_ack;

    evs(lt).m          := m;
    evs(lt).a          := a;
    evs(lt).mem_loc    := mem_loc;
    evs(lt).serialized := false;

    evs(lt).l_req      := l;

        evs(lt).lt_arr     := 0;
    }

rrsp/wr_cmp arrives at the issuer

    action perform(p:proc, lt:lclock) = {
        var m : mem_type;
    var a : addr_type;

update the global memory state

        m := evs(lt).m;
    a := evs(lt).a;

    if evs(lt).cmp = rrsp {

serialize at current global time

        evs(lt).serialized := true;
    };

        evs(lt).l_cmp      := init_l;
    }

read/write arrives at the target

    action perform_grd(lt:lclock) = {
        var m : mem_type;
    var a : addr_type;

update the global memory state

    a := evs(lt).a;
        m := evs(lt).m;

        assert ~evs(lt).serialized;

    if evs(lt).req = read {
            evs(lt).l_req     := init_l;

            evs(lt).req       := nop;

            evs(lt).cmp       := rrsp;

        lt_tar(evs(lt).m) := lt_tar(evs(lt).m).next;
            evs(lt).lt_tar    := lt_tar(evs(lt).m);

    } else if evs(lt).req = write {

serialize at current global time

        evs(lt).serialized := true;

            evs(lt).l_req      := init_l;

            evs(lt).cmp        := wr_cmp;
            evs(lt).req        := nop;

        lt_tar(evs(lt).m)  := lt_tar(evs(lt).m).next;
            evs(lt).lt_tar     := lt_tar(evs(lt).m);

        }
    }

}

arm

module arm_mod = {

    action issue_hook(p:proc,lt:lclock)
    action retire_hook(p:proc,lt:lclock)

    action step_north(ph:ph_type,p:proc,m:mem_type,a:addr_type,choose_op_ack:op_ack_type,mem_loc_arg:mem_loc_type) = {

        var mem_loc    : mem_loc_type;
        var op_ack     : op_ack_type;

        var pio_new    : bool;
        var dram_new   : bool;

    var wr         : bool;
    var rd         : bool;

    var dev        : bool;

open arm_def.ivy

    var ordser0 : bool;
    var ordser1 : bool;
    var ordser2 : bool;
    var ordser3 : bool;
    var ordser4 : bool;
    var ordser5 : bool;
    var ordser6 : bool;
    var ordser7 : bool;
    var ordser8 : bool;
    var ordser9 : bool;
    var ordser10 : bool;
    var ordser11 : bool;
    var ordser12 : bool;
    var ordser13 : bool;
    var ordser14 : bool;
    var ordser15 : bool;
    var ordser16 : bool;

    var ordser : bool;

        wr       := false;
    rd       := false;

    if ph=wr_ph {
        wr         := true;
    } else if ph=rd_ph {
        rd         := true;
    };

make sure all uses of address 'a' agree on m attribute the memc that routes to the address - this is a global attribute applies to all instances

    if some tt:lclock. (ref.evs(tt).req=read | ref.evs(tt).req=write | ref.evs(tt).cmp=rrsp | ref.evs(tt).cmp=wr_cmp) & ref.evs(tt).m=m & ref.evs(tt).a=a {
        mem_loc := ref.evs(tt).mem_loc;

            if mem_loc=mem_memc {
        if ~(choose_op_ack=nGnRnE | choose_op_ack=nGnRE) {
                op_ack  := choose_op_ack;
        } else {
                op_ack  := normal; # pick one
        }
        } else {
        if ~(choose_op_ack=normal) {
                op_ack  := choose_op_ack;
        } else {
                op_ack  := nGnRnE; # pick one
        }
        };

            pio_new  :=  ref.dev(tt) & mem_loc=pio_memc;
            dram_new :=  mem_loc=mem_memc;

    } else {
            if mem_loc_arg=pio_memc {
        mem_loc := mem_loc_arg;

        pio_new  :=  mem_loc_arg=pio_memc;
        dram_new :=  false;

        if ~(choose_op_ack=normal) {
            op_ack := choose_op_ack;
        } else {
                op_ack  := nGnRnE; # pick one
        }
        } else {
                mem_loc      := mem_memc;

                if choose_op_ack=nGRE {
            op_ack       := nGRE;
                } else if choose_op_ack=_GRE {
            op_ack       := _GRE;
        } else {
            op_ack       := normal;
        };

                pio_new      := false;
                dram_new     := true;
        }
        };

        dev := op_ack~=normal;

open arm_ord.ivy

    ordser0 := wr & dev & ref.nGnR(op_ack) & (exists M,A,T. isd.wr(p,M,A,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGnR(ref.evs(T).op_ack) & pio_new & ~(M=m & A=a));
    ordser1 := wr & dev & ref.nGnR(op_ack) & (exists M,A,T. isd.rd(p,M,A,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGnR(ref.evs(T).op_ack));
    ordser2 := wr & dev & ref.nGnR(op_ack) & (exists M,A,T. isd.rd(p,M,A,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGR(ref.evs(T).op_ack));
    ordser3 := wr & dev & ref.nGR(op_ack) & (exists M,A,T. isd.rd(p,M,A,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGnR(ref.evs(T).op_ack));
    ordser4 := wr & dev & ref.nGR(op_ack) & (exists M,A,T. isd.rd(p,M,A,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGR(ref.evs(T).op_ack));
    ordser5 := wr & ~dev & (exists T. isd.wr(p,m,a,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T) & dram_new);
    ordser6 := wr & ~dev & (exists T. isd.wr(p,m,a,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T) & pio_new);
    ordser7 := wr & ~dev & (exists M,A,T. isd.rd(p,M,A,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T));
    ordser8 := rd & dev & ref.nGnR(op_ack) & (exists M,A,T. isd.wr(p,M,A,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGnR(ref.evs(T).op_ack) & dram_new);
    ordser9 := rd & dev & ref.nGnR(op_ack) & (exists M,A,T. isd.wr(p,M,A,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGnR(ref.evs(T).op_ack) & pio_new);
    ordser10 := rd & dev & ref.nGnR(op_ack) & (exists M,A,T. isd.rd(p,M,A,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGnR(ref.evs(T).op_ack) & pio_new & ~(M=m & A=a));
    ordser11 := rd & dev & ref.nGR(op_ack) & (exists T. isd.wr(p,m,a,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGR(ref.evs(T).op_ack) & dram_new);
    ordser12 := rd & dev & ref.nGR(op_ack) & (exists T. isd.wr(p,m,a,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ref.dev(T) & ref.nGR(ref.evs(T).op_ack) & pio_new);
    ordser13 := rd & ~dev & (exists T. isd.wr(p,m,a,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T) & dram_new);
    ordser14 := rd & ~dev & (exists T. isd.wr(p,m,a,T) & (ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T) & pio_new);
    ordser15 := rd & ~dev & (exists T. isd.rd(p,m,a,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T) & dram_new);
    ordser16 := rd & ~dev & (exists T. isd.rd(p,m,a,T) & (ref.evs(T).req=read | ref.evs(T).cmp=rrsp & ~(ref.evs(T).l_cmp=init_l)) & ~ref.dev(T) & pio_new);

    ordser := ordser0 | ordser1 | ordser2 | ordser3 | ordser4 | ordser5 | ordser6 | ordser7 | ordser8 | ordser9 | ordser10 | ordser11 | ordser12 | ordser13 | ordser14 | ordser15 | ordser16;

if ph=wr_ph & wr & ~ordser { ref.lt := ref.lt.next;

issue_hook(p,ref.lt);
isd.wr(p,m,a,ref.lt) := true;

if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).mem_loc=mem_memc & ref.evs(tt).l_req=cf_mem_l minimizing tt {
#       cfabric.t_rd_min := tt;
} else {
cfabric.t_rd_min := ref.lt.next;
}

if mem_loc=mem_memc {
call ref.create(p,write,op_ack,m,a,mem_loc,cf_mem_l);
} else {
call ref.create(p,write,op_ack,m,a,mem_loc,cf_pio_l);
};

} else if ph=rd_ph & rd & ~ordser { ref.lt := ref.lt.next;

issue_hook(p,ref.lt);
isd.rd(p,m,a,ref.lt)  := true;
isd.rsp(p,m,a,ref.lt) := false;

if mem_loc=mem_memc {
    ref.lt_tar_cf := ref.lt_tar_cf.next;

if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).mem_loc=mem_memc & ref.evs(tt).l_req=cf_mem_l {
    # cfabric.t_rd_min unchanged
} else {
    cfabric.t_rd_min     := ref.lt;
    cfabric.t_rd_arr_min := ref.lt_tar_cf;
};


call ref.create(p,read,op_ack,m,a,mem_loc,cf_mem_l);

    ref.evs(ref.lt).lt_arr_cf  := ref.lt_tar_cf;

} else {
if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).mem_loc=mem_memc & ref.evs(tt).l_req=cf_mem_l minimizing tt {
    #       cfabric.t_rd_min := tt;
} else {
    cfabric.t_rd_min := ref.lt.next;
};

call ref.create(p,read,op_ack,m,a,mem_loc,cf_pio_l);
}

} } receive read and write response and check ordering

OrdROB - is to model arm rob

    individual cpl_fair(P:proc) : bool

    after init {
        cpl_fair(P)  := false;
    }

    action step_south(ph:ph_type,p:proc,t:lclock,m:mem_type,a:addr_type) = {
    var ordrob : bool;

    var ordrob0 : bool;
    var ordrob1 : bool;

    var ordser : bool;

    var ordser0 : bool;
    var ordser1 : bool;

        cpl_fair(p) := ph=cpl_ph;
        cpl_fair(p) := false;

if ph=cpl_ph & ref.evs(t).p=p & ref.evs(t).m=m & ref.evs(t).a=a & ref.evs(t).l_cmp=arm_l {}

Refactored the ROB logic here. We first find the least operation that is not blocked by ordering rules. Then if it is completed, we retire it.

        if ph=cpl_ph {
            retire_hook(p,t);
            if some tt:lclock. ref.evs(tt).p=p &
            (ref.evs(tt).cmp=rrsp | ref.evs(tt).cmp=wr_cmp) &
            ref.evs(tt).l_cmp~=init_l
            minimizing tt {

                m := ref.evs(tt).m;
                a := ref.evs(tt).a;
            if  ref.evs(tt).l_cmp=arm_l {
                    ordrob0 := exists T. (ref.evs(T).cmp=rrsp & ref.evs(T).l_cmp~=init_l) & ref.evs(T).p=p & T<tt;
                    ordrob1 := exists T. (ref.evs(T).cmp=wr_cmp & ref.evs(T).l_cmp~=init_l) & ref.evs(T).p=p & T<tt;

ordrob := ordrob0 | ordrob1;

                    ordrob := false;

                    if ref.evs(tt).cmp=rrsp {
                        call ref.perform(p,tt);

                        assert ~ref.prevents(T,tt);

                        isd.rsp(p,m,a,tt)   := false;
                        isd.rd(p,m,a,tt)    := false;
                    } else if ref.evs(tt).cmp=wr_cmp {
                        call ref.perform(p,tt);

                        assert ~ref.prevents(T,tt);

                        isd.wr(p,m,a,tt)    := false;
                    }
                }
            }
        }
    }
}

cfabric fabric

object cfabric = {

    individual rd_fair : bool
    individual wr_fair : bool
    individual rd_pio_fair : bool
    individual wr_pio_fair : bool
    individual cpl_fair : bool

    individual t_rd_min     : lclock # current cfabric rd to be serviced
    individual t_rd_arr_min : tar_cf_clock # current cfabric rd to be serviced

    after init {
     rd_fair             := false;
     wr_fair             := false;
     rd_pio_fair         := false;
     wr_pio_fair         := false;
     cpl_fair            := false;

     t_rd_min            := 0;
     t_rd_arr_min        := 0;
    }

    action complete_hook(lt:lclock)

    action step(ph:ph_type,sel_memc:bool) = {
        var p : proc;
    var m : mem_type;
    var a : addr_type;

    var ordpip0 : bool;
    var ordpip1 : bool;
    var ordpip2 : bool;
    var ordpip3 : bool;

    var ordpip : bool;

        var t          : lclock;

        var wr         : bool;
    var rd         : bool;
    var cmp        : bool;

        wr      := false;
    rd      := false;
    cmp     := false;

        rd_fair := ph=rd_ph & sel_memc;
    rd_fair := false;

        wr_fair := ph=wr_ph & sel_memc;
    wr_fair := false;

        rd_pio_fair := ph=rd_ph & ~sel_memc;
    rd_pio_fair := false;

        wr_pio_fair := ph=wr_ph & ~sel_memc;
    wr_pio_fair := false;

        cpl_fair := ph=cpl_ph;
    cpl_fair := false;

3 channels that process messages in arrival order ph selects between the channels

        if ph=rd_ph {
        if sel_memc {
        if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).mem_loc=mem_memc & ref.evs(tt).l_req=cf_mem_l minimizing ref.evs(tt).lt_arr_cf {
            t  := tt;

            p  := pp;
            m  := mm;
            a  := aa;

            rd := true;
        }
        } else {
        if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ~(ref.evs(tt).mem_loc=mem_memc) & ref.evs(tt).l_req=cf_pio_l minimizing tt {
            t  := tt;

            p  := pp;
            m  := mm;
            a  := aa;

            rd := true;
        }
        }
    } else if ph=wr_ph {
        if sel_memc {
        if  some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.wr(pp,mm,aa,tt) & ref.evs(tt).req=write & ref.evs(tt).l_req=cf_mem_l minimizing tt {
        t  := tt;
        p  := pp;
        m  := mm;
        a  := aa;

        wr := true;
        }
        } else {
        if  some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.wr(pp,mm,aa,tt) & ref.evs(tt).req=write & ref.evs(tt).l_req=cf_pio_l minimizing tt {
        t  := tt;
        p  := pp;
        m  := mm;
        a  := aa;

        wr := true;
        }
        }
    } else if ph=cpl_ph {
        if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. (isd.rd(pp,mm,aa,tt) & ref.evs(tt).cmp=rrsp | isd.wr(pp,mm,aa,tt) & ref.evs(tt).cmp=wr_cmp) & ref.evs(tt).l_cmp=cf_cmp_l minimizing tt {
        t   := tt;
        p  := pp;
        m  := mm;
        a  := aa;

            cmp := true;
        }
    };


    ordpip0 := rd & (exists M,A,T. isd.rd(p,M,A,T) & ref.evs(T).req=read & (ref.evs(T).l_req=cf_mem_l | ref.evs(T).l_req=cf_pio_l) & ref.evs(t).mem_loc=ref.evs(T).mem_loc & ref.evs(t).mem_loc=mem_memc & ref.evs(T).lt_arr_cf<ref.evs(t).lt_arr_cf); # processed

    ordpip1 := wr & (exists M,A,T. isd.wr(p,M,A,T) & ref.evs(T).req=write & (ref.evs(T).l_req=cf_mem_l | ref.evs(T).l_req=cf_pio_l) & ref.evs(t).mem_loc=ref.evs(T).mem_loc & ref.evs(t).mem_loc=mem_memc & T<t); # processed
    ordpip2 := rd & (exists M,A,T. isd.rd(p,M,A,T) & ref.evs(T).req=read & (ref.evs(T).l_req=cf_mem_l | ref.evs(T).l_req=cf_pio_l) &  ref.evs(t).mem_loc=ref.evs(T).mem_loc & ref.evs(t).mem_loc=pio_memc & T<t); # processed
    ordpip3 := wr & (exists M,A,T. isd.wr(p,M,A,T) & ref.evs(T).req=write & (ref.evs(T).l_req=cf_mem_l | ref.evs(T).l_req=cf_pio_l) & ref.evs(t).mem_loc=ref.evs(T).mem_loc & ref.evs(t).mem_loc=pio_memc & T<t); # processed

    ordpip := ordpip0 | ordpip1 | ordpip2 | ordpip3;

    if (rd | wr) & ~ordpip {
        if ref.evs(t).mem_loc=mem_memc {
        ref.evs(t).l_req      := memc_l;
        } else {
        ref.evs(t).l_req := if_l;

        assert ref.evs(t).mem_loc=pio_memc;
        }
        } else if cmp {
            complete_hook(t);
        ref.evs(t).l_cmp := arm_l;
    };

        if rd {
    if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).mem_loc=mem_memc & ref.evs(tt).l_req=cf_mem_l minimizing tt {
        t_rd_min := tt;
    } else if rd {
        t_rd_min := ref.lt.next;
    };

if ph=rd_ph & sel_memc {
    if some tt:lclock,pp:proc,mm:mem_type,aa:addr_type. isd.rd(pp,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).mem_loc=mem_memc & ref.evs(tt).l_req=cf_mem_l minimizing ref.evs(tt).lt_arr_cf {
        t_rd_arr_min := ref.evs(tt).lt_arr_cf;
    } else if rd {
        t_rd_arr_min := ref.lt_tar_cf.next;
    }
    }
    }
        memc_update_witnesses;

    }
}

ifabric fabric

object ifabric = {

    var rd_fair(P:proc) : bool
    var wr_fair(P:proc) : bool
    var cpl_fair(T:lclock) : bool

    after init {
        rd_fair(P) := false;
        wr_fair(P) := false;
        cpl_fair(T) := false;
    }

    action step(ph:ph_type,m:mem_type, a:addr_type, p:proc, lt:lclock) = {

    var ordpip0 : bool;
    var ordpip1 : bool;

    var ordpip : bool;


        var t : lclock;

        var wr       : bool;
    var rd       : bool;
    var cmp      : bool;

            rd_fair(p) := ph=rd_ph;
            rd_fair(P) := false;

            wr_fair(p) := ph=wr_ph;
            wr_fair(P) := false;

            cpl_fair(lt) := ph=cpl_ph;
            cpl_fair(T) := false;

        wr       := false;
    rd       := false;
    cmp      := false;

    if ph=rd_ph {
        if some tt:lclock,mm:mem_type,aa:addr_type. isd.rd(p,mm,aa,tt) & ref.evs(tt).req=read & ref.evs(tt).l_req=if_l minimizing tt {
               rd := true;
           t  := tt;
            }
    } else if ph=wr_ph {
        if some tt:lclock,mm:mem_type,aa:addr_type. isd.wr(p,mm,aa,tt) & ref.evs(tt).req=write & ref.evs(tt).l_req=if_l minimizing tt {
               wr := true;
           t  := tt;
            }
    } else if ph=cpl_ph {

if some tt:lclock. (isd.rd(p,m,a,tt) & ref.evs(tt).cmp=rrsp | isd.wr(p,m,a,tt) & ref.evs(tt).cmp=wr_cmp) & ref.evs(tt).m=m & ref.evs(tt).a=a & ref.evs(tt).p=p & ref.evs(tt).l_cmp=if_l KLM: modified so lt represents the 'next' completion in the queue. This way, we can deliver completions in any order, but guarantee that every completion is eventually delivered.

            if ref.evs(lt).l_cmp=if_l {
               cmp := true;
           t    := lt;
            }
    };

    ordpip0 := rd & (exists M,A,T. isd.rd(p,M,A,T) & ref.evs(T).req=read & ref.evs(T).l_req=if_l & T<t); # processed
    ordpip1 := wr & (exists M,A,T. isd.wr(p,M,A,T) & ref.evs(T).req=write & ref.evs(T).l_req=if_l & T<t); # processed

    ordpip := ordpip0 | ordpip1;

       if (rd | wr) & ~ordpip {
          if  (ref.evs(t).mem_loc=mem_memc | ref.evs(t).mem_loc=pio_memc) {
          ref.evs(t).l_req := memc_l;
          } else {
          assert false;
          }
       } else if cmp {
          ref.evs(t).l_cmp := cf_cmp_l;
       }
        memc_update_witnesses;
    }
}

MEMC

var memc_lt_min : lclock
var memc_pio_min : lclock
var memc_next : lclock
var memc_blocking : lclock

action memc_update_witnesses = {
    if some t4:lclock,pp:proc,mm:mem_type,aa:addr_type.
    (isd.wr(pp,mm,aa,t4) & ref.evs(t4).req=write | isd.rd(pp,mm,aa,t4) & ref.evs(t4).req=read)
    & ref.evs(t4).l_req=memc_l
    minimizing t4 {
    memc_lt_min := t4;
    }
    var mz := ref.evs(memc_lt_min).m;
    if some t5:lclock,pp:proc,aa:addr_type.
    (isd.wr(pp,mz,aa,t5) & ref.evs(t5).req=write | isd.rd(pp,mz,aa,t5) & ref.evs(t5).req=read)
    & ref.evs(t5).l_req=dramc_l
    minimizing ref.evs(t5).lt_arr {
    memc_next := t5;
        dramc(mz).t_min := ref.evs(t5).lt_arr;
    }
    if some t6:lclock.
          (ref.evs(t6).req=write | ref.evs(t6).req=read) & (ref.evs(t6).l_req=dramc_l)
        & ref.evs(t6).m = ref.evs(memc_lt_min).m
        & ref.evs(t6).a = ref.evs(memc_lt_min).a
        & ref.evs(t6).req = ref.evs(memc_lt_min).req {
        memc_blocking := t6;
    }

}

    object memc = {

individual rd_fair : bool

        individual rd_fair(M:mem_type, A:addr_type) : bool
        individual wr_fair(M:mem_type, A:addr_type) : bool
        individual cpl_fair(P:proc, M:mem_type, A:addr_type, T:lclock) : bool

    after init {

rd_fair := false;

        rd_fair(M,A)      := false;
        wr_fair(M,A)      := false;
        cpl_fair(P,M,A,T)  := false;
    }

        action memc_arr_hook(lt : lclock)
        action memc_push_hook(lt : lclock)
        action memc_cpl_hook(lt : lclock)

Added a paramter lt for local time of completions. This is to model the fact the completions are not ordered

    action step(ph:ph_type, p:proc, m:mem_type, a:addr_type, lt:lclock) = {
            var ordpip     : bool;

            var tt         : lclock;

rd_fair := ph=rd_ph; rd_fair := false;

    rd_fair(m,a) := ph=rd_ph;
    rd_fair(M,A) := false;

        wr_fair(m,a) := ph=wr_ph;
    wr_fair(M,A) := false;

        cpl_fair(p,m,a,lt) := ph=cpl_ph;
        cpl_fair(p,m,a,lt) := false;


        if ph=rd_ph {
        ordpip := true;
        tt     := 0;

if some t:lclock. isd.rd(p,m,a,t) & ref.evs(t).req=read & ref.evs(t).l_req=memc_l { tt := t; ordpip := exists T. isd.rd(p,m,a,T) & T<t & ref.evs(T).l_req=memc_l; };

        if some t:lclock, pp:proc. isd.rd(pp,m,a,t) & ref.evs(t).req=read & ref.evs(t).l_req=memc_l minimizing t{
                    tt := t;
            ordpip := false;
        };

            if ~ordpip & tt~=0 & ref.evs(tt).mem_loc=mem_memc {
                memc_push_hook(tt);
                if ~(exists T. ref.evs(T).req=read & ref.evs(T).m=m & ref.evs(T).a=a & ref.evs(T).l_req=dramc_l) {

                ref.lt_tar(ref.evs(tt).m)  := ref.lt_tar(ref.evs(tt).m).next;
                    ref.evs(tt).lt_arr  := ref.lt_tar(ref.evs(tt).m);

            ref.evs(tt).l_req := dramc_l;
                    memc_arr_hook(tt);
            }
        } else if ~ordpip & tt~=0 & ref.evs(tt).mem_loc=pio_memc {
                    ref.evs(tt).l_cmp := memc_l;

                isd.rsp(ref.evs(tt).p,m,a,tt)  := true;

                    call ref.perform_grd(tt);

                    ref.evs(tt).l_cmp := memc_l;

                assert ~ref.prevents(T,tt);
        }
        } else if ph=wr_ph {
        ordpip  := true;
        tt      := 0;

if some t:lclock. isd.wr(p,m,a,t) & ref.evs(t).req=write & ref.evs(t).l_req=memc_l { tt := t; ordpip := exists T. isd.wr(p,m,a,T) & T<t & ref.evs(T).l_req=memc_l; };

        if some t:lclock, pp:proc. isd.wr(pp,m,a,t) & ref.evs(t).req=write & ref.evs(t).l_req=memc_l minimizing t{
                    tt := t;
            ordpip := false;
        };

            if ~ordpip & tt~=0 & ref.evs(tt).mem_loc=mem_memc {
                memc_push_hook(tt);
                if ~(exists T. ref.evs(T).req=write & ref.evs(T).m=m & ref.evs(T).a=a & ref.evs(T).l_req=dramc_l) {

                ref.lt_tar(ref.evs(tt).m)          := ref.lt_tar(ref.evs(tt).m).next;
                    ref.evs(tt).lt_arr  := ref.lt_tar(ref.evs(tt).m);

                    ref.evs(tt).l_req := dramc_l;
                    memc_arr_hook(tt);
            }
        } else if ~ordpip & tt~=0 & (ref.evs(tt).mem_loc=pio_memc) {
            call ref.perform_grd(tt);

            ref.evs(tt).l_cmp := memc_l;

                    assert ~ref.prevents(T,tt);

        }
        } else if ph=cpl_ph & (exists T. (ref.evs(T).cmp=rrsp | ref.evs(T).cmp=wr_cmp) & ref.evs(T).m=m & ref.evs(T).a=a & ref.evs(T).l_cmp=memc_l) {
            var t := lt;

Modified this so that we process event lt, conceptually, the one that is next in the queue

        if (isd.rd(p,m,a,t) & ref.evs(t).cmp=rrsp | isd.wr(p,m,a,t) & ref.evs(t).cmp=wr_cmp) & ref.evs(t).l_cmp=memc_l & ref.evs(t).m=m {
        if ref.evs(t).mem_loc=mem_memc {
                    memc_cpl_hook(t);
            ref.evs(t).l_cmp := cf_cmp_l;

        } else if ref.evs(t).mem_loc=pio_memc {
            ref.evs(t).l_cmp := if_l;
        }
        }
    }

    if some t3:lclock,pp:proc,aa:addr_type. (isd.wr(pp,m,aa,t3) & ref.evs(t3).req=write | isd.rd(pp,m,aa,t3) & ref.evs(t3).req=read) & ref.evs(t3).l_req=dramc_l minimizing ref.evs(t3).lt_arr {
        dramc_next := t3;
        dramc(m).t_min := ref.evs(t3).lt_arr;
    }
        update_witnesses;
    memc_update_witnesses;
    }
}

var dramc_next : lclock
var dramc_lt_min : lclock

action update_witnesses = {
    if some t4:lclock,pp:proc,mm:mem_type,aa:addr_type.
    (isd.wr(pp,mm,aa,t4) & ref.evs(t4).req=write | isd.rd(pp,mm,aa,t4)
    & ref.evs(t4).req=read) & ref.evs(t4).l_req=dramc_l
    minimizing t4 {
    dramc_lt_min := t4;
    }
    var mz := ref.evs(dramc_lt_min).m;
    if some t5:lclock,pp:proc,aa:addr_type.
    (isd.wr(pp,mz,aa,t5) & ref.evs(t5).req=write | isd.rd(pp,mz,aa,t5) & ref.evs(t5).req=read)
    & ref.evs(t5).l_req=dramc_l
    minimizing ref.evs(t5).lt_arr {
    dramc_next := t5;
        dramc(mz).t_min := ref.evs(t5).lt_arr;
    }
}

DRAMC+DRAM

module dramc_mod(m) = {

    individual rd_fair : bool
    individual wr_fair : bool

    individual t_min : tar_clock

    after init {
    rd_fair       := false;
    wr_fair       := false;
    }

    action step_rd = { # a:addr_type
        var ordpip : bool;

        rd_fair := true;
        rd_fair := false;

    if some t:lclock,p:proc,a:addr_type. (isd.rd(p,m,a,t) & ref.evs(t).req=read | isd.wr(p,m,a,t) & ref.evs(t).req=write) & ref.evs(t).l_req=dramc_l minimizing ref.evs(t).lt_arr {
        ordpip := ref.evs(t).req=write;

        if ~ordpip {
        isd.rsp(p,m,a,t)  := true;

        call ref.perform_grd(t);

                assert ~ref.prevents(T,t);

        ref.evs(t).l_cmp := memc_l;
        }
    };

    if some tt:lclock,pp:proc,aa:addr_type. (isd.wr(pp,m,aa,tt) & ref.evs(tt).req=write | isd.rd(pp,m,aa,tt) & ref.evs(tt).req=read) & ref.evs(tt).l_req=dramc_l minimizing ref.evs(tt).lt_arr {
        dramc_next := tt;
        t_min := ref.evs(tt).lt_arr;
    }
        update_witnesses;
    memc_update_witnesses;
    }

    action step_wr = { # a:addr_type
        var ordpip : bool;

        wr_fair := true;
        wr_fair := false;

    if some t:lclock,p:proc,a:addr_type. (isd.wr(p,m,a,t) & ref.evs(t).req=write | isd.rd(p,m,a,t) & ref.evs(t).req=read) & ref.evs(t).l_req=dramc_l minimizing ref.evs(t).lt_arr {

            ordpip := ref.evs(t).req=read;

        if ~ordpip {

WITNESS assert false;

        call ref.perform_grd(t);

        ref.evs(t).l_cmp := memc_l;

                assert ~ref.prevents(T,t);
        }
    };

    if some tt:lclock,pp:proc,aa:addr_type. (isd.wr(pp,m,aa,tt) & ref.evs(tt).req=write | isd.rd(pp,m,aa,tt) & ref.evs(tt).req=read) & ref.evs(tt).l_req=dramc_l minimizing ref.evs(tt).lt_arr {
        dramc_next := tt;
        t_min := ref.evs(tt).lt_arr;
    }
        update_witnesses;
    memc_update_witnesses;
    }
}

Section

instantiate

instantiate arm          : arm_mod

instantiate memc(M:mem_type) : memc_mod(M)

instantiate dramc(M:mem_type)      : dramc_mod(M)

invariant cfabric.t_rd_arr_min=Tarr & ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l -> exists T. ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l & ref.evs(T).lt_arr_cf=cfabric.t_rd_arr_min

invariant ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l & ref.evs(T).mem_loc=mem_memc & T=ref.lt -> ref.evs(T).lt_arr_cf=ref.lt_tar_cf

invariant ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l & ref.evs(T).mem_loc=mem_memc -> ref.evs(T).lt_arr_cf~=0
invariant ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l & ref.evs(T).mem_loc=mem_memc -> ref.evs(T).lt_arr_cf<=ref.lt_tar_cf

invariant ref.evs(T).cmp=rrsp & ref.evs(T).mem_loc=mem_memc -> ref.evs(T).lt_arr_cf<=ref.lt_tar_cf

invariant ref.evs(T).lt_arr_cf <= ref.lt_tar_cf

invariant (ref.evs(T).req=read & (ref.evs(T).l_req=memc_l | ref.evs(T).l_req=dramc_l) | ref.evs(T).cmp=rrsp) & ref.evs(T).mem_loc=mem_memc
           ->
       ref.evs(T).lt_arr_cf< cfabric.t_rd_arr_min

invariant (
           ref.evs(T0).req=read & ref.evs(T0).l_req=cf_mem_l & ref.evs(T0).mem_loc=mem_memc &
           ref.evs(T1).req=read & ref.evs(T1).l_req=cf_mem_l & ref.evs(T1).mem_loc=mem_memc &
       T0<T1
      )
      ->
      ref.evs(T0).lt_arr_cf<ref.evs(T1).lt_arr_cf

invariant (ref.lt=T & ~(T=0)) -> ~(ref.evs(T).req=nop & ref.evs(T).cmp=nop)

invariant (ref.lt<T | T=0) -> ref.evs(T).lt_arr=0 & ref.evs(T).lt_arr_cf=0
invariant ref.lt=0         -> ref.lt_tar_cf=0

invariant ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l & ref.evs(T).mem_loc=mem_memc -> cfabric.t_rd_arr_min<=ref.evs(T).lt_arr_cf

invariant (forall T. ~(ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l)) -> (ref.lt_tar_cf<cfabric.t_rd_arr_min | cfabric.t_rd_arr_min=0)

invariant (forall T. (ref.evs(T).req=nop & ref.evs(T).cmp=nop)) -> cfabric.t_rd_arr_min=0

invariant (ref.evs(T).req=nop & ref.evs(T).cmp=nop | ref.evs(T).req=write |  ref.evs(T).cmp=wr_cmp | (ref.evs(T).req=read | ref.evs(T).cmp=rrsp) & ~(ref.evs(T).mem_loc=mem_memc))
           ->
       ref.evs(T).lt_arr_cf=0

invariant (
           ref.evs(T0).req=read & ref.evs(T0).l_req=cf_mem_l & ref.evs(T0).mem_loc=mem_memc &
           (
             ref.evs(T1).req=write |
             ref.evs(T1).req=read & ~(ref.evs(T1).mem_loc=mem_memc) |
             ref.evs(T1).req=nop
          )
         )
         ->
         ~(ref.evs(T1).lt_arr_cf=cfabric.t_rd_arr_min)

invariant ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l & ref.evs(T).mem_loc=mem_memc -> ~(T<cfabric.t_rd_min)

invariant cfabric.t_rd_min<T -> ((ref.evs(T).cmp=nop | ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp & ~(ref.evs(T).mem_loc=mem_memc)) & (ref.evs(T).req=read & ref.evs(T).mem_loc=mem_memc -> ref.evs(T).l_req=cf_mem_l))

invariant (forall T. ~(ref.evs(T).req=read & ref.evs(T).l_req=cf_mem_l)) -> (ref.lt<cfabric.t_rd_min | cfabric.t_rd_min=0)

invariant (forall T. (ref.evs(T).req=nop & ref.evs(T).cmp=nop)) -> cfabric.t_rd_min=0

invariant (ref.evs(T).req=write | ref.evs(T).req=read | ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp) -> ~(cfabric.t_rd_min=0)
invariant ref.evs(T).req=write & (ref.evs(T).l_req=cf_mem_l | ref.evs(T).l_req=cf_pio_l)  -> (T~=cfabric.t_rd_min)

invariant (
           ref.evs(T0).req=read & ref.evs(T0).l_req=cf_mem_l & ref.evs(T0).mem_loc=mem_memc &
           (
             ref.evs(T1).req=write |
             ref.evs(T1).req=read & ~(ref.evs(T1).mem_loc=mem_memc & ref.evs(T1).l_req=cf_mem_l) |
             ref.evs(T1).req=nop
          )
         )
         ->
         ~(T1=cfabric.t_rd_min)

invariant ref.evs(0).req=nop & ref.evs(0).l_req=init_l & ref.evs(0).cmp=nop & ref.evs(0).l_cmp=init_l & ref.evs(0).lt_arr=0 & ref.evs(0).lt_arr_cf=0

invariant (ref.evs(T).req=write | ref.evs(T).req=read | ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp) & ref.evs(T).mem_loc=pio_memc
           ->
          ref.evs(T).lt_arr=0

invariant (ref.evs(T).req=write | ref.evs(T).req=read) & ref.evs(T).m=M & ref.evs(T).a=A & ref.evs(T).l_req=dramc_l
           ->
            ~(ref.evs(T).lt_arr=0)

invariant (ref.evs(T).req=write | ref.evs(T).req=read) & ref.evs(T).m=M & ref.evs(T).a=A & ~(ref.evs(T).l_req=dramc_l)
           ->
           ref.evs(T).lt_arr=0

If there is any request in dramc(M), then dramc(M).t_min is the minimum arrival time in dramc(M)

        invariant
        ((ref.evs(T0).req=write | ref.evs(T0).req=read) & ref.evs(T0).l_req=dramc_l) & ref.evs(T0).m = M
        ->
        ref.evs(T0).lt_arr >= dramc(M).t_min

If there is any request in dramc(M), the dramc_next has the minimum arrival time in dramc for its memory. This means dramc_next is ready to read or write.

        invariant
        ((ref.evs(T0).req=write | ref.evs(T0).req=read) & ref.evs(T0).l_req=dramc_l)
        ->
        (ref.evs(dramc_next).req=write | ref.evs(dramc_next).req=read)
        & ref.evs(dramc_next).l_req=dramc_l
        & ref.evs(dramc_next).lt_arr = dramc(ref.evs(dramc_next).m).t_min


        invariant
        (ref.evs(T0).req=write | ref.evs(T0).req=read) & (ref.evs(T0).l_req=dramc_l)
        -> dramc_lt_min <= T0
        & (ref.evs(dramc_lt_min).req=write | ref.evs(dramc_lt_min).req=read) & ref.evs(dramc_lt_min).l_req=dramc_l
        & (ref.evs(dramc_next).req=write | ref.evs(dramc_next).req=read) & ref.evs(dramc_next).l_req=dramc_l
        & dramc(ref.evs(dramc_lt_min).m).t_min = ref.evs(dramc_next).lt_arr
        & ref.evs(dramc_lt_min).m = ref.evs(dramc_next).m

        invariant
        (ref.evs(T0).req=write | ref.evs(T0).req=read) & (ref.evs(T0).l_req=memc_l)
        -> memc_lt_min <= T0
        & (ref.evs(memc_lt_min).req=write | ref.evs(memc_lt_min).req=read) & ref.evs(memc_lt_min).l_req=memc_l

        invariant
        (ref.evs(T0).req=write | ref.evs(T0).req=read) & (ref.evs(T0).l_req=memc_l)
        & (ref.evs(T1).req=write | ref.evs(T1).req=read) & (ref.evs(T1).l_req=dramc_l)  & ref.evs(T1).m = ref.evs(memc_lt_min).m
        ->
        (ref.evs(memc_next).req=write | ref.evs(memc_next).req=read) & ref.evs(memc_next).l_req=dramc_l
        & dramc(ref.evs(memc_lt_min).m).t_min = ref.evs(memc_next).lt_arr
        & ref.evs(memc_lt_min).m = ref.evs(memc_next).m

        invariant
        (ref.evs(T0).req=write | ref.evs(T0).req=read) & (ref.evs(T0).l_req=dramc_l)
        & ref.evs(T0).m = ref.evs(memc_lt_min).m
        & ref.evs(T0).a = ref.evs(memc_lt_min).a
        & ref.evs(T0).req = ref.evs(memc_lt_min).req
        ->
        (ref.evs(memc_blocking).req=write | ref.evs(memc_blocking).req=read) & (ref.evs(memc_blocking).l_req=dramc_l)
        & ref.evs(memc_blocking).m = ref.evs(memc_lt_min).m
        & ref.evs(memc_blocking).a = ref.evs(memc_lt_min).a
        & ref.evs(memc_blocking).req = ref.evs(memc_lt_min).req

invariant ref.evs(T).req=read  -> ref.evs(T).l_cmp=init_l
invariant ref.evs(T).req=write -> ref.evs(T).l_cmp=init_l

invariant  ref.evs(T).req=nop -> ref.evs(T).l_req=init_l

invariant (ref.evs(T).req=read | ref.evs(T).req=write | ref.evs(T).req=nop)
invariant (ref.evs(T).cmp=rrsp | ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=nop)

invariant ref.evs(T).req~=nop -> ref.evs(T).cmp=nop
invariant ref.evs(T).cmp~=nop -> ref.evs(T).req=nop

invariant (forall P,M,A. ~(isd.wr(P,M,A,T) | isd.rd(P,M,A,T))) -> (ref.evs(T).l_req=init_l & ref.evs(T).l_cmp=init_l)

invariant ((ref.evs(T).req=write | ref.evs(T).req=read) & ref.evs(T).mem_loc=mem_memc & ref.evs(T).l_req=dramc_l)
       ->
       ~(ref.lt_tar(ref.evs(T).m)<ref.evs(T).lt_arr)

invariant ((ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp) & ref.evs(T).mem_loc=mem_memc)
       ->
       ref.evs(T).lt_arr<ref.evs(T).lt_tar

invariant (
            (ref.evs(T0).req=write & ref.evs(T0).l_req=dramc_l | ref.evs(T0).req=read & ref.evs(T0).l_req=dramc_l) & ref.evs(T0).mem_loc=mem_memc &
            (ref.evs(T1).cmp=wr_cmp | ref.evs(T1).cmp=rrsp) & ref.evs(T1).mem_loc=mem_memc & ref.evs(T1).l_cmp=dramc_l &
        ref.evs(T0).m=ref.evs(T1).m &
        T0~=T1
       )
       ->
       (ref.evs(T0).lt_arr~=ref.evs(T1).lt_tar & ref.evs(T0).lt_arr~=ref.evs(T1).lt_arr)

invariant (
            (ref.evs(T0).req=write & ref.evs(T0).l_req=dramc_l | ref.evs(T0).cmp=wr_cmp | ref.evs(T0).req=read & ref.evs(T0).l_req=dramc_l | ref.evs(T0).cmp=rrsp) & ref.evs(T0).mem_loc=mem_memc &
            (ref.evs(T1).req=write & ref.evs(T1).l_req=dramc_l | ref.evs(T1).cmp=wr_cmp & ref.evs(T1).l_cmp=dramc_l | ref.evs(T1).req=read & ref.evs(T1).l_req=dramc_l | ref.evs(T1).cmp=rrsp & ref.evs(T1).l_cmp=dramc_l) & ref.evs(T1).mem_loc=mem_memc &
        ref.evs(T0).m=ref.evs(T1).m &
        T0~=T1
       )
       ->
       (
        ref.evs(T0).lt_arr~=ref.evs(T1).lt_arr &
        ((ref.evs(T0).cmp=wr_cmp | ref.evs(T0).cmp=rrsp) -> ref.evs(T0).lt_tar~=ref.evs(T1).lt_arr) &
        ((ref.evs(T1).cmp=wr_cmp | ref.evs(T1).cmp=rrsp) -> ref.evs(T0).lt_arr~=ref.evs(T1).lt_tar)
       )

invariant (
            (ref.evs(T0).cmp=wr_cmp | ref.evs(T0).cmp=rrsp) & ref.evs(T0).mem_loc=mem_memc &
            (ref.evs(T1).cmp=wr_cmp | ref.evs(T1).cmp=rrsp) & ref.evs(T1).mem_loc=mem_memc &
        ref.evs(T0).m=ref.evs(T1).m &
        T0~=T1
       )
       ->
       (ref.evs(T0).lt_arr~=ref.evs(T1).lt_arr & ref.evs(T0).lt_tar~=ref.evs(T1).lt_tar)

invariant ~(
            ref.evs(T0).req=write & ref.evs(T1).cmp=rrsp &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
        ref.evs(T0).m=ref.evs(T1).m &
        ref.evs(T0).a=ref.evs(T1).a &
        ref.evs(T0).l_req=dramc_l &
        (ref.evs(T0).lt_arr<ref.evs(T1).lt_arr)
        )

invariant (
            ref.evs(T0).req=read & ref.evs(T1).cmp=rrsp &
        ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
        ref.evs(T0).m=ref.evs(T1).m &
        ref.evs(T0).a=ref.evs(T1).a &
        ref.same_attr(T0,T1) &
        T0<T1
        )
        ->
        (ref.evs(T0).lt_arr<ref.evs(T1).lt_arr)

No RR or WW to same address in mem_memc from arm (normal)

invariant ~(
            (ref.evs(T0).req=read & ref.evs(T1).req=read | ref.evs(T0).req=write & ref.evs(T1).req=write) &
        ref.evs(T0).op_ack=normal &
        ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
        ref.evs(T0).m=ref.evs(T1).m &
        ref.evs(T0).a=ref.evs(T1).a &
        ref.same_attr(T0,T1) &
        T0<T1
        )

RR and WW to same address in mem_memc stay in order

invariant (
            (ref.evs(T0).req=write & ref.evs(T1).req=write | ref.evs(T0).req=read & ref.evs(T1).req=read) &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
        ref.evs(T0).p=ref.evs(T1).p &
        ref.evs(T0).m=ref.evs(T1).m &
        ref.evs(T0).a=ref.evs(T1).a &
        ref.evs(T0).l_req=dramc_l & ref.evs(T1).l_req=dramc_l &
        ref.same_attr(T0,T1) &
        T0<T1
           )
       ->
       (
        (ref.evs(T0).lt_arr<ref.evs(T1).lt_arr)
       )

invariant (ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp) -> ~(ref.lt_tar(ref.evs(T).m)<ref.evs(T).lt_tar)

invariant (
            (ref.evs(T0).cmp=wr_cmp | ref.evs(T0).cmp=rrsp) &
            (ref.evs(T1).cmp=wr_cmp | ref.evs(T1).cmp=rrsp) &
            ref.evs(T0).m=ref.evs(T1).m &
        T0~=T1
           )
           ->
       (ref.evs(T0).lt_tar~=ref.evs(T1).lt_tar)

invariant (
            ref.evs(T0).cmp=wr_cmp & ref.evs(T1).cmp=rrsp &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
        ref.same_attr(T0,T1) &
            T0<T1
           )
           ->
           (
            (ref.evs(T0).lt_tar < ref.evs(T1).lt_tar)
           )

invariant (
             ref.evs(T0).req=read & ref.evs(T1).req=read &
             ref.evs(T0).p=ref.evs(T1).p &
         ref.evs(T0).mem_loc=pio_memc & ref.evs(T1).mem_loc=pio_memc &
         ref.evs(T0).m=ref.evs(T1).m &
         ref.evs(T0).a=ref.evs(T1).a &
         ref.same_attr(T0,T1) &
             T0<T1
           )
           ->
           (
            ref.evs(T0).l_req=cf_pio_l       & (ref.evs(T1).l_req=cf_pio_l) |
            ref.evs(T0).l_req=if_l       & (ref.evs(T1).l_req=if_l  | ref.evs(T1).l_req=cf_pio_l) |
            ref.evs(T0).l_req=memc_l      & (ref.evs(T1).l_req=memc_l | ref.evs(T1).l_req=if_l | ref.evs(T1).l_req=cf_pio_l)
           )

invariant ((ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp) & ref.evs(T).serialized)
           ->
       (
        ref.evs(T).mem_loc=mem_memc |
        ref.evs(T).mem_loc=pio_memc
       )

invariant ref.evs(T).req=write -> ~ref.evs(T).serialized
invariant ref.evs(T).req=read  -> ~ref.evs(T).serialized

invariant (ref.evs(T).req=nop   & ref.evs(T).cmp=wr_cmp) -> ref.evs(T).serialized

invariant ref.evs(T).serialized -> (ref.evs(T).req=nop | ref.evs(T).cmp=nop | ref.evs(T).cmp=rrsp | ref.evs(T).cmp=wr_cmp)

invariant ((ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp))
           ->
       (
        (ref.evs(T).cmp=wr_cmp | ref.evs(T).cmp=rrsp & ~ref.evs(T).serialized) & (
        ref.evs(T).mem_loc=mem_memc & (ref.evs(T).l_cmp=dramc_l | ref.evs(T).l_cmp=memc_l | ref.evs(T).l_cmp=cf_cmp_l | ref.evs(T).l_cmp=arm_l) |
            ref.evs(T).mem_loc=pio_memc & (ref.evs(T).l_cmp=memc_l | ref.evs(T).l_cmp=if_l | ref.evs(T).l_cmp=cf_cmp_l | ref.evs(T).l_cmp=arm_l)
            ) |

        ref.evs(T).serialized & (ref.evs(T).cmp=rrsp | ref.evs(T).cmp=wr_cmp) & ref.evs(T).l_cmp=init_l
       )

invariant ((ref.evs(T).req=write | ref.evs(T).req=read))
           ->
       (
        ref.evs(T).mem_loc=mem_memc & (ref.evs(T).l_req=dramc_l | ref.evs(T).l_req=memc_l | ref.evs(T).l_req=cf_mem_l) |
        ref.evs(T).mem_loc=pio_memc & (ref.evs(T).l_req=memc_l | ref.evs(T).l_req=if_l | ref.evs(T).l_req=cf_pio_l)
       )

invariant ~(
            (ref.evs(T0).req=write & ref.evs(T1).cmp=wr_cmp & ref.evs(T1).l_cmp=init_l | (ref.evs(T0).req=read | ref.evs(T0).cmp=rrsp) & ref.evs(T1).cmp=rrsp) &
        ~ref.evs(T0).serialized & ref.evs(T1).serialized &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
        ref.same_attr(T0,T1) &
            T0<T1
           )

invariant ~ref.evs(T).serialized -> ~(ref.evs(T).mem_loc=mem_loc_init)

initialized to mem_loc_init, but once used has same mapping for all agents

invariant (ref.evs(T).req=nop & ref.evs(T).cmp=nop) -> ref.evs(T).mem_loc=mem_loc_init

invariant ((ref.evs(T0).req~=nop | ref.evs(T0).cmp~=nop) & (ref.evs(T1).req~=nop | ref.evs(T1).cmp~=nop) & ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a)
           ->
       (
        ref.evs(T0).mem_loc=ref.evs(T1).mem_loc
       )

invariant ((ref.evs(T0).req~=nop | ref.evs(T0).cmp~=nop) & (ref.evs(T1).req~=nop | ref.evs(T1).cmp~=nop) & ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a)
           ->
       (
            ref.evs(T0).mem_loc=mem_memc | ref.evs(T0).mem_loc=pio_memc
       )

invariant ((ref.evs(T).req~=nop | ref.evs(T0).cmp~=nop) & ~ref.dev(T)) -> ref.evs(T).op_ack=normal

invariant ((ref.evs(T).req~=nop | ref.evs(T).cmp~=nop) & ref.dev(T)) -> ((ref.evs(T).op_ack=nGnRE | ref.evs(T).op_ack=nGnRnE) | (ref.evs(T).op_ack=_GRE | ref.evs(T).op_ack=nGRE))

invariant ~(
             ref.evs(T0).req=read & (ref.evs(T1).req=read | ref.evs(T1).cmp=rrsp) & ~ref.evs(T0).serialized & ~ref.evs(T1).serialized &
             ref.evs(T0).p=ref.evs(T1).p &
         ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
         ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a &
         ref.both_normal(T0,T1) &
             T0<T1
           )

invariant (ref.evs(T).req=nop | ref.evs(T).cmp=nop | ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp | ref.evs(T).req=read | ref.evs(T).cmp=rrsp)

invariant isd.wr(P,M,A,T)  -> T~=0
invariant isd.rd(P,M,A,T)  -> T~=0

invariant ref.evs(T).mem_loc=pio_memc -> ref.dev(T)

invariant ((isd.wr(P,M,A,T) | isd.rd(P,M,A,T)) & ref.dev(T)) -> ((ref.evs(T).op_ack=nGRE | ref.evs(T).op_ack=_GRE) | (ref.evs(T).op_ack=nGnRnE | ref.evs(T).op_ack=nGnRE))
invariant ((isd.wr(P,M,A,T) | isd.rd(P,M,A,T)) & ~ref.dev(T)) -> ref.evs(T).op_ack=normal

invariant ~(ref.pnd_or_ser_wr(P,M1,A1,T1) & isd.rd(P,M0,A0,T0) & ref.same_attr(T0,T1) & M0=M1 & A0=A1 & T0<T1)

invariant ~(ref.pnd_or_ser_rd(P,M1,A1,T1) & isd.wr(P,M0,A0,T0) & T0<T1 &  ref.dev(T0) &  ref.dev(T1) & ref.both_nGnR(T0,T1))

invariant ~(ref.pnd_or_ser_rd(P,M1,A1,T1) & isd.wr(P,M0,A0,T0) & T0<T1 &  ref.dev(T0) &  ref.dev(T1) & ref.both_nGR(T0,T1) & ref.same_addr(T0,T1))

Never >1 to Normal to/from same address

invariant ~(ref.pnd_or_ser_rd(P,M,A,T1) & isd.rd(P,M,A,T0) & T0<T1 & ~ref.dev(T0) & ~ref.dev(T1))
invariant ~(ref.pnd_or_ser_rd(P,M,A,T1) & isd.wr(P,M,A,T0) & T0<T1 & ~ref.dev(T0) & ~ref.dev(T1))
invariant ~(ref.pnd_or_ser_wr(P,M,A,T1) & isd.rd(P,M,A,T0) & T0<T1 & ~ref.dev(T0) & ~ref.dev(T1))
invariant ~(ref.pnd_or_ser_wr(P,M,A,T1) & isd.wr(P,M,A,T0) & T0<T1 & ~ref.dev(T0) & ~ref.dev(T1))

Section

ref

ref.lt keeps track of the largest value of the logical time value. Starts at value 0 and is then incremented when each write/read is issued

invariant (T=0 | ref.lt<T) -> (ref.evs(T).req=nop & ref.evs(T).cmp=nop & ref.evs(T).serialized)

invariant isd.wr(P,M,A,T)
           <->
           ((ref.evs(T).req=write & ~ref.evs(T).serialized | ref.evs(T).cmp=wr_cmp & ref.evs(T).l_cmp~=init_l & ref.evs(T).serialized) & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A)

invariant (isd.rd(P,M,A,T) & ~isd.rsp(P,M,A,T))
           <->
           (ref.evs(T).req=read & ~ref.evs(T).serialized & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A)

invariant (isd.rd(P,M,A,T) & isd.rsp(P,M,A,T))
           <->
           (ref.evs(T).cmp=rrsp & ~ref.evs(T).serialized & ref.evs(T).p=P & ref.evs(T).m=M & ref.evs(T).a=A)

invariant ref.evs(T).req=read ->  ~ref.evs(T).serialized

invariant (ref.evs(T).cmp=rrsp & ~ref.evs(T).serialized) -> ref.evs(T).l_cmp ~= dramc_l

Section

arm

invariant ((ref.evs(T).req=read | ref.evs(T).cmp=rrsp) & ref.dev(T))  -> (ref.evs(T).op_ack=nGnRnE | ref.evs(T).op_ack=nGnRE | ref.evs(T).op_ack=nGRE | ref.evs(T).op_ack=_GRE)
invariant ((ref.evs(T).req=read | ref.evs(T).cmp=rrsp) & ~ref.dev(T)) -> ref.evs(T).op_ack=normal

invariant ((ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp) & ref.dev(T)) -> (ref.evs(T).op_ack=nGnRnE | ref.evs(T).op_ack=nGnRE | ref.evs(T).op_ack=nGRE | ref.evs(T).op_ack=_GRE)
invariant ((ref.evs(T).req=write | ref.evs(T).cmp=wr_cmp) & ~ref.dev(T)) -> ref.evs(T).op_ack=normal

PIO writes (to same address) can be pipelined and stay in order

invariant (
            (ref.evs(T0).req=write | ref.evs(T0).cmp=wr_cmp) &
            (ref.evs(T1).req=write | ref.evs(T1).cmp=wr_cmp) &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            ref.same_attr(T0,T1) &
            T0<T1
           )
           ->
           ~(ref.evs(T1).serialized & ~ref.evs(T0).serialized)

invariant (
            (ref.evs(T0).req=write & ref.evs(T1).req=write | ref.evs(T0).req=read & ref.evs(T1).req=read) &
        ~ref.evs(T0).serialized &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
            T0<T1
           )
           ->
           (
            ref.evs(T0).l_req=cf_mem_l  & ref.evs(T1).l_req=cf_mem_l   |
            ref.evs(T0).l_req=memc_l & (ref.evs(T1).l_req=memc_l | ref.evs(T1).l_req=cf_mem_l) |
            ref.evs(T0).l_req=dramc_l  & (ref.evs(T1).l_req=dramc_l  | ref.evs(T1).l_req=memc_l | ref.evs(T1).l_req=cf_mem_l)
           )

invariant ~(
            ((ref.evs(T0).req=read | ref.evs(T0).cmp=rrsp) & (ref.evs(T1).req=write | ref.evs(T1).cmp=wr_cmp)) &
        ~ref.evs(T0).serialized &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            ref.evs(T0).mem_loc=pio_memc & ref.evs(T1).mem_loc=pio_memc &
            T0<T1
           )

invariant ~(
            (ref.evs(T0).req=write & (ref.evs(T1).req=read | ref.evs(T1).cmp=rrsp)) &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            ref.evs(T0).mem_loc=pio_memc & ref.evs(T1).mem_loc=pio_memc &
        ref.same_attr(T0,T1) &
            T0<T1
           )

invariant (
            (ref.evs(T0).req=write & ref.evs(T1).req=write | ref.evs(T0).req=read & ref.evs(T1).req=read) &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            ref.evs(T0).mem_loc=pio_memc & ref.evs(T1).mem_loc=pio_memc &
            T0<T1
           )
           ->
           (
            ref.evs(T0).l_req=cf_pio_l  & ref.evs(T1).l_req=cf_pio_l |
            ref.evs(T0).l_req=if_l  & (ref.evs(T1).l_req=if_l | ref.evs(T1).l_req=cf_pio_l) |
            ref.evs(T0).l_req=memc_l & (ref.evs(T1).l_req=memc_l | ref.evs(T1).l_req=if_l | ref.evs(T1).l_req=cf_pio_l)
           )

dramc_mod

invariant (ref.evs(T0).req=write & ref.evs(T0).l_req=dramc_l & ref.evs(T1).req=write & ref.evs(T1).l_req=dramc_l & ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a) -> T0=T1
invariant (ref.evs(T0).req=read  & ref.evs(T0).l_req=dramc_l & ref.evs(T1).req=read & ref.evs(T1).l_req=dramc_l & ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a) -> T0=T1

RAR

invariant (
            ref.evs(T0).req=read & ~ref.evs(T0).serialized &
            ref.evs(T1).req=read &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            T0<T1
           )
           ->
           (
            ref.evs(T1).req=read & ref.evs(T1).l_req=cf_mem_l  & ref.evs(T0).req=read & (ref.evs(T0).l_req=cf_mem_l | ref.evs(T0).l_req=memc_l | ref.evs(T0).l_req=dramc_l) |
            ref.evs(T1).req=read & ref.evs(T1).l_req=memc_l & ref.evs(T0).req=read & (ref.evs(T0).l_req=memc_l | ref.evs(T0).l_req=dramc_l) |
            ref.evs(T1).req=read & ref.evs(T1).l_req=dramc_l  & ref.evs(T0).req=read & ref.evs(T0).l_req=dramc_l
           )

WAW

invariant (
            ref.evs(T0).req=write & ~ref.evs(T0).serialized &
            ref.evs(T1).req=write &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
            T0<T1
           )
           ->
           (
        ref.evs(T0).l_req=cf_mem_l  & ref.evs(T1).l_req=cf_mem_l |
        ref.evs(T0).l_req=memc_l & (ref.evs(T1).l_req=memc_l | ref.evs(T1).l_req=cf_mem_l) |
        ref.evs(T0).l_req=dramc_l  & (ref.evs(T1).l_req=dramc_l  | ref.evs(T1).l_req=memc_l | ref.evs(T1).l_req=cf_mem_l)
           )

RAR

invariant (
            ref.evs(T0).req=read & ~ref.evs(T0).serialized &
            ref.evs(T1).cmp=rrsp &
            ref.evs(T0).p=ref.evs(T1).p &
            ref.evs(T0).mem_loc=mem_memc & ref.evs(T1).mem_loc=mem_memc &
            ref.evs(T0).m=ref.evs(T1).m &
            ref.evs(T0).a=ref.evs(T1).a &
        ref.same_attr(T0,T1) &
            T0<T1
           )
           ->
           (
        ref.evs(T0).l_req=dramc_l & (ref.evs(T1).l_cmp=dramc_l | ref.evs(T1).l_cmp=memc_l | ref.evs(T1).l_cmp=cf_mem_l | ref.evs(T1).l_cmp=arm_l)
           )

RAR/WAW

RR to mem_memc is OrdSer for arm

invariant ~(
             ref.evs(T0).req=read & ref.evs(T1).cmp=rrsp &
             ref.evs(T0).p=ref.evs(T1).p &
         ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a &
         ref.same_attr(T0,T1) &
             T0<T1
           )

WW to same address stay in order, and therefore can't have wr_cmp for younger before older

invariant ~(
             ref.evs(T0).req=write & ref.evs(T0).cmp=nop & ref.evs(T1).req=nop & ref.evs(T1).cmp=wr_cmp &
             ref.evs(T0).p=ref.evs(T1).p &
         ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a &
         ref.same_attr(T0,T1) &
             T0<T1
           )

invariant (
            (ref.evs(T0).req=read | ref.evs(T0).cmp=rrsp) & ref.pio(T0) &
            (ref.evs(T1).req=read | ref.evs(T1).cmp=rrsp) & ref.pio(T1) &
             ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a &
             ref.evs(T0).p=ref.evs(T1).p &
         ref.same_attr(T0,T1) &
             T0<T1
           )
           ->
           ~(~ref.evs(T0).serialized & ref.evs(T1).serialized)

invariant (
            (ref.evs(T0).req=read | ref.evs(T0).cmp=rrsp) &
            (ref.evs(T1).req=read | ref.evs(T1).cmp=rrsp) &
             ref.evs(T0).m=ref.evs(T1).m & ref.evs(T0).a=ref.evs(T1).a &
             ref.evs(T0).p=ref.evs(T1).p &
         ref.same_attr(T0,T1) &
             T0<T1
           )
           ->
           ~(~ref.evs(T0).serialized & ref.evs(T1).serialized)

export arm.step_north
export arm.step_south
export cfabric.step
export ifabric.step
export memc.step
export dramc.step_wr
export dramc.step_rd

Liveness proof starts here. The proof is broken down into a series of lemmas in the following order:

1) Liveness of cf. We prove in isolate cf_live that all operations eventually arrive at a memc.

2) Liveness of dramc. We prove in isolate `that all operation transferred to a dramc eventually complete and the response arrives back at the memc. This proof is done in three steps:

2a) An abstract model of dramc is proved live woth model checking (isolate abs) 2b) A refinement relation is proved between the abstract model and dramc (isolate rfn) 2c) This relation and liveness of the abstract model areused to prove liveness of dramc (isolate tprops)

3) The dramc is proved to be non-blocking. That is, it is always eventually possible for memc to transfer a new operation to dramc. This depends on the liveness property of dramc (isolate dramc_nb).

4) Using the non-blocking property of dramc, we can prove the liveness of memc. That is, every operation in memc is eventually transferred to dramc (isolate dramc_nb2).

5) We prove liveness of completions by memc, that is, a response returned by dramc to memc eventually reaches cf (isolate cmpl_live).

6) We prove that completions of pio operations eventually reach cfabric (isolate cf_pio_live). First we prove liveness of each step along the way (i.e, that requests move from cfabric to ifabric to memc and the completions occur in memc and move from memc to ifabric to cfabric). Then we connect these proofs in a seuqnce of lemmas to show that if a pio requesu reaches cfabric, the completion eventually gets back to cfabric.

7) We then prove that completions all memc operations eventually get back to cfabric by chaining together the liveness properties for memory operations of cfabric, memc and dramc (isolate dramc_nb2).

8) Putting together (6) and (7) we show that completions of all operations (pio and mem) eventually reach cfabric (lemma dramc_nb2.lemma3a). From this point the liveness proofs of pio and memc operations# merge. We show that completions of all operations get back to armc (lemma dramc_nb2.lemma4).

9) It remains to show that all operations are eventually retired from the ROB. To do this we use an abstract model of out-of-order completion with in-order retirement (isolate rfn2).

10) We connect (8) and (9) to get the end-to-end liveness statement (isolate sys_live)

Todo

give the isolates better names.

We include the file mc_schemata because this is needed for the model checker to understand the equality and total order theories.

We use these two modules to inject observable signals into the model. We can use their statevariables in temporal formulas. Notice these modules provid the invariant ~now. That is, when the signal is not being raised, the now variable is always false.

module signal0 = {
    action raise

    specification {
        relation now
        after init { now := false; }
        before raise {
            now := true;
            now := false;
        }
        invariant ~now
    }
}

This version has a value we can reference in formulas.

module signal1(data) = {
    action raise(val:data)

    specification {
        relation now
        var value : data
        after init { now := false; }
        before raise {
            value := val;
            now := true;
            now := false;
        }
        invariant ~now
    }
}

Liveness proof startes here.

We show that every issued memory operation is eventually retired, using a single instance of the 'ranking' tactic. This tactic implelents the rule lexicographic relational rankings with stable schedulers.

isolate sys_live = {

Definitions of useful predicates. These tells us what requests or completions are present where in the system.

An request T is pending somewhere in the system

    function pending(T) =
    (isd.rd(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T) |
    isd.wr(ref.evs(T).p,ref.evs(T).m,ref.evs(T).a,T))

A request T is completed, meaning its response has reached the reorder buffer in a core, but it has not been retired

    function completed(T) =
    (ref.evs(T).cmp = rrsp | ref.evs(T).cmp = wr_cmp)
    & ref.evs(T).l_cmp = arm_l

A completion of request T is queued in cfabric

    function cf_cpl(T) =
    (ref.evs(T).cmp = rrsp | ref.evs(T).cmp = wr_cmp)
    & ref.evs(T).l_cmp = cf_cmp_l

A completion of request T is queued in ifabric

    function if_cpl(T) =
    (ref.evs(T).cmp = rrsp | ref.evs(T).cmp = wr_cmp)
    & ref.evs(T).l_cmp = if_l

Request T is queued in ifabric

    function if_req(T) =
    (ref.evs(T).req = read | ref.evs(T).req = write)
    & ref.evs(T).l_req = if_l

A completion of request T is queued in memc

    function memc_cpl(T) =
    (ref.evs(T).cmp = rrsp | ref.evs(T).cmp = wr_cmp) &
    ref.evs(T).l_cmp = memc_l

Request T is queued in dramc

    function dramc_req(T) =
    (ref.evs(T).req=read | ref.evs(T).req=write)  &
    ref.evs(T).l_req=dramc_l

Request T is queued in memc

    function memc_req(T) =
    (ref.evs(T).req=read | ref.evs(T).req=write)  &
    ref.evs(T).l_req=memc_l

Request T is queued in cfabric and is a dram request

    function cf_mem_req(T) =
    (ref.evs(T).req = read | ref.evs(T).req = write)
    & ref.evs(T).l_req = cf_mem_l

Request T is queued in cfabric and is a pio request

    function cf_pio_req(T) =
    (ref.evs(T).req = read | ref.evs(T).req = write)
    & ref.evs(T).l_req = cf_pio_l

Request T is a pio request

    function is_io(T) = ref.evs(T).mem_loc=pio_memc

The following axioms are fairness constraints. They say that each queue is served infinitely often.

    explicit temporal axiom [cf_rd_fair]
        globally eventually cfabric.rd_fair

    explicit temporal axiom [cf_wr_fair]
        globally eventually cfabric.wr_fair

    explicit temporal axiom [cf_rd_pio_fair]
        globally eventually cfabric.rd_pio_fair

    explicit temporal axiom [cf_wr_pio_fair]
        globally eventually cfabric.wr_pio_fair

    explicit temporal axiom [if_rd_fair]
        forall P. globally eventually ifabric.rd_fair(P)

    explicit temporal axiom [if_wr_fair]
        forall P. globally eventually ifabric.wr_fair(P)

    explicit temporal axiom [memc_rd_fair]
        globally eventually memc.rd_fair(M,A)

    explicit temporal axiom [memc_wr_fair]
        globally eventually memc.wr_fair(M,A)

    explicit temporal axiom [dramc_rd_fair]
        globally eventually dramc(M).rd_fair

    explicit temporal axiom [dramc_wr_fair]
        globally eventually dramc(M).wr_fair

    explicit temporal axiom [memc_cpl_fair]
       forall P,M,A,T. globally eventually memc.cpl_fair(P,M,A,T)

    explicit temporal axiom [if_cpl_fair]
       forall T. globally eventually ifabric.cpl_fair(T)

    explicit temporal axiom [cf_cpl_fair]
    globally eventually cfabric.cpl_fair

    explicit temporal axiom [cpl_fair]
      forall P. globally eventually arm.cpl_fair(P)

Liveness property. Every request issued by every core is eventually retired.

    explicit temporal property [live]
    forall P,T.
        globally ref.evs(T).p=P & pending(T) -> eventually ~pending(T)
    proof {

The skolemizenp tactic replaces universal quantifiers in the goal by Herbrand symbols (without converting to premex normal form).

        tactic skolemizenp

We instantiate all of the fairness axioms

        instantiate cpl_fair with P=_P
        instantiate cf_cpl_fair
        instantiate if_cpl_fair
        instantiate memc_cpl_fair
        instantiate dramc_rd_fair
        instantiate dramc_wr_fair
        instantiate memc_rd_fair
        instantiate memc_wr_fair
        instantiate cf_rd_fair
        instantiate cf_wr_fair
        instantiate cf_rd_pio_fair
        instantiate cf_wr_pio_fair
        instantiate if_rd_fair
        instantiate if_wr_fair

Now we apply the 'ranking' tactic, which uses a lexicographic relational ranking with stable scheduler. Each component of the ranking has the following user-defined predicates:

• work_created: this is 'R' in the paper and puts a finite upper bounded on the ranking.
• work_needed: this is 'delta' in the paper, i.e., the relational ranking
• work_invar: this is 'phi' in the paper, the invariant
• work_progress: this is the justice condition 'r'
• work_helpful: this is the helpful condition 'psi'

The work_created and work_invar condtions are somewhat redundant in that they are generally the same for all ranking components (as in the rule given in the paper). The exception is the work_created condition in component rankings 6a and 6b, which is a binary relation (see comments below).

        tactic ranking with {

            definition work_created[0a](T) = T <= ref.lt
            definition work_needed[0a](T) = T <= _T & pending(T) & ~is_io(T) & cf_mem_req(T)
            definition work_invar[0a] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[0a] = cfabric.rd_fair
            definition work_helpful[0a] = exists T. work_needed[0a](T) & ref.evs(T).req = read

            definition work_created[0b](T) = T <= ref.lt
            definition work_needed[0b](T) = T <= _T & pending(T) & ~is_io(T) & cf_mem_req(T)
            definition work_invar[0b] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[0b] = cfabric.wr_fair
            definition work_helpful[0b] = exists T. work_needed[0b](T) & ref.evs(T).req = write

            definition work_created[1a](T) = T <= ref.lt
            definition work_needed[1a](T) = T <= _T & pending(T) & is_io(T) & cf_pio_req(T)
            definition work_invar[1a] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[1a] = cfabric.rd_pio_fair
            definition work_helpful[1a] = exists T. work_needed[1a](T) & ref.evs(T).req = read

            definition work_created[1b](T) = T <= ref.lt
            definition work_needed[1b](T) = T <= _T & pending(T) & is_io(T) & cf_pio_req(T)
            definition work_invar[1b] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[1b] = cfabric.wr_pio_fair
            definition work_helpful[1b] = exists T. work_needed[1b](T) & ref.evs(T).req = write


            definition work_created[4a](T) = pending(T)
            definition work_needed[4a](T) = T <= _T & pending(T) & is_io(T) & if_req(T)
            definition work_invar[4a] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[4a](P) = ifabric.rd_fair(P)
            definition work_helpful[4a](P) = exists T. work_needed[4a](T) & ref.evs(T).p = P & ref.evs(T).req = read

            definition work_created[4b](T) = pending(T)
            definition work_needed[4b](T) = T <= _T & pending(T) & is_io(T) & if_req(T)
            definition work_invar[4b] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[4b](P) = ifabric.wr_fair(P)
            definition work_helpful[4b](P) = exists T. work_needed[4b](T) & ref.evs(T).p = P & ref.evs(T).req = write

            definition work_created[5a](T) = pending(T)
            definition work_needed[5a](T) = T <= _T & pending(T) & memc_req(T)
            definition work_invar[5a] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[5a](M,A) = memc.rd_fair(M,A)
            definition work_helpful[5a](M,A,T) = work_needed[5a](T) & T = memc_lt_min & ref.evs(T).m = M & ref.evs(T).a = A & ref.evs(T).req=read
            & (~is_io(T) -> ~exists U. dramc_req(U) & ref.evs(U).m = M & ref.evs(U).a = A & ref.evs(U).req = read)

            definition work_created[5b](T) = pending(T)
            definition work_needed[5b](T) = T <= _T & pending(T) & memc_req(T)
            definition work_invar[5b] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[5b](M,A) = memc.wr_fair(M,A)
            definition work_helpful[5b](M,A,T) = work_needed[5b](T) & T = memc_lt_min & ref.evs(T).m = M & ref.evs(T).a = A & ref.evs(T).req=write
            & (~is_io(T) -> ~exists U. dramc_req(U) & ref.evs(U).m = M & ref.evs(U).a = A & ref.evs(U).req = write)

This compoment ranking measures the requests in the dramc that must be handled in order to retire request _T. This includes all request with logical times earlier than T, and also all requests the can block any of these requests. The ranking is expressed as a set of dependency arcs (T,U) such that completion of U depends on completion of T. Request U depends on T if either T and U are in the same dramc queue and T arrived before U, or there is some U' with the same address as U, such that U is in memc and U' is in dramc and T is in dramc and arrived before U'. The existential quantifier over U' is witnessed by a ghost variable memc_blocking. To achieve this with only a single witness, we restrict the ranking to consider only the least operation U in memc to be blocked (witnessed by the auxiliary variable 'memc_lt_min'). This works because removal of 'memc_lt_min' from memc causes a higher-order ranking to be reduced, allowing this ranking to be increased to account for the next 'memc_lt_min'. That is, to account for blocking of a set of queues, we need only consider the head of the one of the queues being blocked.

Notice also that the 'work_helpful' condition is parametereized by both the justice condition, M, and the ranking element (T,U) to be removed. By specifying (T,U) in the helpful condition, we void the existential quantifier in the 'reduces' predicate of premise L2, which would introduce a function cycle.

            definition work_created[6a](T,U) = T <= ref.lt & U <= ref.lt
            definition work_needed[6a](T,U) = U <= _T & (U <= memc_lt_min | ~memc_req(memc_lt_min)) & dramc_req(T) & pending(U)
            & (dramc_req(U) & ref.evs(T).lt_arr <= ref.evs(U).lt_arr
            | memc_req(U) & dramc_req(memc_blocking)
            & ref.evs(memc_blocking).m = ref.evs(U).m
            & ref.evs(memc_blocking).a = ref.evs(U).a
            & ref.evs(memc_blocking).req = ref.evs(U).req
            & ref.evs(T).lt_arr <= ref.evs(memc_blocking).lt_arr)
            & ref.evs(T).m = ref.evs(U).m
            definition work_invar[6a] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[6a](M) = dramc(M).rd_fair
            definition work_helpful[6a](M,T,U) = work_needed[6a](T,U) & ref.evs(T).m = M & ref.evs(T).lt_arr = dramc(M).t_min & ref.evs(T).req=read

            definition work_created[6b](T,U) = T <= ref.lt & U <= ref.lt
            definition work_needed[6b](T,U) = U <= _T & (U <= memc_lt_min | ~memc_req(memc_lt_min)) & dramc_req(T) & pending(U)
            & (dramc_req(U) & ref.evs(T).lt_arr <= ref.evs(U).lt_arr
            | memc_req(U) & dramc_req(memc_blocking)
            & ref.evs(memc_blocking).m = ref.evs(U).m
            & ref.evs(memc_blocking).a = ref.evs(U).a
            & ref.evs(memc_blocking).req = ref.evs(U).req
            & ref.evs(T).lt_arr <= ref.evs(memc_blocking).lt_arr)
            & ref.evs(T).m = ref.evs(U).m
            definition work_invar[6b] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[6b](M) = dramc(M).wr_fair
            definition work_helpful[6b](M,T,U) = work_needed[6b](T,U) & ref.evs(T).m = M & ref.evs(T).lt_arr = dramc(M).t_min & ref.evs(T).req=write

            definition work_created[7](T) = pending(T)
            definition work_needed[7](T) = T <= _T & pending(T) & memc_cpl(T)
            definition work_invar[7] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[7](P,M,A,T) = memc.cpl_fair(P,M,A,T)
            definition work_helpful[7](P,M,A,T) = T <= _T & memc_cpl(T) & P=ref.evs(T).p & M=ref.evs(T).m & A=ref.evs(T).a

            definition work_created[7a](T) = pending(T)
            definition work_needed[7a](T) = T <= _T & pending(T) & is_io(T) & if_cpl(T)
            definition work_invar[7a] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[7a](T) = ifabric.cpl_fair(T)
            definition work_helpful[7a](T) = T <= _T & pending(T) & is_io(T) & if_cpl(T)

            definition work_created[8](T) = pending(T)
            definition work_needed[8](T) = T <= _T & pending(T) & ~completed(T)
            definition work_invar[8] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[8] = cfabric.cpl_fair
            definition work_helpful[8] = exists T. T <= _T & cf_cpl(T)

            definition work_created[9](T) = pending(T)
            definition work_needed[9](T) = T <= _T & pending(T) & ref.evs(T).p=_P
            definition work_invar[9] = pending(_T) & ref.evs(_T).p=_P
            definition work_progress[9] = arm.cpl_fair(_P)
            definition work_helpful[9] =
              forall T. ~( T <= _T
                         & ref.evs(T).p=_P
                         & pending(T)
                         & ~completed(T))

The justice conditions are Booleans that are raised and lowered whenever a given queue is served. Thus, that are invariantly false between actions. These invariants really belong with the justice condition definitions, not here.

            invariant ~arm.cpl_fair(P)
            invariant ~cfabric.cpl_fair
            invariant ~ifabric.cpl_fair(T)
            invariant ~memc.cpl_fair(P,M,A,T)
            invariant ~dramc(M).rd_fair
            invariant ~dramc(M).wr_fair
            invariant ~memc.rd_fair(M,A)
            invariant ~memc.wr_fair(M,A)
            invariant ~cfabric.rd_fair
            invariant ~cfabric.wr_fair
            invariant ~cfabric.rd_pio_fair
            invariant ~cfabric.wr_pio_fair
            invariant ~ifabric.rd_fair(P)
            invariant ~ifabric.wr_fair(P)

This invariant says that a completion cannot be in dramc. It isn't clear why this invariant is not needed for the safety proof. Note that the ranking tactics uses all of the safety proof invariants , in addition to the invariants specified here.

            invariant ref.evs.l_cmp(X) ~= dramc_l
        }
    }

} with this, lclock, tar_clock, tar_cf_clock