riscv/model/riscv.sml

2218 fun PC () = Map.lookup((!c_PC),BitsN.toNat (!procID));
2220 fun write'PC value =
3671          ; write'PC(#stvec((SCSR ()) : SupervisorCSR))
3701          ; write'PC
4630       (BitsN.+(PC (),BitsN.signExtend 64 (BitsN.@@(imm,BitsN.B(0x0,12)))),
4640                  (PC (),
5280     val addr = BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 imm,1))
5284     else ( ( write'GPR(BitsN.+(PC (),BitsN.B(0x4,64)),rd)
5290                     (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5306     else ( ( write'GPR(BitsN.+(PC (),BitsN.B(0x4,64)),rd)
5312                     (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5331       then branchTo(BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 offs,1)))
5337                 (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5353       then branchTo(BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 offs,1)))
5359                 (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5375       then branchTo(BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 offs,1)))
5381                 (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5397       then branchTo(BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 offs,1)))
5403                 (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5419       then branchTo(BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 offs,1)))
5425                 (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
5441       then branchTo(BitsN.+(PC (),BitsN.<<(BitsN.signExtend 64 offs,1)))
5447                 (x,Option.SOME(BitsN.+(PC (),BitsN.B(0x4,64)))))
8314     val vPC = PC ()
14446      " 0x",hex64(PC ())," : ",hex32 w,"   ",instructionToString inst];
14528          ( incrInstret (); write'PC(BitsN.+(PC (),BitsN.B(0x4,64))) )
14533             (interruptIndex i,(BitsN.+(PC (),BitsN.B(0x4,64)),(NONE,p))))
14536        ( incrInstret (); write'NextFetch NONE; write'PC addr )
14540        ; write'PC(curEPC ())
14570              (PC (),(#badaddr(t : SynchronousTrap),Machine))))
14575        ; write'PC(#stvec((SCSR ()) : SupervisorCSR))
14702   ; write'PC(BitsN.fromNat(pc,64))