mips/model/mips.sml

40     M: bool, MD: bool, MMUSize: BitsN.nbit, PC: bool, WR: bool }
621    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
623    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
627    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
629    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
633    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
635    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
639    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
641    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
645    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
647    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
651    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
653    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
657    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
659    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
663    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
665    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
669    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
671    IL = x', IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
675    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
677    IL = IL, IS = x', M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
681    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
683    IL = IL, IS = IS, M = x', MD = MD, MMUSize = MMUSize, PC = PC, WR = WR}
687    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
689    IL = IL, IS = IS, M = M, MD = x', MMUSize = MMUSize, PC = PC, WR = WR}
693    M, MD, MMUSize, PC, WR}: ConfigRegister1, x') =
695    IL = IL, IS = IS, M = M, MD = MD, MMUSize = x', PC = PC, WR = WR}
699    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
701    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = x', WR = WR}
705    MD, MMUSize, PC, WR}: ConfigRegister1, x') =
707    IL = IL, IS = IS, M = M, MD = MD, MMUSize = MMUSize, PC = PC, WR = x'}
1561        MMUSize = BitsN.B(0x0,6), PC = false, WR = false},
1613 val PC = ref (BitsN.B(0x0,64)): BitsN.nbit ref
1844    MMUSize = BitsN.bits(30,25) x, PC = BitsN.bit(x,4), WR = BitsN.bit(x,3)};
1850       PC = PC, WR = WR} =>
1853           BitsN.fromBit MD,BitsN.fromBit PC,BitsN.fromBit WR,
1994                 (BitsN.+((!PC),BitsN.B(0x4,64)),
1996       else (true,BitsN.+((!PC),BitsN.B(0x4,64)))));
2004                (BitsN.+((!PC),BitsN.B(0x4,64)),
2007     then BranchTo := (Option.SOME(true,BitsN.+((!PC),BitsN.B(0x8,64))))
2008   else PC := (BitsN.+((!PC),BitsN.B(0x4,64)));
2049                   (CP0_EPC_rupd((!CP0),BitsN.-((!PC),BitsN.B(0x4,64))))
2058               ( CP0 := (CP0_EPC_rupd((!CP0),(!PC)))
2089           ; PC :=
2402     val vAddr = (!PC)
4667              then ( PC :=
4677            else ( PC := (BitsN.-(#EPC((!CP0) : CP0),BitsN.B(0x4,64)))
4719       BitsN.concat[BitsN.bits(63,28) (!PC),instr_index,BitsN.B(0x0,2)]));
4722   ( write'GPR(BitsN.+((!PC),BitsN.B(0x8,64)),BitsN.B(0x1F,5))
4726         BitsN.concat[BitsN.bits(63,28) (!PC),instr_index,BitsN.B(0x0,2)]))
4735     ( write'GPR(BitsN.+((!PC),BitsN.B(0x8,64)),rd)
4762     ( write'GPR(BitsN.+((!PC),BitsN.B(0x8,64)),BitsN.B(0x1F,5))
4771     ( write'GPR(BitsN.+((!PC),BitsN.B(0x8,64)),BitsN.B(0x1F,5))
4798     ( write'GPR(BitsN.+((!PC),BitsN.B(0x8,64)),BitsN.B(0x1F,5))
4807     ( write'GPR(BitsN.+((!PC),BitsN.B(0x8,64)),BitsN.B(0x1F,5))
11394        (NONE,NONE) => PC := (BitsN.+((!PC),BitsN.B(0x4,64)))
11396        ( BranchDelay := (Option.SOME NONE); BranchTo := NONE; PC := addr )
11400        ; PC := (BitsN.+((!PC),BitsN.B(0x4,64)))
11403        ( BranchDelay := NONE; PC := (BitsN.+((!PC),BitsN.B(0x4,64))) )
11405        ( BranchDelay := NONE; PC := addr )