Add checks for CR Move / Set Boolean instructions.

main
Jean-François Nguyen 2 years ago
parent b579665d7a
commit 7b7aa6cc9b

@ -1,20 +1,35 @@
from power_fv.insn import const
from power_fv.insn.spec.cr import CRSpec
from power_fv.insn.spec.cr import CRLogicalSpec, CRMoveSpec
from power_fv.check.insn import InsnCheck


__all__ = [
"CRAND", "CROR", "CRNAND", "CRXOR", "CRNOR", "CRANDC", "CREQV", "CRORC",
"MCRF" ,
"MCRF", "MCRXRX", "MTCRF", "MFOCRF", "MFCR",
"SETB", #"SETBC", "SETBCR", "SETNBC", "SETNBCR",
]


class CRAND (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRAND ): pass
class CROR (InsnCheck, spec_cls=CRSpec, insn_cls=const.CROR ): pass
class CRNAND (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRNAND): pass
class CRXOR (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRXOR ): pass
class CRNOR (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRNOR ): pass
class CRANDC (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRANDC): pass
class CREQV (InsnCheck, spec_cls=CRSpec, insn_cls=const.CREQV ): pass
class CRORC (InsnCheck, spec_cls=CRSpec, insn_cls=const.CRORC ): pass
class MCRF (InsnCheck, spec_cls=CRSpec, insn_cls=const.MCRF ): pass
class CRAND (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRAND ): pass
class CROR (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CROR ): pass
class CRNAND (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRNAND): pass
class CRXOR (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRXOR ): pass
class CRNOR (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRNOR ): pass
class CRANDC (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRANDC): pass
class CREQV (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CREQV ): pass
class CRORC (InsnCheck, spec_cls=CRLogicalSpec, insn_cls=const.CRORC ): pass

class MCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MCRF ): pass
class MCRXRX (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MCRXRX): pass
class MTOCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MTOCRF): pass
class MTCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MTCRF ): pass
class MFOCRF (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MFOCRF): pass
class MFCR (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.MFCR ): pass

class SETB (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETB ): pass

# TODO: add a --exclude= argument to the 'check' command
# class SETBC (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETBC ): pass
# class SETBCR (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETBCR ): pass
# class SETNBC (InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETNBC ): pass
# class SETNBCR(InsnCheck, spec_cls=CRMoveSpec, insn_cls=const.SETNBCR): pass

@ -36,7 +36,19 @@ class CRNOR (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(
class CRANDC (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(129))
class CREQV (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(289))
class CRORC (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(417))
class MCRF (WordInsn): _fields = (f.PO(19), f.BF(), f.BFA(), f.XO_XL( 0))

class MCRF (WordInsn): _fields = (f.PO(19), f.BF(), f.BFA(), f.XO_XL ( 0))
class MCRXRX (WordInsn): _fields = (f.PO(31), f.BF(), f.XO_X (576))
class MTOCRF (WordInsn): _fields = (f.PO(31), f.RS(), f.XFX_11(1), f.FXM(), f.XO_XFX(144))
class MTCRF (WordInsn): _fields = (f.PO(31), f.RS(), f.XFX_11(0), f.FXM(), f.XO_XFX(144))
class MFOCRF (WordInsn): _fields = (f.PO(31), f.RT(), f.XFX_11(1), f.FXM(), f.XO_XFX( 19))
class MFCR (WordInsn): _fields = (f.PO(31), f.RT(), f.XFX_11(0), f.XO_XFX( 19))

class SETB (WordInsn): _fields = (f.PO(31), f.RT(), f.BFA(), f.XO_X(128))
class SETBC (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(384))
class SETBCR (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(416))
class SETNBC (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(448))
class SETNBCR (WordInsn): _fields = (f.PO(31), f.RT(), f.BI(), f.XO_X(480))

# Load


@ -18,6 +18,7 @@ class D (InsnField): _shape = signed(16); _offset = 16; _name = "D"
class d0 (InsnField): _shape = signed(10); _offset = 16; _name = "d0"
class d1 (InsnField): _shape = signed( 5); _offset = 11; _name = "d1"
class d2 (InsnField): _shape = signed( 1); _offset = 31; _name = "d2"
class FXM (InsnField): _shape = unsigned( 8); _offset = 12; _name = "FXM"
class LEV (InsnField): _shape = unsigned( 7); _offset = 20; _name = "LEV"
class L_D10 (InsnField): _shape = unsigned( 1); _offset = 10; _name = "L"
class L_X10 (InsnField): _shape = unsigned( 1); _offset = 10; _name = "L"
@ -39,6 +40,7 @@ class SI (InsnField): _shape = signed(16); _offset = 16; _name = "SI"
class SH (InsnField): _shape = unsigned( 5); _offset = 16; _name = "SH"
class TO (InsnField): _shape = unsigned( 5); _offset = 6; _name = "TO"
class UI (InsnField): _shape = unsigned(16); _offset = 16; _name = "UI"
class XFX_11(InsnField): _shape = unsigned( 1); _offset = 11; _name = "_11"
class XO (InsnField): _shape = unsigned( 9); _offset = 22; _name = "XO"
class XO_DX (InsnField): _shape = unsigned( 5); _offset = 26; _name = "XO"
class XO_X (InsnField): _shape = unsigned(10); _offset = 21; _name = "XO"

@ -1,16 +1,19 @@
from amaranth import *
from amaranth.asserts import Assume
from amaranth.lib.coding import Encoder

from power_fv import pfv
from power_fv.insn.const import *
from power_fv.build.sby import SymbiYosysPlatform

from . import InsnSpec
from .utils import iea


__all__ = ["CRSpec"]
__all__ = ["CRLogicalSpec", "CRMoveSpec"]


class CRSpec(InsnSpec, Elaboratable):
class CRLogicalSpec(InsnSpec, Elaboratable):
def __init__(self, insn):
self.pfv = pfv.Interface()
self.insn = insn
@ -35,11 +38,11 @@ class CRSpec(InsnSpec, Elaboratable):
result = Signal()

m.d.comb += [
self.pfv.cr.r_mask[::-1].bit_select(self.insn.BA, width=1).eq(1),
self.pfv.cr.r_mask[::-1].bit_select(self.insn.BB, width=1).eq(1),
self.pfv.cr.r_mask.bit_select(31-self.insn.BA, width=1).eq(1),
self.pfv.cr.r_mask.bit_select(31-self.insn.BB, width=1).eq(1),

src_a.eq(self.pfv.cr.r_data[::-1].bit_select(self.insn.BA, width=1)),
src_b.eq(self.pfv.cr.r_data[::-1].bit_select(self.insn.BB, width=1)),
src_a.eq(self.pfv.cr.r_data.bit_select(31-self.insn.BA, width=1)),
src_b.eq(self.pfv.cr.r_data.bit_select(31-self.insn.BB, width=1)),
]

if isinstance(self.insn, CRAND):
@ -60,21 +63,146 @@ class CRSpec(InsnSpec, Elaboratable):
m.d.comb += result.eq(src_a | ~src_b)

m.d.comb += [
self.pfv.cr.w_mask[::-1].bit_select(self.insn.BT, width=1).eq(1),
self.pfv.cr.w_data[::-1].bit_select(self.insn.BT, width=1).eq(result),
self.pfv.cr.w_mask.bit_select(31-self.insn.BT, width=1).eq(1),
self.pfv.cr.w_data.bit_select(31-self.insn.BT, width=1).eq(result),
]

elif isinstance(self.insn, MCRF):
field = Signal(4)
else:
assert False

return m


class CRMoveSpec(InsnSpec, Elaboratable):
def __init__(self, insn):
self.pfv = pfv.Interface()
self.insn = insn

def elaborate(self, platform):
m = Module()

m.d.comb += [
self.pfv.stb .eq(1),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())),
self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1),
]

if isinstance(self.insn, MCRF):
crf = Signal(4)
m.d.comb += [
field.eq(self.pfv.cr.r_data[::-1].word_select(self.insn.BFA, width=4)),
self.pfv.cr.r_mask.word_select(7-self.insn.BFA, width=4).eq(0xf),
crf.eq(self.pfv.cr.r_data.word_select(7-self.insn.BFA, width=4)),

self.pfv.cr.w_mask.word_select(7-self.insn.BF, width=4).eq(0xf),
self.pfv.cr.w_data.word_select(7-self.insn.BF, width=4).eq(crf),
]

elif isinstance(self.insn, MCRXRX):
crf = Record([("ca32", 1), ("ca", 1), ("ov32", 1), ("ov", 1)])

self.pfv.cr.r_mask[::-1].word_select(self.insn.BFA, width=4).eq(0b1111),
self.pfv.cr.w_mask[::-1].word_select(self.insn.BF, width=4).eq(0b1111),
self.pfv.cr.w_data[::-1].word_select(self.insn.BF, width=4).eq(field),
m.d.comb += [
self.pfv.xer.r_mask.ov .eq(1),
self.pfv.xer.r_mask.ov32.eq(1),
self.pfv.xer.r_mask.ca .eq(1),
self.pfv.xer.r_mask.ca32.eq(1),

crf.ov .eq(self.pfv.xer.r_data.ov),
crf.ov32.eq(self.pfv.xer.r_data.ov32),
crf.ca .eq(self.pfv.xer.r_data.ca),
crf.ca32.eq(self.pfv.xer.r_data.ca32),

self.pfv.cr.w_mask.word_select(7-self.insn.BF, width=4).eq(0xf),
self.pfv.cr.w_data.word_select(7-self.insn.BF, width=4).eq(crf),
]

elif isinstance(self.insn, MTOCRF):
crf = Signal(4)

m.submodules.fxm_enc = fxm_enc = Encoder(width=8)
m.d.comb += [
fxm_enc.i.eq(self.insn.FXM),

self.pfv.rs.index.eq(self.insn.RS),
self.pfv.rs.r_stb.eq(1),
crf.eq(self.pfv.rs.r_data.word_select(fxm_enc.o, width=4)),

self.pfv.cr.w_mask.word_select(fxm_enc.o, width=4).eq(0xf),
self.pfv.cr.w_data.word_select(fxm_enc.o, width=4).eq(crf),
]

# Unless exactly one FXM bit is set to 1, CR contents are undefined.
if isinstance(platform, SymbiYosysPlatform):
m.d.comb += Assume(~fxm_enc.n)

elif isinstance(self.insn, MTCRF):
m.d.comb += [
self.pfv.rs.index.eq(self.insn.RS),
self.pfv.rs.r_stb.eq(1),

self.pfv.cr.w_mask.eq(Cat(Repl(b, 4) for b in self.insn.FXM)),
self.pfv.cr.w_data.eq(self.pfv.rs.r_data[:32]),
]

elif isinstance(self.insn, MFOCRF):
crf = Signal(4)

m.submodules.fxm_enc = fxm_enc = Encoder(width=8)
m.d.comb += [
fxm_enc.i.eq(self.insn.FXM),

self.pfv.cr.r_mask.word_select(fxm_enc.o, width=4).eq(Mux(fxm_enc.n, 0x0, 0xf)),
crf.eq(self.pfv.cr.r_data.word_select(fxm_enc.o, width=4)),

self.pfv.rt.index.eq(self.insn.RT),
self.pfv.rt.w_stb.eq(1),
self.pfv.rt.w_data.word_select(fxm_enc.o, width=4).eq(crf),
]

# Unless exactly one FXM bit is set to 1, RT contents are undefined.
if isinstance(platform, SymbiYosysPlatform):
m.d.comb += Assume(~fxm_enc.n)

elif isinstance(self.insn, MFCR):
m.d.comb += [
self.pfv.cr.r_mask.eq(Repl(1, 32)),
self.pfv.rt.index .eq(self.insn.RT),
self.pfv.rt.w_stb .eq(1),
self.pfv.rt.w_data.eq(self.pfv.cr.r_data),
]

elif isinstance(self.insn, SETB):
crf = Signal(4)
m.d.comb += [
self.pfv.cr.r_mask.word_select(7-self.insn.BFA, width=4).eq(0xf),
crf.eq(self.pfv.cr.r_data.word_select(7-self.insn.BFA, width=4)),

self.pfv.rt.index.eq(self.insn.RT),
self.pfv.rt.w_stb.eq(1),
self.pfv.rt.w_data.eq(Mux(crf[3-0], Repl(1, 64), crf[3-1])),
]

elif isinstance(self.insn, (SETBC, SETBCR, SETNBC, SETNBCR)):
crb = Signal()

m.d.comb += [
self.pfv.cr.r_mask.bit_select(31-self.insn.BI, width=1).eq(1),
crb.eq(self.pfv.cr.r_data.bit_select(31-self.insn.BI, width=1)),

self.pfv.rt.index.eq(self.insn.RT),
self.pfv.rt.w_stb.eq(1),
]

if isinstance(self.insn, SETBC):
m.d.comb += self.pfv.rt.w_data.eq(crb)
if isinstance(self.insn, SETBCR):
m.d.comb += self.pfv.rt.w_data.eq(~crb)
if isinstance(self.insn, SETNBC):
m.d.comb += self.pfv.rt.w_data.eq(Mux(crb, -1, 0))
if isinstance(self.insn, SETNBCR):
m.d.comb += self.pfv.rt.w_data.eq(Mux(crb, 0, -1))

else:
assert False


Loading…
Cancel
Save