In-depth refactoring, improved user interface.

* A PowerFVSession class provides a REPL interface. Functionality is
  split into commands (e.g. add checks, build) which can be provided
  interactively or from a file.

  See cores/microwatt for an example of its integration.

* Instruction specifications are now separated from verification
  testbenches.

  An InsnSpec class provides a behavioral model using the same PowerFV
  interface as a core. This interface is output-only for a core, but
  bidirectional for the InsnSpec:
    - fields related to context (e.g. read data) are inputs,
    - fields related to side-effects (e.g. write strobes) are outputs.

  The testbench is responsible for driving inputs to the same values
  as the core, then check outputs for equivalence. This decoupling
  provides a path towards using PowerFV in simulation.

* Instruction encodings are now defined by their fields, not their
  format (which was problematic e.g. X-form has dozens of variants).

  Field declarations can be preset to a value, or left undefined. In
  the latter case, they are implicitly cast to AnyConst (which is
  useful for arbitrary values like immediates).
main
Jean-François Nguyen 3 years ago
parent 05965592f9
commit dd6048f14b

@ -7,7 +7,7 @@
Get Microwatt:

```
git clone git@git.openpower.foundation:jfng/microwatt -b powerfv
git clone git@git.openpower.foundation:jfng/microwatt -b powerfv microwatt-src
```

## Usage
@ -17,13 +17,19 @@ git clone git@git.openpower.foundation:jfng/microwatt -b powerfv
```
poetry shell

python ./run.py --help
python microwatt.py -h

exit
```

### Run the checks locally
### Run commands from a file

```
python run.py --jobs=$(nproc)
python microwatt.py -c checks.pfv
```

### Run commands interactively

```
python microwatt.py -i
```

@ -1,173 +0,0 @@
from amaranth import *
from amaranth.asserts import *

from power_fv import pfv


__all__ = ["MicrowattWrapper"]


class MicrowattWrapper(Elaboratable):
def __init__(self):
self.pfv = pfv.Interface()

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

wb_insn_dat_r = AnySeq(64)
wb_insn_ack = AnySeq( 1)
wb_insn_stall = AnySeq( 1)
wb_insn_adr = Signal(29, attrs={"keep": True})
wb_insn_dat_w = Signal(64, attrs={"keep": True})
wb_insn_sel = Signal( 8, attrs={"keep": True})
wb_insn_cyc = Signal( attrs={"keep": True})
wb_insn_stb = Signal( attrs={"keep": True})
wb_insn_we = Signal( attrs={"keep": True})

wb_data_dat_r = AnySeq(64)
wb_data_ack = AnySeq( 1)
wb_data_stall = AnySeq( 1)
wb_data_adr = Signal(29, attrs={"keep": True})
wb_data_dat_w = Signal(64, attrs={"keep": True})
wb_data_sel = Signal( 8, attrs={"keep": True})
wb_data_cyc = Signal( 1, attrs={"keep": True})
wb_data_stb = Signal( 1, attrs={"keep": True})
wb_data_we = Signal( 1, attrs={"keep": True})

wb_snoop_adr = AnySeq(29)
wb_snoop_dat_w = AnySeq(64)
wb_snoop_sel = AnySeq( 8)
wb_snoop_cyc = AnySeq( 1)
wb_snoop_stb = AnySeq( 1)
wb_snoop_we = AnySeq( 1)

dmi_addr = AnySeq( 4)
dmi_din = AnySeq(64)
dmi_req = AnySeq( 1)
dmi_wr = AnySeq( 1)
dmi_dout = Signal(64, attrs={"keep": True})
dmi_ack = Signal( attrs={"keep": True})

terminated = Signal( attrs={"keep": True})

# FIXME: ghdl-yosys-plugin doesn't yet support setting parameters (see issue 136).
# As a workaround, use our own toplevel entity.
m.submodules.toplevel = Instance("toplevel",
("i", "clk", ClockSignal("sync")),
("i", "rst", ResetSignal("sync")),
("i", "alt_reset", Const(0)),
("i", "ext_irq", Const(0)),

("i", "wishbone_insn_in.dat", wb_insn_dat_r),
("i", "wishbone_insn_in.ack", wb_insn_ack),
("i", "wishbone_insn_in.stall", wb_insn_stall),
("o", "wishbone_insn_out.adr", wb_insn_adr),
("o", "wishbone_insn_out.dat", wb_insn_dat_w),
("o", "wishbone_insn_out.sel", wb_insn_sel),
("o", "wishbone_insn_out.cyc", wb_insn_cyc),
("o", "wishbone_insn_out.stb", wb_insn_stb),
("o", "wishbone_insn_out.we", wb_insn_we),

("i", "wishbone_data_in.dat", wb_data_dat_r),
("i", "wishbone_data_in.ack", wb_data_ack),
("i", "wishbone_data_in.stall", wb_data_stall),
("o", "wishbone_data_out.adr", wb_data_adr),
("o", "wishbone_data_out.dat", wb_data_dat_w),
("o", "wishbone_data_out.sel", wb_data_sel),
("o", "wishbone_data_out.cyc", wb_data_cyc),
("o", "wishbone_data_out.stb", wb_data_stb),
("o", "wishbone_data_out.we", wb_data_we),

("i", "wb_snoop_in.adr", wb_snoop_adr),
("i", "wb_snoop_in.dat", wb_snoop_dat_w),
("i", "wb_snoop_in.sel", wb_snoop_sel),
("i", "wb_snoop_in.cyc", wb_snoop_cyc),
("i", "wb_snoop_in.stb", wb_snoop_stb),
("i", "wb_snoop_in.we", wb_snoop_we),

("i", "dmi_addr", dmi_addr),
("i", "dmi_din", dmi_din),
("o", "dmi_dout", dmi_dout),
("i", "dmi_req", dmi_req),
("i", "dmi_wr", dmi_wr),
("o", "dmi_ack", dmi_ack),

("o", "terminated_out", terminated),

("o", "pfv_stb", self.pfv.stb),
("o", "pfv_insn", self.pfv.insn),
("o", "pfv_order", self.pfv.order),
("o", "pfv_intr", self.pfv.intr),
("o", "pfv_cia", self.pfv.cia),
("o", "pfv_nia", self.pfv.nia),

("o", "pfv_ra_index", self.pfv.ra.index),
("o", "pfv_ra_r_stb", self.pfv.ra.r_stb),
("o", "pfv_ra_r_data", self.pfv.ra.r_data),
("o", "pfv_ra_w_stb", self.pfv.ra.w_stb),
("o", "pfv_ra_w_data", self.pfv.ra.w_data),

("o", "pfv_rb_index", self.pfv.rb.index),
("o", "pfv_rb_r_stb", self.pfv.rb.r_stb),
("o", "pfv_rb_r_data", self.pfv.rb.r_data),

("o", "pfv_rs_index", self.pfv.rs.index),
("o", "pfv_rs_r_stb", self.pfv.rs.r_stb),
("o", "pfv_rs_r_data", self.pfv.rs.r_data),

("o", "pfv_rt_index", self.pfv.rt.index),
("o", "pfv_rt_r_stb", self.pfv.rt.r_stb),
("o", "pfv_rt_r_data", self.pfv.rt.r_data),
("o", "pfv_rt_w_stb", self.pfv.rt.w_stb),
("o", "pfv_rt_w_data", self.pfv.rt.w_data),

("o", "pfv_cr_r_stb", self.pfv.cr.r_stb),
("o", "pfv_cr_r_data", self.pfv.cr.r_data),
("o", "pfv_cr_w_stb", self.pfv.cr.w_stb),
("o", "pfv_cr_w_data", self.pfv.cr.w_data),

("o", "pfv_msr_r_mask", self.pfv.msr.r_mask),
("o", "pfv_msr_r_data", self.pfv.msr.r_data),
("o", "pfv_msr_w_mask", self.pfv.msr.w_mask),
("o", "pfv_msr_w_data", self.pfv.msr.w_data),

("o", "pfv_lr_r_mask", self.pfv.lr.r_mask),
("o", "pfv_lr_r_data", self.pfv.lr.r_data),
("o", "pfv_lr_w_mask", self.pfv.lr.w_mask),
("o", "pfv_lr_w_data", self.pfv.lr.w_data),

("o", "pfv_ctr_r_mask", self.pfv.ctr.r_mask),
("o", "pfv_ctr_r_data", self.pfv.ctr.r_data),
("o", "pfv_ctr_w_mask", self.pfv.ctr.w_mask),
("o", "pfv_ctr_w_data", self.pfv.ctr.w_data),

("o", "pfv_xer_r_mask", self.pfv.xer.r_mask),
("o", "pfv_xer_r_data", self.pfv.xer.r_data),
("o", "pfv_xer_w_mask", self.pfv.xer.w_mask),
("o", "pfv_xer_w_data", self.pfv.xer.w_data),

("o", "pfv_tar_r_mask", self.pfv.tar.r_mask),
("o", "pfv_tar_r_data", self.pfv.tar.r_data),
("o", "pfv_tar_w_mask", self.pfv.tar.w_mask),
("o", "pfv_tar_w_data", self.pfv.tar.w_data),

("o", "pfv_srr0_r_mask", self.pfv.srr0.r_mask),
("o", "pfv_srr0_r_data", self.pfv.srr0.r_data),
("o", "pfv_srr0_w_mask", self.pfv.srr0.w_mask),
("o", "pfv_srr0_w_data", self.pfv.srr0.w_data),

("o", "pfv_srr1_r_mask", self.pfv.srr1.r_mask),
("o", "pfv_srr1_r_data", self.pfv.srr1.r_data),
("o", "pfv_srr1_w_mask", self.pfv.srr1.w_mask),
("o", "pfv_srr1_w_data", self.pfv.srr1.w_data),
)

with m.If(Initial()):
m.d.comb += Assume(~self.pfv.stb)

m.d.comb += [
Assume(~dmi_req),
Assume(~terminated),
]

return m

@ -0,0 +1,7 @@
check unique --depth=15 --skip=12
check cia --depth=15
check gpr --depth=15
check insn --depth=15

build --build-dir=./build --src-dir=./microwatt-src
exit

@ -0,0 +1,328 @@
import os
import pathlib
import textwrap

from amaranth import *
from amaranth.asserts import *

from power_fv import pfv
from power_fv.core import PowerFVCore
from power_fv.session import PowerFVSession


__all__ = ["MicrowattWrapper", "MicrowattCore", "MicrowattSession"]


class MicrowattWrapper(Elaboratable):
@classmethod
def add_check_arguments(cls, parser):
group = parser.add_argument_group(title="microwatt options")
group.add_argument(
"--ex1-bypass", choices=("true","false"), default="true",
help="(default: %(default)s)")
group.add_argument(
"--has-btc", choices=("true","false"), default="true",
help="(default: %(default)s)")
group.add_argument(
"--icache-num-lines", type=int, default=2,
help="(default: %(default)s)")
group.add_argument(
"--icache-num-ways", type=int, default=1,
help="(default: %(default)s)")
group.add_argument(
"--icache-tlb-size", type=int, default=1,
help="(default: %(default)s)")
group.add_argument(
"--dcache-num-lines", type=int, default=2,
help="(default: %(default)s)")
group.add_argument(
"--dcache-num-ways", type=int, default=1,
help="(default: %(default)s)")
group.add_argument(
"--dcache-tlb-set-size", type=int, default=1,
help="(default: %(default)s)")
group.add_argument(
"--dcache-tlb-num-ways", type=int, default=1,
help="(default: %(default)s)")

# ghdl-yosys-plugin doesn't yet support setting instance parameters from outside VHDL
# (see upstream issue 136).
# As a workaround, we use a template to generate a VHDL toplevel at build-time, which
# is instantiated in .elaborate().

MICROWATT_TOPLEVEL = textwrap.dedent(r"""
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

library work;
use work.common.all;
use work.wishbone_types.all;
use work.powerfv_types.all;

entity toplevel is
port (
clk : in std_ulogic;
rst : in std_ulogic;

-- Alternate reset (0xffff0000) for use by DRAM init fw
alt_reset : in std_ulogic;

-- Wishbone interface
wishbone_insn_in : in wishbone_slave_out;
wishbone_insn_out : out wishbone_master_out;
wishbone_data_in : in wishbone_slave_out;
wishbone_data_out : out wishbone_master_out;
wb_snoop_in : in wishbone_master_out;

dmi_addr : in std_ulogic_vector(3 downto 0);
dmi_din : in std_ulogic_vector(63 downto 0);
dmi_dout : out std_ulogic_vector(63 downto 0);
dmi_req : in std_ulogic;
dmi_wr : in std_ulogic;
dmi_ack : out std_ulogic;

ext_irq : in std_ulogic;

terminated_out : out std_logic;

pfv_out : out pfv_t
);
end entity toplevel;

architecture behave of toplevel is
signal pfv : pfv_t;
begin
core: entity work.core
generic map (
SIM => false,
DISABLE_FLATTEN => false,
EX1_BYPASS => {ex1_bypass},
HAS_FPU => false,
HAS_BTC => {has_btc},
HAS_SHORT_MULT => false,
HAS_POWERFV => true,
LOG_LENGTH => 0,
ICACHE_NUM_LINES => {icache_num_lines},
ICACHE_NUM_WAYS => {icache_num_ways},
ICACHE_TLB_SIZE => {icache_tlb_size},
DCACHE_NUM_LINES => {dcache_num_lines},
DCACHE_NUM_WAYS => {dcache_num_ways},
DCACHE_TLB_SET_SIZE => {dcache_tlb_set_size},
DCACHE_TLB_NUM_WAYS => {dcache_tlb_num_ways}
)
port map (
clk => clk,
rst => rst,
alt_reset => alt_reset,
wishbone_insn_in => wishbone_insn_in,
wishbone_insn_out => wishbone_insn_out,
wishbone_data_in => wishbone_data_in,
wishbone_data_out => wishbone_data_out,
wb_snoop_in => wb_snoop_in,
dmi_addr => dmi_addr,
dmi_din => dmi_din,
dmi_dout => dmi_dout,
dmi_req => dmi_req,
dmi_wr => dmi_wr,
dmi_ack => dmi_ack,
ext_irq => ext_irq,
terminated_out => terminated_out,
pfv_out => pfv_out
);
end architecture behave;
""")

def __init__(self, **kwargs):
self.pfv = pfv.Interface()
self._kwargs = kwargs

def _render_toplevel(self):
return self.MICROWATT_TOPLEVEL.format(**self._kwargs)

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

wb_insn_dat_r = AnySeq(64)
wb_insn_ack = AnySeq( 1)
wb_insn_stall = AnySeq( 1)
wb_insn_adr = Signal(29, attrs={"keep": True})
wb_insn_dat_w = Signal(64, attrs={"keep": True})
wb_insn_sel = Signal( 8, attrs={"keep": True})
wb_insn_cyc = Signal( attrs={"keep": True})
wb_insn_stb = Signal( attrs={"keep": True})
wb_insn_we = Signal( attrs={"keep": True})

wb_data_dat_r = AnySeq(64)
wb_data_ack = AnySeq( 1)
wb_data_stall = AnySeq( 1)
wb_data_adr = Signal(29, attrs={"keep": True})
wb_data_dat_w = Signal(64, attrs={"keep": True})
wb_data_sel = Signal( 8, attrs={"keep": True})
wb_data_cyc = Signal( 1, attrs={"keep": True})
wb_data_stb = Signal( 1, attrs={"keep": True})
wb_data_we = Signal( 1, attrs={"keep": True})

wb_snoop_adr = AnySeq(29)
wb_snoop_dat_w = AnySeq(64)
wb_snoop_sel = AnySeq( 8)
wb_snoop_cyc = AnySeq( 1)
wb_snoop_stb = AnySeq( 1)
wb_snoop_we = AnySeq( 1)

dmi_addr = AnySeq( 4)
dmi_din = AnySeq(64)
dmi_req = AnySeq( 1)
dmi_wr = AnySeq( 1)
dmi_dout = Signal(64, attrs={"keep": True})
dmi_ack = Signal( attrs={"keep": True})

terminated = Signal( attrs={"keep": True})

m.submodules.dut = Instance("toplevel",
("i", "clk", ClockSignal()),
("i", "rst", ResetSignal()),
("i", "alt_reset", Const(0)),
("i", "ext_irq", Const(0)),

("i", "wishbone_insn_in.dat" , wb_insn_dat_r),
("i", "wishbone_insn_in.ack" , wb_insn_ack ),
("i", "wishbone_insn_in.stall", wb_insn_stall),
("o", "wishbone_insn_out.adr" , wb_insn_adr ),
("o", "wishbone_insn_out.dat" , wb_insn_dat_w),
("o", "wishbone_insn_out.sel" , wb_insn_sel ),
("o", "wishbone_insn_out.cyc" , wb_insn_cyc ),
("o", "wishbone_insn_out.stb" , wb_insn_stb ),
("o", "wishbone_insn_out.we" , wb_insn_we ),

("i", "wishbone_data_in.dat" , wb_data_dat_r),
("i", "wishbone_data_in.ack" , wb_data_ack ),
("i", "wishbone_data_in.stall", wb_data_stall),
("o", "wishbone_data_out.adr" , wb_data_adr ),
("o", "wishbone_data_out.dat" , wb_data_dat_w),
("o", "wishbone_data_out.sel" , wb_data_sel ),
("o", "wishbone_data_out.cyc" , wb_data_cyc ),
("o", "wishbone_data_out.stb" , wb_data_stb ),
("o", "wishbone_data_out.we" , wb_data_we ),

("i", "wb_snoop_in.adr", wb_snoop_adr ),
("i", "wb_snoop_in.dat", wb_snoop_dat_w),
("i", "wb_snoop_in.sel", wb_snoop_sel ),
("i", "wb_snoop_in.cyc", wb_snoop_cyc ),
("i", "wb_snoop_in.stb", wb_snoop_stb ),
("i", "wb_snoop_in.we" , wb_snoop_we ),

("i", "dmi_addr", dmi_addr),
("i", "dmi_din" , dmi_din ),
("o", "dmi_dout", dmi_dout),
("i", "dmi_req" , dmi_req ),
("i", "dmi_wr" , dmi_wr ),
("o", "dmi_ack" , dmi_ack ),

("o", "terminated_out", terminated),

("o", "pfv_out.stb" , self.pfv.stb ),
("o", "pfv_out.insn" , self.pfv.insn ),
("o", "pfv_out.order", self.pfv.order),
("o", "pfv_out.intr" , self.pfv.intr ),
("o", "pfv_out.cia" , self.pfv.cia ),
("o", "pfv_out.nia" , self.pfv.nia ),
("o", "pfv_out.ra" , self.pfv.ra ),
("o", "pfv_out.rb" , self.pfv.rb ),
("o", "pfv_out.rs" , self.pfv.rs ),
("o", "pfv_out.rt" , self.pfv.rt ),
("o", "pfv_out.cr" , self.pfv.cr ),
("o", "pfv_out.msr" , self.pfv.msr ),
("o", "pfv_out.lr" , self.pfv.lr ),
("o", "pfv_out.ctr" , self.pfv.ctr ),
("o", "pfv_out.tar" , self.pfv.tar ),
("o", "pfv_out.xer" , self.pfv.xer ),
("o", "pfv_out.srr0" , self.pfv.srr0 ),
("o", "pfv_out.srr1" , self.pfv.srr1 ),
)

m.d.comb += [
Assume(~dmi_req),
Assume(~terminated),
]

return m


class MicrowattCore(PowerFVCore):
MICROWATT_FILES = (
"cache_ram.vhdl",
"common.vhdl",
"control.vhdl",
"core_debug.vhdl",
"core.vhdl",
"countbits.vhdl",
"cr_file.vhdl",
"crhelpers.vhdl",
"dcache.vhdl",
"decode1.vhdl",
"decode2.vhdl",
"decode_types.vhdl",
"divider.vhdl",
"execute1.vhdl",
"fetch1.vhdl",
"fpu.vhdl",
"helpers.vhdl",
"icache.vhdl",
"insn_helpers.vhdl",
"loadstore1.vhdl",
"logical.vhdl",
"mmu.vhdl",
"multiply.vhdl",
"nonrandom.vhdl",
"plru.vhdl",
"pmu.vhdl",
"powerfv_types.vhdl",
"powerfv.vhdl",
"ppc_fx_insns.vhdl",
"register_file.vhdl",
"rotator.vhdl",
"utils.vhdl",
"wishbone_types.vhdl",
"writeback.vhdl",
)

@classmethod
def add_check_arguments(cls, parser):
super().add_check_arguments(parser)
MicrowattWrapper.add_check_arguments(parser)

@classmethod
def wrapper(cls, **kwargs):
return MicrowattWrapper(**kwargs)

@classmethod
def add_build_arguments(cls, parser):
super().add_build_arguments(parser)
group = parser.add_argument_group(title="microwatt options")
group.add_argument(
"--src-dir", type=pathlib.Path, default=pathlib.Path("./microwatt-src"),
help="microwatt directory (default: %(default)s)")
group.add_argument(
"--ghdl-opts", type=str, default="--std=08",
help="ghdl options (default: '%(default)s')")

@classmethod
def add_files(cls, platform, wrapper, *, src_dir, **kwargs):
assert isinstance(wrapper, MicrowattWrapper)

for filename in cls.MICROWATT_FILES:
contents = open(os.path.join(src_dir, filename), "r")
platform.add_file(filename, contents)

top_filename = "top-powerfv.vhdl"
top_contents = wrapper._render_toplevel()
platform.add_file(top_filename, top_contents)


class MicrowattSession(PowerFVSession, core_cls=MicrowattCore):
pass


if __name__ == "__main__":
MicrowattSession().main()

@ -1,209 +0,0 @@
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

library work;
use work.common.all;
use work.wishbone_types.all;
use work.powerfv_types.all;

entity toplevel is
port (
clk : in std_ulogic;
rst : in std_ulogic;

-- Alternate reset (0xffff0000) for use by DRAM init fw
alt_reset : in std_ulogic;

-- Wishbone interface
wishbone_insn_in : in wishbone_slave_out;
wishbone_insn_out : out wishbone_master_out;

wishbone_data_in : in wishbone_slave_out;
wishbone_data_out : out wishbone_master_out;

wb_snoop_in : in wishbone_master_out;

dmi_addr : in std_ulogic_vector(3 downto 0);
dmi_din : in std_ulogic_vector(63 downto 0);
dmi_dout : out std_ulogic_vector(63 downto 0);
dmi_req : in std_ulogic;
dmi_wr : in std_ulogic;
dmi_ack : out std_ulogic;

ext_irq : in std_ulogic;

terminated_out : out std_logic;

pfv_stb : out std_ulogic;
pfv_insn : out std_ulogic_vector(63 downto 0);
pfv_order : out std_ulogic_vector(63 downto 0);
pfv_intr : out std_ulogic;
pfv_cia : out std_ulogic_vector(63 downto 0);
pfv_nia : out std_ulogic_vector(63 downto 0);

pfv_ra_index : out std_ulogic_vector( 4 downto 0);
pfv_ra_r_stb : out std_ulogic;
pfv_ra_r_data : out std_ulogic_vector(63 downto 0);
pfv_ra_w_stb : out std_ulogic;
pfv_ra_w_data : out std_ulogic_vector(63 downto 0);
pfv_rb_index : out std_ulogic_vector( 4 downto 0);
pfv_rb_r_stb : out std_ulogic;
pfv_rb_r_data : out std_ulogic_vector(63 downto 0);
pfv_rs_index : out std_ulogic_vector( 4 downto 0);
pfv_rs_r_stb : out std_ulogic;
pfv_rs_r_data : out std_ulogic_vector(63 downto 0);
pfv_rt_index : out std_ulogic_vector( 4 downto 0);
pfv_rt_r_stb : out std_ulogic;
pfv_rt_r_data : out std_ulogic_vector(63 downto 0);
pfv_rt_w_stb : out std_ulogic;
pfv_rt_w_data : out std_ulogic_vector(63 downto 0);

pfv_cr_r_stb : out std_ulogic_vector( 7 downto 0);
pfv_cr_r_data : out std_ulogic_vector(31 downto 0);
pfv_cr_w_stb : out std_ulogic_vector( 7 downto 0);
pfv_cr_w_data : out std_ulogic_vector(31 downto 0);

pfv_msr_r_mask : out std_ulogic_vector(63 downto 0);
pfv_msr_r_data : out std_ulogic_vector(63 downto 0);
pfv_msr_w_mask : out std_ulogic_vector(63 downto 0);
pfv_msr_w_data : out std_ulogic_vector(63 downto 0);

pfv_lr_r_mask : out std_ulogic_vector(63 downto 0);
pfv_lr_r_data : out std_ulogic_vector(63 downto 0);
pfv_lr_w_mask : out std_ulogic_vector(63 downto 0);
pfv_lr_w_data : out std_ulogic_vector(63 downto 0);

pfv_ctr_r_mask : out std_ulogic_vector(63 downto 0);
pfv_ctr_r_data : out std_ulogic_vector(63 downto 0);
pfv_ctr_w_mask : out std_ulogic_vector(63 downto 0);
pfv_ctr_w_data : out std_ulogic_vector(63 downto 0);

pfv_xer_r_mask : out std_ulogic_vector(63 downto 0);
pfv_xer_r_data : out std_ulogic_vector(63 downto 0);
pfv_xer_w_mask : out std_ulogic_vector(63 downto 0);
pfv_xer_w_data : out std_ulogic_vector(63 downto 0);

pfv_tar_r_mask : out std_ulogic_vector(63 downto 0);
pfv_tar_r_data : out std_ulogic_vector(63 downto 0);
pfv_tar_w_mask : out std_ulogic_vector(63 downto 0);
pfv_tar_w_data : out std_ulogic_vector(63 downto 0);

pfv_srr0_r_mask : out std_ulogic_vector(63 downto 0);
pfv_srr0_r_data : out std_ulogic_vector(63 downto 0);
pfv_srr0_w_mask : out std_ulogic_vector(63 downto 0);
pfv_srr0_w_data : out std_ulogic_vector(63 downto 0);

pfv_srr1_r_mask : out std_ulogic_vector(63 downto 0);
pfv_srr1_r_data : out std_ulogic_vector(63 downto 0);
pfv_srr1_w_mask : out std_ulogic_vector(63 downto 0);
pfv_srr1_w_data : out std_ulogic_vector(63 downto 0)
);
end entity toplevel;

architecture behave of toplevel is
signal pfv : pfv_t;
begin
core: entity work.core
generic map (
SIM => false,
DISABLE_FLATTEN => false,
EX1_BYPASS => true,
HAS_FPU => false,
HAS_BTC => true,
HAS_SHORT_MULT => false,
HAS_POWERFV => true,
LOG_LENGTH => 0,
ICACHE_NUM_LINES => 2,
ICACHE_NUM_WAYS => 1,
ICACHE_TLB_SIZE => 1,
DCACHE_NUM_LINES => 2,
DCACHE_NUM_WAYS => 1,
DCACHE_TLB_SET_SIZE => 1,
DCACHE_TLB_NUM_WAYS => 1
)
port map (
clk => clk,
rst => rst,
alt_reset => alt_reset,
wishbone_insn_in => wishbone_insn_in,
wishbone_insn_out => wishbone_insn_out,
wishbone_data_in => wishbone_data_in,
wishbone_data_out => wishbone_data_out,
wb_snoop_in => wb_snoop_in,
dmi_addr => dmi_addr,
dmi_din => dmi_din,
dmi_dout => dmi_dout,
dmi_req => dmi_req,
dmi_wr => dmi_wr,
dmi_ack => dmi_ack,
ext_irq => ext_irq,
terminated_out => terminated_out,
pfv_out => pfv
);

pfv_stb <= pfv.stb;
pfv_insn <= pfv.insn;
pfv_order <= pfv.order;
pfv_intr <= pfv.intr;
pfv_cia <= pfv.cia;
pfv_nia <= pfv.nia;

pfv_ra_index <= pfv.ra.index;
pfv_ra_r_stb <= pfv.ra.r_stb;
pfv_ra_r_data <= pfv.ra.r_data;
pfv_ra_w_stb <= pfv.ra.w_stb;
pfv_ra_w_data <= pfv.ra.w_data;
pfv_rb_index <= pfv.rb.index;
pfv_rb_r_stb <= pfv.rb.r_stb;
pfv_rb_r_data <= pfv.rb.r_data;
pfv_rs_index <= pfv.rs.index;
pfv_rs_r_stb <= pfv.rs.r_stb;
pfv_rs_r_data <= pfv.rs.r_data;
pfv_rt_index <= pfv.rt.index;
pfv_rt_r_stb <= pfv.rt.r_stb;
pfv_rt_r_data <= pfv.rt.r_data;
pfv_rt_w_stb <= pfv.rt.w_stb;
pfv_rt_w_data <= pfv.rt.w_data;

pfv_cr_r_stb <= pfv.cr.r_stb;
pfv_cr_r_data <= pfv.cr.r_data;
pfv_cr_w_stb <= pfv.cr.w_stb;
pfv_cr_w_data <= pfv.cr.w_data;

pfv_msr_r_mask <= pfv.msr.r_mask;
pfv_msr_r_data <= pfv.msr.r_data;
pfv_msr_w_mask <= pfv.msr.w_mask;
pfv_msr_w_data <= pfv.msr.w_data;

pfv_lr_r_mask <= pfv.lr.r_mask;
pfv_lr_r_data <= pfv.lr.r_data;
pfv_lr_w_mask <= pfv.lr.w_mask;
pfv_lr_w_data <= pfv.lr.w_data;

pfv_ctr_r_mask <= pfv.ctr.r_mask;
pfv_ctr_r_data <= pfv.ctr.r_data;
pfv_ctr_w_mask <= pfv.ctr.w_mask;
pfv_ctr_w_data <= pfv.ctr.w_data;

pfv_xer_r_mask <= pfv.xer.r_mask;
pfv_xer_r_data <= pfv.xer.r_data;
pfv_xer_w_mask <= pfv.xer.w_mask;
pfv_xer_w_data <= pfv.xer.w_data;

pfv_tar_r_mask <= pfv.tar.r_mask;
pfv_tar_r_data <= pfv.tar.r_data;
pfv_tar_w_mask <= pfv.tar.w_mask;
pfv_tar_w_data <= pfv.tar.w_data;

pfv_srr0_r_mask <= pfv.srr0.r_mask;
pfv_srr0_r_data <= pfv.srr0.r_data;
pfv_srr0_w_mask <= pfv.srr0.w_mask;
pfv_srr0_w_data <= pfv.srr0.w_data;

pfv_srr1_r_mask <= pfv.srr1.r_mask;
pfv_srr1_r_data <= pfv.srr1.r_data;
pfv_srr1_w_mask <= pfv.srr1.w_mask;
pfv_srr1_w_data <= pfv.srr1.w_data;

end architecture behave;

@ -1,194 +0,0 @@
import argparse
import os
import multiprocessing

from amaranth import *

from power_fv.checks import *
from power_fv.checks.all import *
from power_fv.build import SymbiYosysPlatform

from _wrapper import MicrowattWrapper


def microwatt_files():
_filenames = (
"cache_ram.vhdl",
"common.vhdl",
"control.vhdl",
"core_debug.vhdl",
"core.vhdl",
"countbits.vhdl",
"cr_file.vhdl",
"crhelpers.vhdl",
"dcache.vhdl",
"decode1.vhdl",
"decode2.vhdl",
"decode_types.vhdl",
"divider.vhdl",
"execute1.vhdl",
"fetch1.vhdl",
"fpu.vhdl",
"helpers.vhdl",
"icache.vhdl",
"insn_helpers.vhdl",
"loadstore1.vhdl",
"logical.vhdl",
"mmu.vhdl",
"multiply.vhdl",
"nonrandom.vhdl",
"plru.vhdl",
"pmu.vhdl",
"powerfv_types.vhdl",
"powerfv.vhdl",
"ppc_fx_insns.vhdl",
"register_file.vhdl",
"rotator.vhdl",
"utils.vhdl",
"wishbone_types.vhdl",
"writeback.vhdl",
)

for filename in _filenames:
contents = open(os.path.join(os.curdir, "microwatt", filename), "r").read()
yield filename, contents

top_filename = "microwatt_top.vhdl"
top_contents = open(os.path.join(os.curdir, top_filename), "r").read()
yield top_filename, top_contents


def run_check(*args):
check_name, tb_args = args

check = PowerFVCheck.registry[check_name]()
dut = MicrowattWrapper()
tb = check.get_testbench(dut, **tb_args)

platform = SymbiYosysPlatform()
for filename, contents in microwatt_files():
platform.add_file(filename, contents)

tb_name = "{}_tb".format(check_name)
build_dir = "build/{}".format(tb_name)

platform.build(
top = tb,
name = tb_name,
build_dir = build_dir,
mode = "bmc",
ghdl_opts = "--std=08",
prep_opts = "-nordff",
)


if __name__ == "__main__":
parser = argparse.ArgumentParser()
parser.add_argument("-j", "--jobs",
help="Number of worker processes (default: os.cpu_count())",
type=int,
default=os.cpu_count(),
)

args = parser.parse_args()

checks = [
("cons_unique", {"post": 15, "pre": 12}),
("cons_ia_fwd", {"post": 15}),
("cons_gpr", {"post": 15}),
("cons_cr", {"post": 15}),
("cons_lr", {"post": 15}),
("cons_ctr", {"post": 15}),
("cons_xer", {"post": 15}),
("cons_tar", {"post": 15}),
("cons_srr0", {"post": 15}),
("cons_srr1", {"post": 15}),

("insn_b", {"post": 15}),
("insn_ba", {"post": 15}),
("insn_bl", {"post": 15}),
("insn_bla", {"post": 15}),
("insn_bc", {"post": 15}),
("insn_bca", {"post": 15}),
("insn_bcl", {"post": 15}),
("insn_bcla", {"post": 15}),
("insn_bclr", {"post": 15}),
("insn_bclrl", {"post": 15}),
("insn_bcctr", {"post": 15}),
("insn_bcctrl", {"post": 15}),
("insn_bctar", {"post": 15}),
("insn_bctarl", {"post": 15}),

("insn_crand", {"post": 15}),
("insn_cror", {"post": 15}),
("insn_crnand", {"post": 15}),
("insn_crxor", {"post": 15}),
("insn_crnor", {"post": 15}),
("insn_crandc", {"post": 15}),
("insn_creqv", {"post": 15}),
("insn_crorc", {"post": 15}),
("insn_mcrf", {"post": 15}),

("insn_addi", {"post": 15}),
("insn_addis", {"post": 15}),
("insn_addpcis", {"post": 15}),
("insn_add", {"post": 15}),
("insn_add.", {"post": 15}),
("insn_addo", {"post": 15}),
("insn_addo.", {"post": 15}),
("insn_addic", {"post": 15}),
("insn_addic.", {"post": 15}),
("insn_subf", {"post": 15}),
("insn_subf.", {"post": 15}),
("insn_subfo", {"post": 15}),
("insn_subfo.", {"post": 15}),
("insn_subfic", {"post": 15}),
("insn_addc", {"post": 15}),
("insn_addc.", {"post": 15}),
("insn_addco", {"post": 15}),
("insn_addco.", {"post": 15}),
("insn_adde", {"post": 15}),
("insn_adde.", {"post": 15}),
("insn_addeo", {"post": 15}),
("insn_addeo.", {"post": 15}),
("insn_subfc", {"post": 15}),
("insn_subfc.", {"post": 15}),
("insn_subfco", {"post": 15}),
("insn_subfco.", {"post": 15}),
("insn_subfe", {"post": 15}),
("insn_subfe.", {"post": 15}),
("insn_subfeo", {"post": 15}),
("insn_subfeo.", {"post": 15}),
("insn_addme", {"post": 15}),
("insn_addme.", {"post": 15}),
("insn_addmeo", {"post": 15}),
("insn_addmeo.", {"post": 15}),
("insn_addze", {"post": 15}),
("insn_addze.", {"post": 15}),
("insn_addzeo", {"post": 15}),
("insn_addzeo.", {"post": 15}),
("insn_subfme", {"post": 15}),
("insn_subfme.", {"post": 15}),
("insn_subfmeo", {"post": 15}),
("insn_subfmeo.", {"post": 15}),
("insn_subfze", {"post": 15}),
("insn_subfze.", {"post": 15}),
("insn_subfzeo", {"post": 15}),
("insn_subfzeo.", {"post": 15}),
("insn_addex", {"post": 15}),
("insn_neg", {"post": 15}),
("insn_neg.", {"post": 15}),
("insn_nego", {"post": 15}),
("insn_nego.", {"post": 15}),

("insn_cmpi", {"post": 15}),
("insn_cmpli", {"post": 15}),
("insn_cmp", {"post": 15}),
("insn_cmpl", {"post": 15}),

("insn_mtspr", {"post": 15}),
("insn_mfspr", {"post": 15}),
]

with multiprocessing.Pool(processes=args.jobs) as pool:
pool.starmap(run_check, checks)

@ -1 +0,0 @@
from .plat import *

@ -1,7 +1,8 @@
from amaranth import *
from amaranth.build import *
from amaranth.lib.cdc import ResetSynchronizer

from .. import tb
from power_fv.check import PowerFVCheck


__all__ = ["SymbiYosysPlatform"]
@ -25,9 +26,9 @@ class SymbiYosysPlatform(TemplatedPlatform):
* ``ghdl_opts``: adds options for the ``ghdl`` Yosys command.
* ``ghdl_top``: Top-level unit for the ``ghdl`` Yosys command (default: "top").
* ``prep_opts``: adds options for the ``prep`` Yosys command (default: "-flatten -nordff").
* ``chformal``: adds options for the ``chformal`` Yosys command (default: "-early").
* ``script_before_read``: inserts commands before reading input files in Yosys script.
* ``script_after_read``: inserts command after reading input files in Yosys script.
* ``script_after_synth``: inserts command after ``prep`` in Yosys script.

Build products:
(TODO)
@ -47,14 +48,14 @@ class SymbiYosysPlatform(TemplatedPlatform):
"{{name}}.sby": r"""
# {{autogenerated}}
[options]
mode {{get_override("mode")}}
mode {{get_override("mode")|default("bmc")}}
expect pass,fail
append 0
depth {{get_override("depth")}}
skip {{get_override("skip")}}

[engines]
smtbmc
smtbmc boolector

[files]
{% for file in platform.iter_files(".il", ".v", ".sv", ".vhdl") -%}
@ -79,8 +80,8 @@ class SymbiYosysPlatform(TemplatedPlatform):
read_ilang {{name}}.il
delete w:$verilog_initial_trigger
{{get_override("script_after_read")|default("# (script_after_read placeholder)")}}
prep {{get_override("prep_opts")|default("-flatten -nordff")}} -top {{name}}
chformal {{get_override("chformal_opts")|default("-early")}}
prep {{get_override("prep_opts")|default("-nordff")}} -top {{name}}
{{get_override("script_after_synth")|default("# (script_after_synth placeholder)")}}
""",
}
command_templates = [
@ -93,30 +94,18 @@ class SymbiYosysPlatform(TemplatedPlatform):
]

default_clk = "clk"
default_rst = "rst"
resources = [
Resource("clk", 0, Pins("clk", dir="i"), Clock(1e6)),
Resource("rst", 0, Pins("rst", dir="i")),
]
connectors = []

def create_missing_domain(self, name):
if name == "sync":
m = Module()
clk_i = self.request(self.default_clk).i
rst_i = self.request(self.default_rst).i
rst_i = Const(0)

m = Module()
m.domains.sync = ClockDomain("sync")
m.d.comb += [
ClockSignal("sync").eq(clk_i),
ResetSignal("sync").eq(rst_i),
]
m.d.comb += ClockSignal("sync").eq(clk_i)
m.submodules.reset_sync = ResetSynchronizer(rst_i, domain="sync")
return m

def build(self, top, mode="bmc", **kwargs):
if not isinstance(top, tb.Testbench):
raise TypeError("Top-level must be an instance of power_fv.tb.Testbench")

depth = str(top.bmc_depth)
skip = str(top.bmc_depth - 1)

return super().build(top, mode=mode, depth=depth, skip=skip, **kwargs)

@ -0,0 +1,73 @@
from abc import ABCMeta, abstractmethod
from pathlib import Path

from power_fv.build import sby


__all__ = ["PowerFVCheck"]


class PowerFVCheckMeta(ABCMeta):
all_checks = {}

def __new__(metacls, clsname, bases, namespace, name=None, **kwargs):
if name is not None:
if name in metacls.all_checks:
raise NameError("Check {!r} already exists".format(name))
namespace["name"] = name

cls = ABCMeta.__new__(metacls, clsname, bases, namespace, **kwargs)
if name is not None:
metacls.all_checks[name] = cls
cls.name = name
return cls

@classmethod
def find(cls, *name):
for check_name, check_cls in cls.all_checks.items():
assert isinstance(check_name, tuple)
if len(name) > len(check_name):
continue
if name == check_name[:len(name)]:
yield check_name, check_cls


class PowerFVCheck(metaclass=PowerFVCheckMeta):
@classmethod
def add_check_arguments(cls, parser):
parser.add_argument(
"name", metavar="NAME", type=str, help="name of the check")
parser.add_argument(
"--depth", type=int, default=15,
help="depth of the BMC, in clock cycles (default: %(default)s)")
parser.add_argument(
"--skip", type=int, default=None,
help="skip the specified number of clock cycles (default: DEPTH-1))")

@classmethod
def add_build_arguments(cls, parser):
parser.add_argument(
"--build-dir", type=Path, default=Path("./build"),
help="output directory (default: %(default)s)")

def __init__(self, *, depth, skip, core, **kwargs):
self.depth = depth
self.skip = skip if skip is not None else depth - 1
self.core = core
self.dut = core.wrapper(**kwargs)

@abstractmethod
def testbench(self):
raise NotImplementedError

def build(self, *, build_dir, **kwargs):
platform = sby.SymbiYosysPlatform()
self.core.add_files(platform, self.dut, **kwargs)

top = self.testbench()
build_dir = build_dir / top.name
overrides = {key: str(value) for key, value in kwargs.items()}
overrides["depth"] = str(self.depth)
overrides["skip"] = str(self.skip)

return platform.build(top, name=top.name, build_dir=build_dir, **overrides)

@ -0,0 +1,24 @@
from amaranth import *


__all__ = ["Timer"]


class Timer(Elaboratable):
def __init__(self, start):
if not isinstance(start, int) or start < 0:
raise TypeError("Start value must be a non-negative integer, not {!r}"
.format(start))

self.ctr = Signal(range(start + 1), reset=start, reset_less=True)
self.zero = Signal()

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

with m.If(self.ctr != 0):
m.d.sync += self.ctr.eq(self.ctr - 1)

m.d.comb += self.zero.eq(self.ctr == 0)

return m

@ -0,0 +1,4 @@
from .unique import *
from .cia import *
from .gpr import *
from .insn.all import *

@ -0,0 +1,56 @@
from amaranth import *
from amaranth.asserts import *

from power_fv.check import PowerFVCheck
from power_fv.check._timer import Timer


__all__ = ["CIACheck"]


class CIACheck(PowerFVCheck, name=("cia",)):
"""CIA check.

Given a pair of instructions retiring in order, the CIA of the second must match the NIA
of the first.
"""

def testbench(self):
return CIATestbench(self)


class CIATestbench(Elaboratable):
def __init__(self, check):
if not isinstance(check, CIACheck):
raise TypeError("Check must be an instance of CIACheck, not {!r}"
.format(check))
self.check = check
self.name = "cia_tb"

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

m.submodules.t_post = t_post = Timer(self.check.depth - 1)
m.submodules.dut = dut = self.check.dut

pred_stb = Signal()
pred_order = Signal(unsigned(64))
pred_nia = Signal(unsigned(64))

m.d.comb += pred_order.eq(AnyConst(64))

with m.If(dut.pfv.stb & (dut.pfv.order == pred_order)):
m.d.sync += [
pred_stb.eq(1),
pred_nia.eq(dut.pfv.nia)
]

with m.If(t_post.zero):
m.d.comb += [
Assume(dut.pfv.stb),
Assume(dut.pfv.order == pred_order + 1),
Assume(dut.pfv.order > 0),
Assert(pred_stb.implies(dut.pfv.cia == pred_nia)),
]

return m

@ -0,0 +1,100 @@
from amaranth import *
from amaranth.lib.coding import Encoder
from amaranth.asserts import *

from power_fv.check import PowerFVCheck
from power_fv.check._timer import Timer


__all__ = ["GPRCheck"]


class GPRCheck(PowerFVCheck, name=("gpr",)):
"""GPR consistency check.

Checks that:
* reads from a GPR return the last value that was written to it;
* writes to multiple GPRs by a single instruction (e.g. load with update) do not conflict
with each other.
"""

def testbench(self):
return GPRTestbench(self)


class GPRTestbench(Elaboratable):
def __init__(self, check):
if not isinstance(check, GPRCheck):
raise TypeError("Check must be an instance of GPRCheck, not {!r}"
.format(check))
self.check = check
self.name = "gpr_tb"

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

m.submodules.t_post = t_post = Timer(self.check.depth - 1)
m.submodules.dut = dut = self.check.dut

spec_order = AnyConst(dut.pfv.order.shape())
spec_index = AnyConst(unsigned(5))

gpr_write = Record([("ra", 1), ("rb", 1), ("rs", 1), ("rt", 1)])
gpr_read = Record.like(gpr_write)

m.d.comb += [
gpr_write.ra.eq(dut.pfv.ra.w_stb & (dut.pfv.ra.index == spec_index)),
gpr_write.rb.eq(dut.pfv.rb.w_stb & (dut.pfv.rb.index == spec_index)),
gpr_write.rs.eq(dut.pfv.rs.w_stb & (dut.pfv.rs.index == spec_index)),
gpr_write.rt.eq(dut.pfv.rt.w_stb & (dut.pfv.rt.index == spec_index)),

gpr_read .ra.eq(dut.pfv.ra.r_stb & (dut.pfv.ra.index == spec_index)),
gpr_read .rb.eq(dut.pfv.rb.r_stb & (dut.pfv.rb.index == spec_index)),
gpr_read .rs.eq(dut.pfv.rs.r_stb & (dut.pfv.rs.index == spec_index)),
gpr_read .rt.eq(dut.pfv.rt.r_stb & (dut.pfv.rt.index == spec_index)),
]

gpr_conflict = Record([("prev", 1), ("curr", 1)])
gpr_written = Record([("prev", 1)])
gpr_shadow = Record([("prev", 64)])

m.submodules.write_enc = write_enc = Encoder(len(gpr_write))
m.d.comb += write_enc.i.eq(gpr_write)

with m.If(dut.pfv.stb & write_enc.i.any() & write_enc.n):
# Write conflict: more then one bit of `gpr_write` is asserted.
m.d.comb += gpr_conflict.curr.eq(1)
m.d.sync += gpr_conflict.prev.eq(dut.pfv.order < spec_order)

with m.If(dut.pfv.stb & (dut.pfv.order < spec_order)):
with m.If(gpr_write.any()):
m.d.sync += gpr_written.prev.eq(1)
with m.If(gpr_write.ra):
m.d.sync += gpr_shadow.prev.eq(dut.pfv.ra.w_data)
with m.If(gpr_write.rb):
m.d.sync += gpr_shadow.prev.eq(dut.pfv.rb.w_data)
with m.If(gpr_write.rs):
m.d.sync += gpr_shadow.prev.eq(dut.pfv.rs.w_data)
with m.If(gpr_write.rt):
m.d.sync += gpr_shadow.prev.eq(dut.pfv.rt.w_data)

with m.If(t_post.zero):
m.d.comb += [
Assume(dut.pfv.stb),
Assume(dut.pfv.order == spec_order),
Assert(~gpr_conflict.curr),
Assert(~gpr_conflict.prev),
]
with m.If(gpr_written.prev):
with m.If(gpr_read.ra):
m.d.comb += Assert(dut.pfv.ra.r_data == gpr_shadow.prev)
with m.If(gpr_read.rb):
m.d.comb += Assert(dut.pfv.rb.r_data == gpr_shadow.prev)
with m.If(gpr_read.rs):
m.d.comb += Assert(dut.pfv.rs.r_data == gpr_shadow.prev)
with m.If(gpr_read.rt):
m.d.comb += Assert(dut.pfv.rt.r_data == gpr_shadow.prev)

m.d.comb += Assert(~Past(t_post.zero))

return m

@ -0,0 +1,204 @@
from amaranth import *
from amaranth.asserts import *

from power_fv.check import PowerFVCheck, PowerFVCheckMeta
from power_fv.check._timer import Timer


__all__ = ["InsnCheckMeta", "InsnCheck", "InsnTestbench"]


class InsnCheckMeta(PowerFVCheckMeta):
def __new__(metacls, clsname, bases, namespace, spec_cls=None, insn_cls=None, **kwargs):
if insn_cls is not None:
name = ("insn", insn_cls.__name__.lower())
else:
name = None

cls = PowerFVCheckMeta.__new__(metacls, clsname, bases, namespace, name=name, **kwargs)
if spec_cls is not None:
cls.spec_cls = spec_cls
if insn_cls is not None:
cls.insn_cls = insn_cls
return cls


class InsnCheck(PowerFVCheck, metaclass=InsnCheckMeta):
def __init__(self, *, depth, skip, core, **kwargs):
super().__init__(depth=depth, skip=skip, core=core, **kwargs)
self.insn = self.insn_cls()
self.spec = self.spec_cls(self.insn)

def testbench(self):
return InsnTestbench(self)


class InsnTestbench(Elaboratable):
def __init__(self, check):
if not isinstance(check, InsnCheck):
raise TypeError("Check must be an instance of InsnCheck, not {!r}"
.format(check))
self.check = check
self.name = "{}_tb".format("_".join(check.name))

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

m.submodules.t_post = t_post = Timer(self.check.depth - 1)
m.submodules.dut = dut = self.check.dut
m.submodules.spec = spec = self.check.spec

m.d.comb += [
spec.pfv.order.eq(dut.pfv.order),
spec.pfv.cia .eq(dut.pfv.cia),
]

with m.If(t_post.zero):
m.d.comb += [
Assume(dut.pfv.stb),
Assume(dut.pfv.insn == spec.pfv.insn),
Assert(dut.pfv.intr == spec.pfv.intr),
]

with m.If(t_post.zero & ~spec.pfv.intr):
m.d.comb += [
Assert(dut.pfv.nia == spec.pfv.nia),
]

m.submodules.ra = ra = _GPRFileTest(self.check, port="ra")
m.submodules.rb = rb = _GPRFileTest(self.check, port="rb")
m.submodules.rs = rs = _GPRFileTest(self.check, port="rs")
m.submodules.rt = rt = _GPRFileTest(self.check, port="rt")

m.d.comb += [
spec.pfv.ra.r_data.eq(dut.pfv.ra.r_data),
spec.pfv.rb.r_data.eq(dut.pfv.rb.r_data),
spec.pfv.rs.r_data.eq(dut.pfv.rs.r_data),
spec.pfv.rt.r_data.eq(dut.pfv.rt.r_data),
]

with m.If(t_post.zero & ~spec.pfv.intr):
m.d.comb += [
Assert(ra.valid.all()),
Assert(rb.valid.all()),
Assert(rs.valid.all()),
Assert(rt.valid.all()),
]

m.submodules.cr = cr = _SysRegTest(self.check, reg="cr" )
m.submodules.msr = msr = _SysRegTest(self.check, reg="msr" )
m.submodules.lr = lr = _SysRegTest(self.check, reg="lr" )
m.submodules.ctr = ctr = _SysRegTest(self.check, reg="ctr" )
m.submodules.tar = tar = _SysRegTest(self.check, reg="tar" )
m.submodules.xer = xer = _SysRegTest(self.check, reg="xer" )
m.submodules.srr0 = srr0 = _SysRegTest(self.check, reg="srr0")
m.submodules.srr1 = srr1 = _SysRegTest(self.check, reg="srr1")

m.d.comb += [
spec.pfv.cr .r_data.eq(dut.pfv.cr .r_data),
spec.pfv.msr .r_data.eq(dut.pfv.msr .r_data),
spec.pfv.lr .r_data.eq(dut.pfv.lr .r_data),
spec.pfv.ctr .r_data.eq(dut.pfv.ctr .r_data),
spec.pfv.tar .r_data.eq(dut.pfv.tar .r_data),
spec.pfv.xer .r_data.eq(dut.pfv.xer .r_data),
spec.pfv.srr0.r_data.eq(dut.pfv.srr0.r_data),
spec.pfv.srr1.r_data.eq(dut.pfv.srr1.r_data),
]

with m.If(t_post.zero & ~spec.pfv.intr):
m.d.comb += [
Assert(cr .valid.all()),
Assert(msr .valid.all()),
Assert(lr .valid.all()),
Assert(ctr .valid.all()),
Assert(tar .valid.all()),
Assert(xer .valid.all()),
Assert(srr0.valid.all()),
Assert(srr1.valid.all()),
]

m.d.comb += Assert(~Past(t_post.zero))

return m


class _GPRFileTest(Elaboratable):
def __init__(self, check, *, port):
self._dut = getattr(check.dut .pfv, port)
self._spec = getattr(check.spec.pfv, port)

self.valid = Record([
("read" , [("index", 1), ("r_stb", 1)]),
("write", [("index", 1), ("w_stb", 1), ("w_data", 1)]),
])

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

dut = Record.like(self._dut )
spec = Record.like(self._spec)

m.d.comb += [
dut .eq(self._dut ),
spec.eq(self._spec),

# If the spec reads from a GPR, the DUT must read it too.
self.valid.read.index.eq(spec.r_stb.implies(dut.index == spec.index)),
self.valid.read.r_stb.eq(spec.r_stb.implies(dut.r_stb)),

# The DUT and the spec must write the same value to the same GPR.
self.valid.write.index .eq(spec.w_stb.implies(dut.index == spec.index)),
self.valid.write.w_stb .eq(spec.w_stb == dut.w_stb),
self.valid.write.w_data.eq(spec.w_stb.implies(dut.w_data == spec.w_data)),
]

return m


class _SysRegTest(Elaboratable):
def __init__(self, check, *, reg):
self._dut = getattr(check.dut .pfv, reg)
self._spec = getattr(check.spec.pfv, reg)

self.valid = Record([
("read" , [("r_mask", 1)]),
("write", [("w_mask", 1), ("w_data", 1), ("r_mask", 1), ("r_data", 1)]),
])

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

dut = Record([
("r_mask", len(self._dut.r_mask)),
("r_data", len(self._dut.r_data)),
("w_mask", len(self._dut.w_mask)),
("w_data", len(self._dut.w_data)),
])
spec = Record.like(dut)
keep = Record([
("w_mask", len(self._dut.w_mask)),
])

def contains(a, mask, b=None):
if b is None:
b = mask
return a & mask == b & mask

m.d.comb += [
dut .eq(self._dut ),
spec.eq(self._spec),

# The DUT and the spec must read from the same bits.
self.valid.read.r_mask.eq(contains(dut.r_mask, spec.r_mask)),

# The DUT and the spec must write the same values to the same bits.
self.valid.write.w_mask.eq(contains(dut.w_mask, spec.w_mask)),
self.valid.write.w_data.eq(contains(dut.w_data, spec.w_mask, spec.w_data)),

# The DUT may write to more bits than the spec iff their values are preserved.
keep.w_mask.eq(dut.w_mask & ~spec.w_mask),
self.valid.write.r_mask.eq(contains(dut.r_mask, keep.w_mask)),
self.valid.write.r_data.eq(contains(dut.r_data, keep.w_mask, dut.w_data)),
]

return m

@ -0,0 +1,73 @@
from power_fv.insn import const
from power_fv.insn.spec.addsub import AddSubSpec
from power_fv.check.insn import InsnCheck


__all__ = [
"ADDI" , "ADDIS" , "ADDPCIS",
"ADD" , "ADD_" , "ADDO" , "ADDO_" , "ADDIC" , "ADDIC_",
"SUBF" , "SUBF_" , "SUBFO" , "SUBFO_" , "SUBFIC",
"ADDC" , "ADDC_" , "ADDCO" , "ADDCO_" ,
"ADDE" , "ADDE_" , "ADDEO" , "ADDEO_" ,
"SUBFC" , "SUBFC_" , "SUBFCO" , "SUBFCO_" ,
"SUBFE" , "SUBFE_" , "SUBFEO" , "SUBFEO_" ,
"ADDME" , "ADDME_" , "ADDMEO" , "ADDMEO_" ,
"ADDZE" , "ADDZE_" , "ADDZEO" , "ADDZEO_" ,
"SUBFME", "SUBFME_", "SUBFMEO", "SUBFMEO_",
"SUBFZE", "SUBFZE_", "SUBFZEO", "SUBFZEO_",
"ADDEX" ,
"NEG" , "NEG_" , "NEGO" , "NEGO_" ,
]


class ADDI (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDI ): pass
class ADDIS (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDIS ): pass
class ADDPCIS (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDPCIS ): pass
class ADD (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADD ): pass
class ADD_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADD_ ): pass
class ADDO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDO ): pass
class ADDO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDO_ ): pass
class ADDIC (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDIC ): pass
class ADDIC_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDIC_ ): pass
class SUBF (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBF ): pass
class SUBF_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBF_ ): pass
class SUBFO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFO ): pass
class SUBFO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFO_ ): pass
class SUBFIC (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFIC ): pass
class ADDC (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDC ): pass
class ADDC_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDC_ ): pass
class ADDCO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDCO ): pass
class ADDCO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDCO_ ): pass
class ADDE (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDE ): pass
class ADDE_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDE_ ): pass
class ADDEO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDEO ): pass
class ADDEO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDEO_ ): pass
class SUBFC (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFC ): pass
class SUBFC_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFC_ ): pass
class SUBFCO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFCO ): pass
class SUBFCO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFCO_ ): pass
class SUBFE (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFE ): pass
class SUBFE_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFE_ ): pass
class SUBFEO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFEO ): pass
class SUBFEO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFEO_ ): pass
class ADDME (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDME ): pass
class ADDME_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDME_ ): pass
class ADDMEO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDMEO ): pass
class ADDMEO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDMEO_ ): pass
class ADDZE (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDZE ): pass
class ADDZE_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDZE_ ): pass
class ADDZEO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDZEO ): pass
class ADDZEO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDZEO_ ): pass
class SUBFME (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFME ): pass
class SUBFME_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFME_ ): pass
class SUBFMEO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFMEO ): pass
class SUBFMEO_(InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFMEO_): pass
class SUBFZE (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFZE ): pass
class SUBFZE_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFZE_ ): pass
class SUBFZEO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFZEO ): pass
class SUBFZEO_(InsnCheck, spec_cls=AddSubSpec, insn_cls=const.SUBFZEO_): pass
class ADDEX (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.ADDEX ): pass
class NEG (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.NEG ): pass
class NEG_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.NEG_ ): pass
class NEGO (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.NEGO ): pass
class NEGO_ (InsnCheck, spec_cls=AddSubSpec, insn_cls=const.NEGO_ ): pass

@ -0,0 +1,5 @@
from .addsub import *
from .branch import *
from .cr import *
from .compare import *
from .spr import *

@ -0,0 +1,30 @@
from power_fv.insn import const
from power_fv.insn.spec.branch import BranchSpec
from power_fv.check.insn import InsnCheck


__all__ = [
"B" , "BA" , "BL" , "BLA" ,
"BC", "BCA", "BCL", "BCLA",
"BCLR" , "BCLRL" ,
"BCCTR", "BCCTRL",
"BCTAR", "BCTARL",
]


class B (InsnCheck, spec_cls=BranchSpec, insn_cls=const.B ): pass
class BA (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BA ): pass
class BL (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BL ): pass
class BLA (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BLA ): pass

class BC (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BC ): pass
class BCA (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCA ): pass
class BCL (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCL ): pass
class BCLA (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCLA): pass

class BCLR (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCLR ): pass
class BCLRL (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCLRL ): pass
class BCCTR (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCCTR ): pass
class BCCTRL(InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCCTRL): pass
class BCTAR (InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCTAR ): pass
class BCTARL(InsnCheck, spec_cls=BranchSpec, insn_cls=const.BCTARL): pass

@ -0,0 +1,14 @@
from power_fv.insn import const
from power_fv.insn.spec.compare import CompareSpec
from power_fv.check.insn import InsnCheck


__all__ = [
"CMPI", "CMPLI", "CMP", "CMPL",
]


class CMPI (InsnCheck, spec_cls=CompareSpec, insn_cls=const.CMPI ): pass
class CMPLI (InsnCheck, spec_cls=CompareSpec, insn_cls=const.CMPLI): pass
class CMP (InsnCheck, spec_cls=CompareSpec, insn_cls=const.CMP ): pass
class CMPL (InsnCheck, spec_cls=CompareSpec, insn_cls=const.CMPL ): pass

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


__all__ = [
"CRAND", "CROR", "CRNAND", "CRXOR", "CRNOR", "CRANDC", "CREQV", "CRORC",
"MCRF" ,
]


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

@ -0,0 +1,27 @@
from power_fv.insn import const
from power_fv.insn.spec.spr import SPRMoveSpec
from power_fv.check.insn import InsnCheck


__all__ = [
"MTXER" , "MFXER" ,
"MTLR" , "MFLR" ,
"MTCTR" , "MFCTR" ,
"MTSRR0", "MFSRR0",
"MTSRR1", "MFSRR1",
"MTTAR" , "MFTAR" ,
]


class MTXER (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MTXER ): pass
class MFXER (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MFXER ): pass
class MTLR (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MTLR ): pass
class MFLR (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MFLR ): pass
class MTCTR (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MTCTR ): pass
class MFCTR (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MFCTR ): pass
class MTSRR0(InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MTSRR0): pass
class MFSRR0(InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MFSRR0): pass
class MTSRR1(InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MTSRR1): pass
class MFSRR1(InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MFSRR1): pass
class MTTAR (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MTTAR ): pass
class MFTAR (InsnCheck, spec_cls=SPRMoveSpec, insn_cls=const.MFTAR ): pass

@ -0,0 +1,60 @@
from amaranth import *
from amaranth.asserts import *

from power_fv.check import PowerFVCheck
from power_fv.check._timer import Timer


__all__ = ["UniquenessCheck"]


class UniquenessCheck(PowerFVCheck, name=("unique",)):
"""Uniqueness check.

Checks that every retired instruction is assigned an unique `pfv.order` value.
"""

def testbench(self):
return UniquenessTestbench(self)


class UniquenessTestbench(Elaboratable):
def __init__(self, check):
if not isinstance(check, UniquenessCheck):
raise TypeError("Check must be an instance of UniquenessCheck, not {!r}"
.format(check))
self.check = check
self.name = "unique_tb"

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

m.submodules.t_pre = t_pre = Timer(self.check.skip - 1)
m.submodules.t_post = t_post = Timer(self.check.depth - 1)
m.submodules.dut = dut = self.check.dut

spec_order = AnyConst(dut.pfv.order.shape())
duplicate = Record([("prev", 1), ("curr", 1)])

with m.If(Rose(t_pre.zero)):
m.d.comb += [
Assume(dut.pfv.stb),
Assume(dut.pfv.order == spec_order),
Assert(~duplicate.prev),
Assert(~duplicate.curr),
]

with m.Elif(t_pre.zero):
with m.If(dut.pfv.stb & (dut.pfv.order == spec_order)):
m.d.sync += duplicate.prev.eq(1)
m.d.comb += duplicate.curr.eq(1)

with m.If(t_post.zero):
m.d.comb += [
Assert(~duplicate.prev),
Assert(~duplicate.curr),
]

m.d.comb += Assert(~Past(t_post.zero))

return m

@ -1,12 +0,0 @@
class PowerFVCheck:
registry = {}
name = None

def __init_subclass__(cls, name):
if name in cls.registry:
raise ValueError("Check name {!r} is already registered".format(name))
cls.registry[name] = cls
cls.name = name