diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py
index 34fbf16..4782c23 100644
--- a/cores/microwatt/run.py
+++ b/cores/microwatt/run.py
@@ -98,6 +98,23 @@ if __name__ == "__main__":
         ("gpr",          None, 15),
         ("cr",           None, 15),
         ("spr",          None, 15),
+
+        ("insn_b",       None, 15),
+        ("insn_ba",      None, 15),
+        ("insn_bl",      None, 15),
+        ("insn_bla",     None, 15),
+        ("insn_bc",      None, 15),
+        ("insn_bca",     None, 15),
+        ("insn_bcla",    None, 15),
+
+        # TODO:
+        #("insn_bcl",    None, 15),
+        #("insn_bclr",   None, 15),
+        #("insn_bclrl",  None, 15),
+        #("insn_bcctr",  None, 15),
+        #("insn_bcctrl", None, 15),
+        #("insn_bctar",  None, 15),
+        #("insn_bctarl", None, 15),
     ]
 
     with multiprocessing.Pool(processes=args.jobs) as pool:
diff --git a/power_fv/checks/_branch.py b/power_fv/checks/_branch.py
new file mode 100644
index 0000000..45fcd0e
--- /dev/null
+++ b/power_fv/checks/_branch.py
@@ -0,0 +1,210 @@
+from amaranth import *
+from amaranth.asserts import *
+
+from .. import pfv
+from ..insn import *
+
+
+__all__ = ["Check"]
+
+
+class Check(Elaboratable):
+    _insn_cls = None
+
+    def __init_subclass__(cls, *, insn_cls):
+        cls._insn_cls = insn_cls
+
+    def __init__(self):
+        self.pfv  = pfv.Interface()
+        self.trig = Record([
+            ("pre",  1),
+            ("post", 1),
+        ])
+
+    def elaborate(self, platform):
+        m = Module()
+
+        # TODO:
+        # - support MSR (stop assuming 64-bit mode)
+        # - support interrupts (detect illegal forms)
+
+        spec_insn = self._insn_cls()
+
+        with m.If(self.trig.post):
+            m.d.sync += [
+                Assume(self.pfv.stb),
+                Assume(self.pfv.insn[32:] == spec_insn),
+            ]
+
+        if isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+            bo_valid_patterns = [
+                "0000-",
+                "0001-",
+                "001--",
+                "0100-",
+                "0101-",
+                "011--",
+                "1-00-",
+                "1-01-"
+            ]
+            if not isinstance(spec_insn, Instruction_B):
+                # "Branch always" mnemonics are undefined for B-form conditional branches.
+                # (Appendix C.2.2, Book I)
+                bo_valid_patterns.append("1-1--")
+
+            bo_valid = Signal()
+            m.d.comb += bo_valid.eq(spec_insn.bo.matches(*bo_valid_patterns))
+
+            # FIXME(microwatt,interrupts): turn this into an assert
+            with m.If(self.trig.post):
+                m.d.sync += Assume(bo_valid | self.pfv.intr)
+
+        # NIA
+
+        spec_nia = Signal(unsigned(64))
+        taken    = Signal()
+        offset   = Signal(signed(62))
+
+        if isinstance(spec_insn, Instruction_I):
+            m.d.comb += [
+                taken .eq(1),
+                offset.eq(spec_insn.li)
+            ]
+
+        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+            cond_bit = Signal()
+            ctr_any  = Signal()
+            cond_ok  = Signal()
+            ctr_ok   = Signal()
+
+            m.d.comb += [
+                cond_bit.eq(self.pfv.cr.r_data[::-1].bit_select(spec_insn.bi, width=1)),
+                ctr_any .eq(self.pfv.ctr.w_data.any()),
+                cond_ok .eq(spec_insn.bo[4] | (spec_insn.bo[3] == cond_bit)),
+                ctr_ok  .eq(spec_insn.bo[2] | (ctr_any ^ spec_insn.bo[1])),
+            ]
+
+            if isinstance(spec_insn, Instruction_XL_b) and spec_insn.xo.value == 528: # bcctr/bcctrl
+                m.d.comb += taken.eq(cond_ok)
+            else:
+                m.d.comb += taken.eq(cond_ok & ctr_ok)
+
+            if isinstance(spec_insn, Instruction_B):
+                m.d.comb += offset.eq(spec_insn.bd)
+            elif spec_insn.xo.value ==  16: # bclr/bclrl
+                m.d.comb += offset.eq(self.pfv.lr .r_data[:61])
+            elif spec_insn.xo.value == 528: # bcctr/bcctrl
+                m.d.comb += offset.eq(self.pfv.ctr.r_data[:61])
+            elif spec_insn.xo.value == 560: # bctar/bctarl
+                m.d.comb += offset.eq(self.pfv.tar.r_data[:61])
+            else:
+                assert False
+
+        else:
+            assert False
+
+        with m.If(taken):
+            if isinstance(spec_insn, (Instruction_I, Instruction_B)) and spec_insn.aa.value == 0:
+                m.d.comb += spec_nia.eq(self.pfv.cia + (offset << 2))
+            else:
+                m.d.comb += spec_nia.eq(offset << 2)
+        with m.Else():
+            m.d.comb += spec_nia.eq(self.pfv.cia + 4)
+
+        with m.If(self.trig.post & ~self.pfv.intr):
+            m.d.sync += Assert(self.pfv.nia == spec_nia)
+
+        # CR
+
+        spec_cr_r_stb = Signal(8)
+
+        if isinstance(spec_insn, Instruction_I):
+            m.d.comb += spec_cr_r_stb.eq(0)
+        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+            m.d.comb += spec_cr_r_stb[::-1].bit_select(spec_insn.bi[2:], width=1).eq(1)
+        else:
+            assert False
+
+        with m.If(self.trig.post & ~self.pfv.intr):
+            for i, spec_cr_r_stb_bit in enumerate(spec_cr_r_stb):
+                pfv_cr_r_stb_bit = self.pfv.cr.r_stb[i]
+                m.d.sync += Assert(spec_cr_r_stb_bit.implies(pfv_cr_r_stb_bit))
+
+        # LR
+
+        spec_lr_r_stb  = Signal()
+        spec_lr_w_stb  = Signal()
+        spec_lr_w_data = Signal(64)
+
+        if isinstance(spec_insn, (Instruction_I, Instruction_B)):
+            m.d.comb += spec_lr_r_stb.eq(0)
+        elif isinstance(spec_insn, (Instruction_XL_b)):
+            m.d.comb += spec_lr_r_stb.eq(spec_insn.xo == 16) # bclr/bclrl
+        else:
+            assert False
+
+        m.d.comb += [
+            spec_lr_w_stb .eq(spec_insn.lk),
+            spec_lr_w_data.eq(self.pfv.cia + 4),
+        ]
+
+        with m.If(self.trig.post & ~self.pfv.intr):
+            m.d.sync += [
+                Assert(self.pfv.lr.r_stb == spec_lr_r_stb),
+                Assert(self.pfv.lr.w_stb == spec_lr_w_stb),
+                Assert(self.pfv.lr.w_stb.implies(self.pfv.lr.w_data == spec_lr_w_data)),
+            ]
+
+        # CTR
+
+        spec_ctr_r_stb  = Signal()
+        spec_ctr_w_stb  = Signal()
+        spec_ctr_w_data = Signal(64)
+
+        if isinstance(spec_insn, Instruction_I):
+            m.d.comb += spec_ctr_r_stb.eq(0)
+        elif isinstance(spec_insn, Instruction_B):
+            m.d.comb += spec_ctr_r_stb.eq(~spec_insn.bo[2])
+        elif isinstance(spec_insn, (Instruction_B, Instruction_XL_b)):
+            m.d.comb += spec_ctr_r_stb.eq(1)
+        else:
+            assert False
+
+        if isinstance(spec_insn, Instruction_I):
+            m.d.comb += spec_ctr_w_stb.eq(0)
+        elif isinstance(spec_insn, Instruction_B):
+            m.d.comb += spec_ctr_w_stb.eq(~spec_insn.bo[2])
+        elif isinstance(spec_insn, Instruction_XL_b):
+            if spec_insn.xo.value == 528: # bcctr/bcctrl
+                m.d.comb += spec_ctr_w_stb.eq(0)
+            else:
+                m.d.comb += spec_ctr_w_stb.eq(~spec_insn.bo[2])
+        else:
+            assert False
+
+        m.d.comb += spec_ctr_w_data.eq(self.pfv.ctr.r_data - 1)
+
+        with m.If(self.trig.post & ~self.pfv.intr):
+            m.d.sync += [
+                Assert(self.pfv.ctr.r_stb == spec_ctr_r_stb),
+                Assert(self.pfv.ctr.w_stb == spec_ctr_w_stb),
+                Assert(self.pfv.ctr.w_stb.implies(self.pfv.ctr.w_data == spec_ctr_w_data)),
+            ]
+
+        # TAR
+
+        spec_tar_r_stb = Signal()
+
+        if isinstance(spec_insn, (Instruction_I, Instruction_B)):
+            m.d.comb += spec_tar_r_stb.eq(0)
+        elif isinstance(spec_insn, (Instruction_XL_b)):
+            m.d.comb += spec_tar_r_stb.eq(spec_insn.xo == 560) # bctar/bctarl
+        else:
+            assert False
+
+        with m.If(self.trig.post & ~self.pfv.intr):
+            m.d.sync += [
+                Assert(self.pfv.tar.r_stb == spec_tar_r_stb),
+            ]
+
+        return m
diff --git a/power_fv/checks/insn_b.py b/power_fv/checks/insn_b.py
new file mode 100644
index 0000000..5a3a830
--- /dev/null
+++ b/power_fv/checks/insn_b.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.B):
+    pass
diff --git a/power_fv/checks/insn_ba.py b/power_fv/checks/insn_ba.py
new file mode 100644
index 0000000..03b4ddc
--- /dev/null
+++ b/power_fv/checks/insn_ba.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BA):
+    pass
diff --git a/power_fv/checks/insn_bc.py b/power_fv/checks/insn_bc.py
new file mode 100644
index 0000000..470e64b
--- /dev/null
+++ b/power_fv/checks/insn_bc.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BC):
+    pass
diff --git a/power_fv/checks/insn_bca.py b/power_fv/checks/insn_bca.py
new file mode 100644
index 0000000..ba31123
--- /dev/null
+++ b/power_fv/checks/insn_bca.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCA):
+    pass
diff --git a/power_fv/checks/insn_bcctr.py b/power_fv/checks/insn_bcctr.py
new file mode 100644
index 0000000..cdc0790
--- /dev/null
+++ b/power_fv/checks/insn_bcctr.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCCTR):
+    pass
diff --git a/power_fv/checks/insn_bcctrl.py b/power_fv/checks/insn_bcctrl.py
new file mode 100644
index 0000000..96725fc
--- /dev/null
+++ b/power_fv/checks/insn_bcctrl.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCTRL):
+    pass
diff --git a/power_fv/checks/insn_bcl.py b/power_fv/checks/insn_bcl.py
new file mode 100644
index 0000000..4d287f2
--- /dev/null
+++ b/power_fv/checks/insn_bcl.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCL):
+    pass
diff --git a/power_fv/checks/insn_bcla.py b/power_fv/checks/insn_bcla.py
new file mode 100644
index 0000000..960d28e
--- /dev/null
+++ b/power_fv/checks/insn_bcla.py
@@ -0,0 +1,10 @@
+from . import _branch
+
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCLA):
+    pass
diff --git a/power_fv/checks/insn_bclr.py b/power_fv/checks/insn_bclr.py
new file mode 100644
index 0000000..a6e639f
--- /dev/null
+++ b/power_fv/checks/insn_bclr.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCLR):
+    pass
diff --git a/power_fv/checks/insn_bclrl.py b/power_fv/checks/insn_bclrl.py
new file mode 100644
index 0000000..236ea26
--- /dev/null
+++ b/power_fv/checks/insn_bclrl.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCLRL):
+    pass
diff --git a/power_fv/checks/insn_bctar.py b/power_fv/checks/insn_bctar.py
new file mode 100644
index 0000000..df26f1e
--- /dev/null
+++ b/power_fv/checks/insn_bctar.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCTAR):
+    pass
diff --git a/power_fv/checks/insn_bctarl.py b/power_fv/checks/insn_bctarl.py
new file mode 100644
index 0000000..908056c
--- /dev/null
+++ b/power_fv/checks/insn_bctarl.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BCTARL):
+    pass
diff --git a/power_fv/checks/insn_bl.py b/power_fv/checks/insn_bl.py
new file mode 100644
index 0000000..05fe1c1
--- /dev/null
+++ b/power_fv/checks/insn_bl.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BL):
+    pass
diff --git a/power_fv/checks/insn_bla.py b/power_fv/checks/insn_bla.py
new file mode 100644
index 0000000..a34d516
--- /dev/null
+++ b/power_fv/checks/insn_bla.py
@@ -0,0 +1,9 @@
+from . import _branch
+from .. import insn
+
+
+__all__ = ["Check"]
+
+
+class Check(_branch.Check, insn_cls=insn.BLA):
+    pass
diff --git a/power_fv/insn.py b/power_fv/insn.py
new file mode 100644
index 0000000..c00de79
--- /dev/null
+++ b/power_fv/insn.py
@@ -0,0 +1,88 @@
+from amaranth import *
+from amaranth.asserts import AnyConst
+from amaranth.hdl.ast import ValueCastable
+
+
+class Instruction_I(ValueCastable):
+    po = None
+    li = None
+    aa = None
+    lk = None
+
+    def __init_subclass__(cls, *, po, aa, lk):
+        cls.po = Const(po, unsigned(6))
+        cls.aa = Const(aa, 1)
+        cls.lk = Const(lk, 1)
+
+    def __init__(self):
+        self.li = AnyConst(signed(24))
+
+    @ValueCastable.lowermethod
+    def as_value(self):
+        return Cat(self.lk, self.aa, self.li, self.po)
+
+
+class Instruction_B(ValueCastable):
+    po = None
+    bo = None
+    bi = None
+    bd = None
+    aa = None
+    lk = None
+
+    def __init_subclass__(cls, *, po, aa, lk):
+        cls.po = Const(po, unsigned(6))
+        cls.aa = Const(aa, 1)
+        cls.lk = Const(lk, 1)
+
+    def __init__(self):
+        self.bo = AnyConst(unsigned( 5))
+        self.bi = AnyConst(unsigned( 5))
+        self.bd = AnyConst(  signed(14))
+
+    @ValueCastable.lowermethod
+    def as_value(self):
+        return Cat(self.lk, self.aa, self.bd, self.bi, self.bo, self.po)
+
+
+class Instruction_XL_b(ValueCastable):
+    po = None
+    bo = None
+    bi = None
+    _0 = None
+    bh = None
+    xo = None
+    lk = None
+
+    def __init_subclass__(cls, *, po, xo, lk):
+        cls.po = Const(po, unsigned(6))
+        cls.xo = Const(xo, unsigned(9))
+        cls.lk = Const(1)
+
+    def __init__(self):
+        self.bo = AnyConst(unsigned(5))
+        self.bi = AnyConst(unsigned(5))
+        self._0 = AnyConst(unsigned(3))
+        self.bh = AnyConst(unsigned(2))
+
+    @ValueCastable.lowermethod
+    def as_value(self):
+        return Cat(self.lk, self.xo, self.bh, self._0, self.bi, self.bo, self.po)
+
+
+class B      (Instruction_I, po=18, aa=0, lk=0): pass
+class BA     (Instruction_I, po=18, aa=1, lk=0): pass
+class BL     (Instruction_I, po=18, aa=0, lk=1): pass
+class BLA    (Instruction_I, po=18, aa=1, lk=1): pass
+
+class BC     (Instruction_B, po=16, aa=0, lk=0): pass
+class BCA    (Instruction_B, po=16, aa=1, lk=0): pass
+class BCL    (Instruction_B, po=16, aa=0, lk=1): pass
+class BCLA   (Instruction_B, po=16, aa=1, lk=1): pass
+
+class BCLR   (Instruction_XL_b, po=19, xo= 16, lk=0): pass
+class BCLRL  (Instruction_XL_b, po=19, xo= 16, lk=1): pass
+class BCCTR  (Instruction_XL_b, po=19, xo=528, lk=0): pass
+class BCCTRL (Instruction_XL_b, po=19, xo=528, lk=1): pass
+class BCTAR  (Instruction_XL_b, po=19, xo=560, lk=0): pass
+class BCTARL (Instruction_XL_b, po=19, xo=560, lk=1): pass