diff --git a/cores/microwatt/README.md b/cores/microwatt/README.md index b0750ce..4317d7e 100644 --- a/cores/microwatt/README.md +++ b/cores/microwatt/README.md @@ -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 ``` diff --git a/cores/microwatt/_wrapper.py b/cores/microwatt/_wrapper.py deleted file mode 100644 index f34a933..0000000 --- a/cores/microwatt/_wrapper.py +++ /dev/null @@ -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 diff --git a/cores/microwatt/checks.pfv b/cores/microwatt/checks.pfv new file mode 100644 index 0000000..087cba7 --- /dev/null +++ b/cores/microwatt/checks.pfv @@ -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 diff --git a/cores/microwatt/microwatt.py b/cores/microwatt/microwatt.py new file mode 100644 index 0000000..6b05e72 --- /dev/null +++ b/cores/microwatt/microwatt.py @@ -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() diff --git a/cores/microwatt/microwatt_top.vhdl b/cores/microwatt/microwatt_top.vhdl deleted file mode 100644 index 29374e9..0000000 --- a/cores/microwatt/microwatt_top.vhdl +++ /dev/null @@ -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; diff --git a/cores/microwatt/run.py b/cores/microwatt/run.py deleted file mode 100644 index 21be517..0000000 --- a/cores/microwatt/run.py +++ /dev/null @@ -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) diff --git a/power_fv/build/__init__.py b/power_fv/build/__init__.py index 2aadad1..e69de29 100644 --- a/power_fv/build/__init__.py +++ b/power_fv/build/__init__.py @@ -1 +0,0 @@ -from .plat import * diff --git a/power_fv/build/plat.py b/power_fv/build/sby.py similarity index 78% rename from power_fv/build/plat.py rename to power_fv/build/sby.py index 6994f8f..d119dc8 100644 --- a/power_fv/build/plat.py +++ b/power_fv/build/sby.py @@ -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) diff --git a/power_fv/check/__init__.py b/power_fv/check/__init__.py new file mode 100644 index 0000000..12131d7 --- /dev/null +++ b/power_fv/check/__init__.py @@ -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) diff --git a/power_fv/check/_timer.py b/power_fv/check/_timer.py new file mode 100644 index 0000000..6a9aa51 --- /dev/null +++ b/power_fv/check/_timer.py @@ -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 diff --git a/power_fv/check/all.py b/power_fv/check/all.py new file mode 100644 index 0000000..1a32d57 --- /dev/null +++ b/power_fv/check/all.py @@ -0,0 +1,4 @@ +from .unique import * +from .cia import * +from .gpr import * +from .insn.all import * diff --git a/power_fv/check/cia.py b/power_fv/check/cia.py new file mode 100644 index 0000000..a6dbe1d --- /dev/null +++ b/power_fv/check/cia.py @@ -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 diff --git a/power_fv/check/gpr.py b/power_fv/check/gpr.py new file mode 100644 index 0000000..3c6acc4 --- /dev/null +++ b/power_fv/check/gpr.py @@ -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 diff --git a/power_fv/check/insn/__init__.py b/power_fv/check/insn/__init__.py new file mode 100644 index 0000000..3ff867a --- /dev/null +++ b/power_fv/check/insn/__init__.py @@ -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 diff --git a/power_fv/check/insn/addsub.py b/power_fv/check/insn/addsub.py new file mode 100644 index 0000000..eeda7cd --- /dev/null +++ b/power_fv/check/insn/addsub.py @@ -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 diff --git a/power_fv/check/insn/all.py b/power_fv/check/insn/all.py new file mode 100644 index 0000000..f6a532d --- /dev/null +++ b/power_fv/check/insn/all.py @@ -0,0 +1,5 @@ +from .addsub import * +from .branch import * +from .cr import * +from .compare import * +from .spr import * diff --git a/power_fv/check/insn/branch.py b/power_fv/check/insn/branch.py new file mode 100644 index 0000000..10d4913 --- /dev/null +++ b/power_fv/check/insn/branch.py @@ -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 diff --git a/power_fv/check/insn/compare.py b/power_fv/check/insn/compare.py new file mode 100644 index 0000000..142af87 --- /dev/null +++ b/power_fv/check/insn/compare.py @@ -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 diff --git a/power_fv/check/insn/cr.py b/power_fv/check/insn/cr.py new file mode 100644 index 0000000..2c90f3b --- /dev/null +++ b/power_fv/check/insn/cr.py @@ -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 diff --git a/power_fv/check/insn/spr.py b/power_fv/check/insn/spr.py new file mode 100644 index 0000000..5249063 --- /dev/null +++ b/power_fv/check/insn/spr.py @@ -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 diff --git a/power_fv/check/unique.py b/power_fv/check/unique.py new file mode 100644 index 0000000..5907a0d --- /dev/null +++ b/power_fv/check/unique.py @@ -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 diff --git a/power_fv/checks/__init__.py b/power_fv/checks/__init__.py deleted file mode 100644 index 2941bd1..0000000 --- a/power_fv/checks/__init__.py +++ /dev/null @@ -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 - - def get_testbench(self, dut, *args, **kwargs): - raise NotImplementedError diff --git a/power_fv/checks/all.py b/power_fv/checks/all.py deleted file mode 100644 index eee112e..0000000 --- a/power_fv/checks/all.py +++ /dev/null @@ -1,2 +0,0 @@ -from .cons.all import * -from .insn.all import * diff --git a/power_fv/checks/cons/all.py b/power_fv/checks/cons/all.py deleted file mode 100644 index e819cf8..0000000 --- a/power_fv/checks/cons/all.py +++ /dev/null @@ -1,5 +0,0 @@ -from .unique import * -from .ia_fwd import * -from .gpr import * -from .cr import * -from .spr.all import * diff --git a/power_fv/checks/cons/cr.py b/power_fv/checks/cons/cr.py deleted file mode 100644 index c289fa1..0000000 --- a/power_fv/checks/cons/cr.py +++ /dev/null @@ -1,78 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - - -__all__ = ["CRSpec", "CRCheck"] - - -class CRSpec(Elaboratable): - """Condition Register consistency specification. - - Checks that reads from CR fields return the last value that was written to them. - """ - def __init__(self, post): - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spec_order = AnyConst(self.pfv.order.width) - - cr_map = Array( - Record([ - ("pfv", [ - ("r_stb", 1), - ("r_data", 4), - ("w_stb", 1), - ("w_data", 4), - ]), - ("written", 1), - ("shadow", 4), - ], name=f"cr_{i}") for i in range(8) - ) - - cr_written_any = 0 - - for i, cr_field in enumerate(cr_map): - m.d.comb += [ - cr_field.pfv.r_stb .eq(self.pfv.cr.r_stb[i]), - cr_field.pfv.r_data.eq(self.pfv.cr.r_data.word_select(i, 4)), - cr_field.pfv.w_stb .eq(self.pfv.cr.w_stb[i]), - cr_field.pfv.w_data.eq(self.pfv.cr.w_data.word_select(i, 4)), - ] - cr_written_any |= cr_field.written - - with m.If(self.pfv.stb & ~self.pfv.intr & (self.pfv.order <= spec_order)): - for cr_field in cr_map: - with m.If(cr_field.pfv.w_stb): - m.d.sync += [ - cr_field.written.eq(1), - cr_field.shadow .eq(cr_field.pfv.w_data), - ] - - with m.If(self.post.stb): - m.d.sync += [ - Assume(Past(self.pfv.stb)), - Assume(Past(self.pfv.order) == spec_order), - Assume(cr_written_any), - ] - with m.If(~Past(self.pfv.intr)): - for cr_field in cr_map: - with m.If(Past(cr_field.pfv.r_stb)): - m.d.sync += Assert(Past(cr_field.pfv.r_data) == Past(cr_field.shadow)) - - return m - - -class CRCheck(PowerFVCheck, name="cons_cr"): - def get_testbench(self, dut, post): - tb_spec = CRSpec(post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/cons/gpr.py b/power_fv/checks/cons/gpr.py deleted file mode 100644 index 302e667..0000000 --- a/power_fv/checks/cons/gpr.py +++ /dev/null @@ -1,85 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - - -__all__ = ["GPRSpec", "GPRCheck"] - - -class GPRSpec(Elaboratable): - """GPR consistency specification. - - 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 target the - same register. - """ - def __init__(self, post): - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spec_order = AnyConst(self.pfv.order.width) - spec_gpr_index = AnyConst(5) - - gpr_ra_read = Signal() - gpr_ra_write = Signal() - gpr_rb_read = Signal() - gpr_rs_read = Signal() - gpr_rt_read = Signal() - gpr_rt_write = Signal() - - gpr_conflict = Signal() - gpr_written = Signal() - gpr_shadow = Signal(64) - - m.d.comb += [ - gpr_ra_read .eq(self.pfv.ra.r_stb & (self.pfv.ra.index == spec_gpr_index)), - gpr_ra_write.eq(self.pfv.ra.w_stb & (self.pfv.ra.index == spec_gpr_index)), - gpr_rb_read .eq(self.pfv.rb.r_stb & (self.pfv.rb.index == spec_gpr_index)), - gpr_rs_read .eq(self.pfv.rs.r_stb & (self.pfv.rs.index == spec_gpr_index)), - gpr_rt_read .eq(self.pfv.rt.r_stb & (self.pfv.rt.index == spec_gpr_index)), - gpr_rt_write.eq(self.pfv.rt.w_stb & (self.pfv.rt.index == spec_gpr_index)), - ] - - with m.If(self.pfv.stb & ~self.pfv.intr & (self.pfv.order <= spec_order)): - with m.If(gpr_ra_write & gpr_rt_write): - m.d.sync += gpr_conflict.eq(1) - with m.If(gpr_ra_write | gpr_rt_write): - m.d.sync += gpr_written.eq(1) - with m.If(gpr_ra_write): - m.d.sync += gpr_shadow.eq(self.pfv.ra.w_data) - with m.Else(): - m.d.sync += gpr_shadow.eq(self.pfv.rt.w_data) - - with m.If(self.post.stb): - m.d.sync += [ - Assume(Past(self.pfv.stb)), - Assume(Past(self.pfv.order) == spec_order), - ] - with m.If(~Past(self.pfv.intr)): - m.d.sync += Assert(gpr_written.implies(~gpr_conflict)) - with m.If(gpr_written & Past(gpr_ra_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.ra.r_data)) - with m.If(gpr_written & Past(gpr_rb_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rb.r_data)) - with m.If(gpr_written & Past(gpr_rs_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rs.r_data)) - with m.If(gpr_written & Past(gpr_rt_read)): - m.d.sync += Assert(Past(gpr_shadow) == Past(self.pfv.rt.r_data)) - - return m - - -class GPRCheck(PowerFVCheck, name="cons_gpr"): - def get_testbench(self, dut, post): - tb_spec = GPRSpec(post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/cons/ia_fwd.py b/power_fv/checks/cons/ia_fwd.py deleted file mode 100644 index a96a8cb..0000000 --- a/power_fv/checks/cons/ia_fwd.py +++ /dev/null @@ -1,52 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - - -__all__ = ["IAForwardSpec", "IAForwardCheck"] - - -class IAForwardSpec(Elaboratable): - """IA forward specification. - - Given two instructions retiring in order, the NIA of the first must match the CIA - of the second. - """ - def __init__(self, post): - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - pred_order = AnyConst(self.pfv.order.width) - pred_stb = Signal() - pred_nia = Signal.like(self.pfv.nia) - - with m.If(self.pfv.stb & (self.pfv.order == pred_order)): - m.d.sync += [ - pred_stb.eq(1), - pred_nia.eq(self.pfv.nia) - ] - - with m.If(self.post.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(self.pfv.order == pred_order + 1), - Assume(self.pfv.order > 0), - Assert(pred_stb.implies(self.pfv.cia == pred_nia)), - ] - - return m - - -class IAForwardCheck(PowerFVCheck, name="cons_ia_fwd"): - def get_testbench(self, dut, post): - tb_spec = IAForwardSpec(post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/cons/spr/__init__.py b/power_fv/checks/cons/spr/__init__.py deleted file mode 100644 index e69de29..0000000 diff --git a/power_fv/checks/cons/spr/_storage.py b/power_fv/checks/cons/spr/_storage.py deleted file mode 100644 index 44967cf..0000000 --- a/power_fv/checks/cons/spr/_storage.py +++ /dev/null @@ -1,77 +0,0 @@ -from collections import OrderedDict - -from amaranth import * -from amaranth.asserts import * - -from ... import PowerFVCheck -from .... import pfv, tb - - -__all__ = ["SPRSpec", "SPRCheck"] - - -class StorageSPRSpec(Elaboratable): - """Storage SPR specification. - - Checks that reads from supported SPRs return the last value that was written to them. - """ - def __init__(self, spr_name, spr_reset, post): - self.spr_name = spr_name - self.spr_reset = spr_reset - - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - @property - def pfv_spr(self): - return getattr(self.pfv, self.spr_name) - - def elaborate(self, platform): - m = Module() - - spr = Record([ - ("written", 1), - ("shadow", self.pfv_spr.r_data.width), - ], name=self.spr_name) - - spec_order = AnyConst(self.pfv.order.width) - - with m.If(Initial()): - m.d.sync += Assume(spr.shadow == self.spr_reset) - - with m.If(self.pfv.stb & (self.pfv.order <= spec_order)): - with m.If(self.pfv_spr.w_mask.any()): - m.d.sync += [ - spr.written.eq(1), - spr.shadow .eq((spr.shadow & ~self.pfv_spr.w_mask) | (self.pfv_spr.w_data & self.pfv_spr.w_mask)), - ] - - with m.If(self.post.stb): - m.d.sync += [ - Assume(Past(self.pfv.stb)), - Assume(Past(self.pfv.order) == spec_order), - ] - - with m.If(spr.written): - p_spr_r_mask = Past(self.pfv_spr.r_mask) - p_spr_r_data = Past(self.pfv_spr.r_data) - p_spr_shadow = Past(spr.shadow) - m.d.sync += Assert((p_spr_r_data & p_spr_r_mask) == (p_spr_shadow & p_spr_r_mask)) - - m.d.sync += Assume(spr.written & Past(self.pfv_spr.r_mask).any()) # FIXME rm - - return m - - -class StorageSPRCheck(PowerFVCheck, name="_cons_spr_storage"): - def __init_subclass__(cls, name, spr_name): - super().__init_subclass__(name) - cls.spr_name = spr_name - - def get_testbench(self, dut, post, spr_reset=0): - tb_spec = StorageSPRSpec(self.spr_name, spr_reset, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/cons/spr/all.py b/power_fv/checks/cons/spr/all.py deleted file mode 100644 index 89fb27b..0000000 --- a/power_fv/checks/cons/spr/all.py +++ /dev/null @@ -1,9 +0,0 @@ -from ._storage import StorageSPRCheck - - -class LR (StorageSPRCheck, name="cons_lr", spr_name="lr" ): pass -class CTR (StorageSPRCheck, name="cons_ctr", spr_name="ctr" ): pass -class XER (StorageSPRCheck, name="cons_xer", spr_name="xer" ): pass -class TAR (StorageSPRCheck, name="cons_tar", spr_name="tar" ): pass -class SRR0 (StorageSPRCheck, name="cons_srr0", spr_name="srr0"): pass -class SRR1 (StorageSPRCheck, name="cons_srr1", spr_name="srr1"): pass diff --git a/power_fv/checks/cons/unique.py b/power_fv/checks/cons/unique.py deleted file mode 100644 index 92edce2..0000000 --- a/power_fv/checks/cons/unique.py +++ /dev/null @@ -1,49 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - - -__all__ = ["UniquenessSpec", "UniquenessCheck"] - - -class UniquenessSpec(Elaboratable): - """Uniqueness specification. - - A core cannot retire two instructions that share the same `pfv.order` identifier. - """ - def __init__(self, pre, post): - self.pfv = pfv.Interface() - self.pre = tb.Trigger(cycle=pre) - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield from (self.pre, self.post) - - def elaborate(self, platform): - m = Module() - - spec_order = AnyConst(self.pfv.order.shape()) - duplicate = Signal() - - with m.If(self.pre.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(spec_order == self.pfv.order), - Assume(~duplicate), - ] - with m.Elif(self.pfv.stb & (self.pfv.order == spec_order)): - m.d.sync += duplicate.eq(1) - - with m.If(self.post.stb): - m.d.sync += Assert(~duplicate) - - return m - - -class UniquenessCheck(PowerFVCheck, name="cons_unique"): - def get_testbench(self, dut, pre, post): - tb_spec = UniquenessSpec(pre, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/insn/__init__.py b/power_fv/checks/insn/__init__.py deleted file mode 100644 index e69de29..0000000 diff --git a/power_fv/checks/insn/_addsub.py b/power_fv/checks/insn/_addsub.py deleted file mode 100644 index 630c9b7..0000000 --- a/power_fv/checks/insn/_addsub.py +++ /dev/null @@ -1,370 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - -from ._fmt import * -from ._insn import * - - -__all__ = ["AddSubtractSpec", "AddSubtractCheck"] - - -class AddSubtractSpec(Elaboratable): - def __init__(self, insn_cls, post): - self.insn_cls = insn_cls - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spec_insn = self.insn_cls() - - with m.If(self.post.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(self.pfv.insn[32:] == spec_insn), - ] - - spec_ra_r_stb = Signal() - spec_rb_r_stb = Signal() - spec_rt_w_stb = Signal() - spec_rt_w_data = Signal(64) - spec_cr_w_stb = Signal( 8) - spec_cr_w_data = Signal(32) - spec_msr_r_mask = Signal(64) - spec_xer_r_mask = Signal(64) - spec_xer_w_mask = Signal(64) - spec_xer_w_data = Signal(64) - - src_a = Signal(signed(64)) - src_b = Signal(signed(64)) - src_c = Signal() - result = Signal(unsigned(65)) - - ca_64 = Signal() - ca_32 = Signal() - ov_64 = Signal() - ov_32 = Signal() - - # Operand A : (RA) or 0 or NIA or ~(RA) - - if isinstance(spec_insn, (ADDI, ADDIS)): - m.d.comb += [ - spec_ra_r_stb.eq(spec_insn.ra != 0), - src_a.eq(Mux(spec_insn.ra != 0, self.pfv.ra.r_data, 0)), - ] - elif isinstance(spec_insn, ADDPCIS): - m.d.comb += [ - spec_ra_r_stb.eq(0), - src_a.eq(self.pfv.nia), - ] - elif isinstance(spec_insn, ( - ADD , ADD_ , ADDO , ADDO_ , - ADDIC, ADDIC_, - ADDC , ADDC_ , ADDCO , ADDCO_ , - ADDE , ADDE_ , ADDEO , ADDEO_ , - ADDME, ADDME_, ADDMEO, ADDMEO_, - ADDZE, ADDZE_, ADDZEO, ADDZEO_, - ADDEX, - )): - m.d.comb += [ - spec_ra_r_stb.eq(1), - src_a.eq(self.pfv.ra.r_data), - ] - elif isinstance(spec_insn, ( - SUBF , SUBF_ , SUBFO , SUBFO_ , - SUBFIC, - SUBFC , SUBFC_ , SUBFCO , SUBFCO_ , - SUBFE , SUBFE_ , SUBFEO , SUBFEO_ , - SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, - SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, - NEG , NEG_ , NEGO , NEGO_ , - )): - m.d.comb += [ - spec_ra_r_stb.eq(1), - src_a.eq(~self.pfv.ra.r_data), - ] - else: - assert False - - # Operand B : SI or SI<<16 or D<<16 or (RB) or -1 or 0 - - if isinstance(spec_insn, (ADDI, ADDIC, ADDIC_, SUBFIC)): - m.d.comb += [ - spec_rb_r_stb.eq(0), - src_b.eq(spec_insn.si), - ] - elif isinstance(spec_insn, ADDIS): - m.d.comb += [ - spec_rb_r_stb.eq(0), - src_b.eq(Cat(Const(0, 16), spec_insn.si).as_signed()), - ] - elif isinstance(spec_insn, ADDPCIS): - imm_d = Signal(signed(16)) - m.d.comb += [ - spec_rb_r_stb.eq(0), - imm_d.eq(Cat(spec_insn.d2, spec_insn.d1, spec_insn.d0)), - src_b.eq(Cat(Const(0, 16), imm_d).as_signed()), - ] - elif isinstance(spec_insn, ( - ADD , ADD_ , ADDO , ADDO_ , - SUBF , SUBF_ , SUBFO , SUBFO_ , - ADDC , ADDC_ , ADDCO , ADDCO_ , - ADDE , ADDE_ , ADDEO , ADDEO_ , - SUBFC, SUBFC_, SUBFCO, SUBFCO_, - SUBFE, SUBFE_, SUBFEO, SUBFEO_, - ADDEX, - )): - m.d.comb += [ - spec_rb_r_stb.eq(1), - src_b.eq(self.pfv.rb.r_data), - ] - elif isinstance(spec_insn, ( - ADDME , ADDME_ , ADDMEO , ADDMEO_ , - SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, - )): - m.d.comb += [ - spec_rb_r_stb.eq(0), - src_b.eq(-1), - ] - elif isinstance(spec_insn, ( - ADDZE , ADDZE_ , ADDZEO , ADDZEO_ , - SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, - NEG , NEG_ , NEGO , NEGO_ , - )): - m.d.comb += [ - spec_rb_r_stb.eq(0), - src_b.eq(0), - ] - else: - assert False - - # Operand C : 0 or 1 or XER.CA or XER.OV - - if isinstance(spec_insn, ( - ADDI , ADDIS , ADDPCIS, - ADD , ADD_ , ADDO , ADDO_ , - ADDIC, ADDIC_, - ADDC , ADDC_ , ADDCO , ADDCO_, - )): - m.d.comb += src_c.eq(0) - elif isinstance(spec_insn, ( - SUBF , SUBF_ , SUBFO , SUBFO_ , - SUBFIC, - SUBFC , SUBFC_, SUBFCO, SUBFCO_, - NEG , NEG_ , NEGO , NEGO_ , - )): - m.d.comb += src_c.eq(1) - elif isinstance(spec_insn, ( - ADDE , ADDE_ , ADDEO , ADDEO_ , - SUBFE , SUBFE_ , SUBFEO , SUBFEO_ , - ADDME , ADDME_ , ADDMEO , ADDMEO_ , - ADDZE , ADDZE_ , ADDZEO , ADDZEO_ , - SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, - SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, - )): - m.d.comb += [ - spec_xer_r_mask[63 - 34].eq(1), # XER.CA - src_c.eq(self.pfv.xer.r_data[63 - 34]), - ] - elif isinstance(spec_insn, ADDEX): - m.d.comb += [ - spec_xer_r_mask[63 - 33].eq(1), # XER.OV - src_c.eq(self.pfv.xer.r_data[63 - 33]), - ] - else: - assert False - - # Result : Operand A + Operand B + Operand C - - tmp_a = Signal(unsigned(65)) - tmp_b = Signal(unsigned(65)) - - m.d.comb += [ - tmp_a .eq(src_a.as_unsigned()), - tmp_b .eq(src_b.as_unsigned()), - result.eq(tmp_a + tmp_b + src_c), - - ca_64.eq(result[64]), - ca_32.eq(result[32] ^ src_a[32] ^ src_b[32]), - ov_64.eq((ca_64 ^ result[63]) & ~(src_a[63] ^ src_b[63])), - ov_32.eq((ca_32 ^ result[31]) & ~(src_a[31] ^ src_b[31])), - ] - - # GPRs - - m.d.comb += [ - spec_rt_w_stb .eq(1), - spec_rt_w_data.eq(result[:64]), - ] - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert(spec_ra_r_stb.implies(self.pfv.ra.r_stb)), - Assert(spec_rb_r_stb.implies(self.pfv.rb.r_stb)), - Assert(self.pfv.rt.w_stb == spec_rt_w_stb), - Assert(spec_rt_w_stb.implies(self.pfv.rt.w_data == spec_rt_w_data)), - ] - - # MSR - - msr_r_sf = Signal() - - m.d.comb += [ - spec_msr_r_mask[63 - 0].eq(1), - msr_r_sf.eq(self.pfv.msr.r_data[63 - 0]), - ] - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += Assert((self.pfv.msr.r_mask & spec_msr_r_mask) == spec_msr_r_mask) - - # XER - - xer_r_so = Signal() - xer_w_so = Signal() - xer_w_ov = Signal() - xer_w_ca = Signal() - xer_w_ov32 = Signal() - xer_w_ca32 = Signal() - - if isinstance(spec_insn, ( - ADD_ , ADDO_ , ADDIC_ , - SUBF_ , SUBFO_ , - ADDC_ , ADDCO_ , ADDE_ , ADDEO_ , - SUBFC_ , SUBFCO_ , SUBFE_ , SUBFEO_ , - ADDME_ , ADDMEO_ , ADDZE_ , ADDZEO_ , - SUBFME_, SUBFMEO_, SUBFZE_, SUBFZEO_, - NEG_ , NEGO_ , - )): - # Read XER.SO (to update CR0) - m.d.comb += [ - xer_r_so.eq(self.pfv.xer.r_data[63 - 32]), - spec_xer_r_mask[63 - 32].eq(1), - ] - - if isinstance(spec_insn, ( - ADDO , ADDO_ , SUBFO , SUBFO_ , - ADDCO , ADDCO_ , SUBFCO , SUBFCO_ , - ADDEO , ADDEO_ , SUBFEO , SUBFEO_ , - ADDMEO, ADDMEO_, SUBFMEO, SUBFMEO_, - ADDZEO, ADDZEO_, SUBFZEO, SUBFZEO_, - NEGO , NEGO_ , - )): - # Set XER.SO, write XER.OV and XER.OV32 - m.d.comb += [ - xer_w_so .eq(xer_w_ov), - xer_w_ov .eq(Mux(msr_r_sf, ov_64, ov_32)), - xer_w_ov32.eq(ov_32), - spec_xer_w_mask[63 - 32].eq(xer_w_so), - spec_xer_w_data[63 - 32].eq(xer_w_so), - spec_xer_w_mask[63 - 33].eq(1), - spec_xer_w_data[63 - 33].eq(xer_w_ov), - spec_xer_w_mask[63 - 44].eq(1), - spec_xer_w_data[63 - 44].eq(xer_w_ov32), - ] - elif isinstance(spec_insn, ADDEX): - # Write XER.OV and XER.OV32 - m.d.comb += [ - xer_w_ov .eq(Mux(msr_r_sf, ca_64, ca_32)), - xer_w_ov32.eq(ca_32), - spec_xer_w_mask[63 - 33].eq(1), - spec_xer_w_data[63 - 33].eq(xer_w_ov), - spec_xer_w_mask[63 - 44].eq(1), - spec_xer_w_data[63 - 44].eq(xer_w_ov32), - ] - - if isinstance(spec_insn, ( - ADDIC , ADDIC_ , SUBFIC , - ADDC , ADDC_ , ADDCO , ADDCO_ , - SUBFC , SUBFC_ , SUBFCO , SUBFCO_ , - ADDE , ADDE_ , ADDEO , ADDEO_ , - SUBFE , SUBFE_ , SUBFEO , SUBFEO_ , - ADDME , ADDME_ , ADDMEO , ADDMEO_ , - SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, - ADDZE , ADDZE_ , ADDZEO , ADDZEO_ , - SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, - )): - # Write XER.CA and XER.CA32 - m.d.comb += [ - xer_w_ca .eq(Mux(msr_r_sf, ca_64, ca_32)), - xer_w_ca32.eq(ca_32), - spec_xer_w_mask[63 - 34].eq(1), - spec_xer_w_data[63 - 34].eq(xer_w_ca), - spec_xer_w_mask[63 - 45].eq(1), - spec_xer_w_data[63 - 45].eq(xer_w_ca32), - ] - - keep_xer_w_mask = Signal(64) - keep_xer_w_data = Signal(64) - - m.d.comb += [ - keep_xer_w_mask.eq(self.pfv.xer.w_mask & ~spec_xer_w_mask), - keep_xer_w_data.eq(self.pfv.xer.r_data & keep_xer_w_mask), - ] - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert((self.pfv.xer.r_mask & spec_xer_r_mask) == spec_xer_r_mask), - Assert((self.pfv.xer.w_mask & spec_xer_w_mask) == spec_xer_w_mask), - Assert((self.pfv.xer.w_data & spec_xer_w_mask) == spec_xer_w_data), - Assert((self.pfv.xer.r_mask & keep_xer_w_mask) == keep_xer_w_mask), - Assert((self.pfv.xer.w_data & keep_xer_w_mask) == keep_xer_w_data), - ] - - # CR - - cr0_w_lt = Signal() - cr0_w_gt = Signal() - cr0_w_eq = Signal() - cr0_w_so = Signal() - - if isinstance(spec_insn, ( - ADD_ , ADDO_ , ADDIC_ , - SUBF_ , SUBFO_ , - ADDC_ , ADDCO_ , ADDE_ , ADDEO_ , - SUBFC_ , SUBFCO_ , SUBFE_ , SUBFEO_ , - ADDME_ , ADDMEO_ , ADDZE_ , ADDZEO_ , - SUBFME_, SUBFMEO_, SUBFZE_, SUBFZEO_, - NEG_ , NEGO_ , - )): - # Write CR0 - m.d.comb += [ - cr0_w_lt.eq(Mux(msr_r_sf, result[63], result[31])), - cr0_w_gt.eq(~(cr0_w_lt | cr0_w_eq)), - cr0_w_eq.eq(~Mux(msr_r_sf, result[:64].any(), result[:32].any())), - cr0_w_so.eq(Mux(xer_w_so, xer_w_so, xer_r_so)), - - spec_cr_w_stb [ 7 - 0].eq(1), - spec_cr_w_data[31 - 0].eq(cr0_w_lt), - spec_cr_w_data[31 - 1].eq(cr0_w_gt), - spec_cr_w_data[31 - 2].eq(cr0_w_eq), - spec_cr_w_data[31 - 3].eq(cr0_w_so), - ] - - spec_cr_w_mask = Signal(32) - m.d.comb += spec_cr_w_mask.eq(Cat(Repl(s, 4) for s in spec_cr_w_stb)) - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert(self.pfv.cr.w_stb == spec_cr_w_stb), - Assert((self.pfv.cr.w_data & spec_cr_w_mask) == spec_cr_w_data), - ] - - return m - - -class AddSubtractCheck(PowerFVCheck, name="_insn_addsub"): - def __init_subclass__(cls, name, insn_cls): - super().__init_subclass__(name) - cls.insn_cls = insn_cls - - def get_testbench(self, dut, post): - tb_spec = AddSubtractSpec(self.insn_cls, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/insn/_branch.py b/power_fv/checks/insn/_branch.py deleted file mode 100644 index 1bd8cdf..0000000 --- a/power_fv/checks/insn/_branch.py +++ /dev/null @@ -1,251 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb -from ...utils import iea_mask - -from ._fmt import * -from ._insn import * - - -__all__ = ["BranchSpec", "BranchCheck"] - - -class BranchSpec(Elaboratable): - def __init__(self, insn_cls, post): - self.insn_cls = insn_cls - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spec_insn = self.insn_cls() - - with m.If(self.post.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(self.pfv.insn[32:] == spec_insn), - Assert(self.pfv.msr.w_mask[63 - 0]), # MSR.SF - ] - - msr_w_sf = Signal() - m.d.comb += msr_w_sf.eq(self.pfv.msr.w_data[63 - 0]) - - if isinstance(spec_insn, (Instruction_B, Instruction_XL_bc)): - bo_valid_patterns = [ - "001--", - "011--", - "1-1--", - ] - if not isinstance(spec_insn, (BCCTR, BCCTRL)): - # bcctr/bcctrl forms with BO(2)=0 ("decrement and test CTR") are illegal. - bo_valid_patterns += [ - "0000-", - "0001-", - "0100-", - "0101-", - "1-00-", - "1-01-", - ] - - bo_invalid = Signal() - m.d.comb += bo_invalid.eq(~spec_insn.bo.matches(*bo_valid_patterns)) - - with m.If(self.post.stb): - m.d.sync += Assert(bo_invalid.implies(self.pfv.intr)) - - # NIA - - spec_nia = Signal(unsigned(64)) - taken = Signal() - offset = Signal(signed(62)) - target = Signal(signed(64)) - - 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_bc)): - 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[:32].any() | - (self.pfv.ctr.w_data[32:].any() & msr_w_sf)), - cond_ok .eq(spec_insn.bo[4-0] | (spec_insn.bo[4-1] == cond_bit)), - ctr_ok .eq(spec_insn.bo[4-2] | (ctr_any ^ spec_insn.bo[4-3])), - ] - - if isinstance(spec_insn, (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 isinstance(spec_insn, (BCLR, BCLRL)): - m.d.comb += offset.eq(self.pfv.lr .r_data[2:]) - elif isinstance(spec_insn, (BCCTR, BCCTRL)): - m.d.comb += offset.eq(self.pfv.ctr.r_data[2:]) - elif isinstance(spec_insn, (BCTAR, BCTARL)): - m.d.comb += offset.eq(self.pfv.tar.r_data[2:]) - 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 += target.eq(self.pfv.cia + (offset << 2)) - else: - m.d.comb += target.eq(offset << 2) - with m.Else(): - m.d.comb += target.eq(self.pfv.cia + 4) - - m.d.comb += spec_nia.eq(iea_mask(target, msr_w_sf)) - - with m.If(self.post.stb & ~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_bc)): - 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.post.stb & ~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_r_mask = Signal(64) - spec_lr_w_mask = Signal(64) - 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_bc)): - if isinstance(spec_insn, (BCLR, BCLRL)): - m.d.comb += spec_lr_r_stb.eq(1) - else: - m.d.comb += spec_lr_r_stb.eq(0) - else: - assert False - - m.d.comb += spec_lr_w_stb.eq(spec_insn.lk) - - cia_4 = Signal(unsigned(64)) - m.d.comb += cia_4.eq(self.pfv.cia + 4) - - m.d.comb += [ - spec_lr_r_mask.eq(Repl(spec_lr_r_stb, 64)), - spec_lr_w_mask.eq(Repl(spec_lr_w_stb, 64)), - spec_lr_w_data.eq(iea_mask(cia_4, msr_w_sf)), - ] - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert((self.pfv.lr.r_mask & spec_lr_r_mask) == spec_lr_r_mask), - Assert(self.pfv.lr.w_mask == spec_lr_w_mask), - Assert((self.pfv.lr.w_data & spec_lr_w_mask) == (spec_lr_w_data & spec_lr_w_mask)), - ] - - # CTR - - spec_ctr_r_stb = Signal() - spec_ctr_w_stb = Signal() - - spec_ctr_r_mask = Signal(64) - spec_ctr_w_mask = Signal(64) - 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[4-2]) - elif isinstance(spec_insn, Instruction_XL_bc): - if isinstance(spec_insn, (BCCTR, BCCTRL)): - m.d.comb += spec_ctr_r_stb.eq(1) - else: - m.d.comb += spec_ctr_r_stb.eq(~spec_insn.bo[4-2]) - 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[4-2]) - elif isinstance(spec_insn, Instruction_XL_bc): - if isinstance(spec_insn, (BCCTR, BCCTRL)): - m.d.comb += spec_ctr_w_stb.eq(0) - else: - m.d.comb += spec_ctr_w_stb.eq(~spec_insn.bo[4-2]) - else: - assert False - - m.d.comb += [ - spec_ctr_r_mask.eq(Repl(spec_ctr_r_stb, 64)), - spec_ctr_w_mask.eq(Repl(spec_ctr_w_stb, 64)), - spec_ctr_w_data.eq(self.pfv.ctr.r_data - 1), - ] - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert((self.pfv.ctr.r_mask & spec_ctr_r_mask) == spec_ctr_r_mask), - Assert(self.pfv.ctr.w_mask == spec_ctr_w_mask), - Assert((self.pfv.ctr.w_data & spec_ctr_w_mask) == (spec_ctr_w_data & spec_ctr_w_mask)), - ] - - # TAR - - spec_tar_r_stb = Signal() - spec_tar_r_mask = Signal(64) - - if isinstance(spec_insn, (Instruction_I, Instruction_B)): - m.d.comb += spec_tar_r_stb.eq(0) - elif isinstance(spec_insn, (Instruction_XL_bc)): - if isinstance(spec_insn, (BCTAR, BCTARL)): - m.d.comb += spec_tar_r_stb.eq(1) - else: - m.d.comb += spec_tar_r_stb.eq(0) - else: - assert False - - m.d.comb += spec_tar_r_mask.eq(Repl(spec_tar_r_stb, 64)) - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += Assert((self.pfv.tar.r_mask & spec_tar_r_mask) == spec_tar_r_mask) - - return m - - -class BranchCheck(PowerFVCheck, name="_insn_branch"): - def __init_subclass__(cls, name, insn_cls): - super().__init_subclass__(name) - cls.insn_cls = insn_cls - - def get_testbench(self, dut, post): - tb_spec = BranchSpec(self.insn_cls, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/insn/_compare.py b/power_fv/checks/insn/_compare.py deleted file mode 100644 index fe07860..0000000 --- a/power_fv/checks/insn/_compare.py +++ /dev/null @@ -1,152 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - -from ._fmt import * -from ._insn import * - - -__all__ = ["CompareSpec", "CompareCheck"] - - -class CompareSpec(Elaboratable): - def __init__(self, insn_cls, post): - self.insn_cls = insn_cls - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spec_insn = self.insn_cls() - - with m.If(self.post.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(self.pfv.insn[32:] == spec_insn), - ] - - # GPRs - - spec_ra_r_stb = Signal() - spec_rb_r_stb = Signal() - - if isinstance(spec_insn, (CMPI, CMPLI, CMP, CMPL)): - m.d.comb += spec_ra_r_stb.eq(1) - else: - assert False - - if isinstance(spec_insn, (CMPI, CMPLI)): - m.d.comb += spec_rb_r_stb.eq(0) - elif isinstance(spec_insn, (CMP, CMPL)): - m.d.comb += spec_rb_r_stb.eq(1) - else: - assert False - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert(self.pfv.ra.r_stb == spec_ra_r_stb), - Assert(self.pfv.rb.r_stb == spec_rb_r_stb), - ] - - # CR - - spec_cr_w_stb = Signal(8) - spec_cr_w_data = Signal(32) - - a = Signal(signed(64)) - b = Signal(signed(64)) - c = Record([("lt", 1), ("gt", 1), ("eq_", 1), ("so", 1)]) - - if isinstance(spec_insn, (CMPI, CMP)): - with m.If(spec_insn.l): - m.d.comb += a.eq(self.pfv.ra.r_data) - with m.Else(): - m.d.comb += a.eq(self.pfv.ra.r_data[:32].as_signed()) - elif isinstance(spec_insn, (CMPL, CMPLI)): - with m.If(spec_insn.l): - m.d.comb += a.eq(self.pfv.ra.r_data) - with m.Else(): - m.d.comb += a.eq(self.pfv.ra.r_data[:32].as_unsigned()) - else: - assert False - - if isinstance(spec_insn, CMPI): - m.d.comb += b.eq(spec_insn.si) - elif isinstance(spec_insn, CMPLI): - m.d.comb += b.eq(spec_insn.ui) - elif isinstance(spec_insn, CMP): - with m.If(spec_insn.l): - m.d.comb += b.eq(self.pfv.rb.r_data) - with m.Else(): - m.d.comb += b.eq(self.pfv.rb.r_data[:32].as_signed()) - elif isinstance(spec_insn, CMPL): - with m.If(spec_insn.l): - m.d.comb += b.eq(self.pfv.rb.r_data) - with m.Else(): - m.d.comb += b.eq(self.pfv.rb.r_data[:32].as_unsigned()) - else: - assert False - - if isinstance(spec_insn, (CMPI, CMP)): - m.d.comb += [ - c.lt.eq(a.as_signed() < b.as_signed()), - c.gt.eq(a.as_signed() > b.as_signed()), - ] - elif isinstance(spec_insn, (CMPLI, CMPL)): - m.d.comb += [ - c.lt.eq(a.as_unsigned() < b.as_unsigned()), - c.gt.eq(a.as_unsigned() > b.as_unsigned()), - ] - else: - assert False - - m.d.comb += [ - c.eq_.eq(a == b), - c.so .eq(self.pfv.xer.r_data[63 - 32]), # XER.SO - ] - - m.d.comb += [ - spec_cr_w_stb[::-1].bit_select(spec_insn.bf, width=1).eq(1), - spec_cr_w_data[::-1].eq(Repl(c, 8)), - ] - - with m.If(self.post.stb & ~self.pfv.intr): - for i in range(8): - spec_cr_w_field = spec_cr_w_data .word_select(i, width=4) - pfv_cr_w_field = self.pfv.cr.w_data.word_select(i, width=4) - - m.d.sync += [ - Assert(self.pfv.cr.w_stb[i] == spec_cr_w_stb[i]), - Assert(spec_cr_w_stb[i].implies(pfv_cr_w_field == spec_cr_w_field)), - ] - - # XER - - spec_xer_r_mask = Signal(64) - - if isinstance(spec_insn, (CMPI, CMPLI, CMP, CMPL)): - m.d.comb += spec_xer_r_mask[63 - 32].eq(1) # XER.SO - else: - assert False - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += Assert((self.pfv.xer.r_mask & spec_xer_r_mask) == spec_xer_r_mask) - - return m - - -class CompareCheck(PowerFVCheck, name="_insn_compare"): - def __init_subclass__(cls, name, insn_cls): - super().__init_subclass__(name) - cls.insn_cls = insn_cls - - def get_testbench(self, dut, post): - tb_spec = CompareSpec(self.insn_cls, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/insn/_cr.py b/power_fv/checks/insn/_cr.py deleted file mode 100644 index 77dbea3..0000000 --- a/power_fv/checks/insn/_cr.py +++ /dev/null @@ -1,128 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - -from ._fmt import * -from ._insn import * - - -__all__ = ["CRSpec", "CRCheck"] - - -class CRSpec(Elaboratable): - def __init__(self, insn_cls, post): - self.insn_cls = insn_cls - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - def elaborate(self, platform): - m = Module() - - spec_insn = self.insn_cls() - - with m.If(self.post.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(self.pfv.insn[32:] == spec_insn), - ] - - # CR - - spec_cr_r_stb = Signal(8) - spec_cr_w_stb = Signal(8) - spec_cr_w_data = Signal(32) - - if isinstance(spec_insn, Instruction_XL_crl): - ba_r_field = Signal(4) - bb_r_field = Signal(4) - bt_r_field = Signal(4) - ba_r_bit = Signal() - bb_r_bit = Signal() - bt_w_bit = Signal() - - m.d.comb += [ - ba_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.ba[2:], width=4)), - bb_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.bb[2:], width=4)), - bt_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.bt[2:], width=4)), - - ba_r_bit.eq(ba_r_field.bit_select(spec_insn.ba[:2], width=1)), - bb_r_bit.eq(bb_r_field.bit_select(spec_insn.bb[:2], width=1)), - ] - - if isinstance(spec_insn, CRAND): - m.d.comb += bt_w_bit.eq(ba_r_bit & bb_r_bit) - elif isinstance(spec_insn, CROR): - m.d.comb += bt_w_bit.eq(ba_r_bit | bb_r_bit) - elif isinstance(spec_insn, CRNAND): - m.d.comb += bt_w_bit.eq(~(ba_r_bit & bb_r_bit)) - elif isinstance(spec_insn, CRXOR): - m.d.comb += bt_w_bit.eq(ba_r_bit ^ bb_r_bit) - elif isinstance(spec_insn, CRNOR): - m.d.comb += bt_w_bit.eq(~(ba_r_bit | bb_r_bit)) - elif isinstance(spec_insn, CRANDC): - m.d.comb += bt_w_bit.eq(ba_r_bit & ~bb_r_bit) - elif isinstance(spec_insn, CREQV): - m.d.comb += bt_w_bit.eq(ba_r_bit == bb_r_bit) - elif isinstance(spec_insn, CRORC): - m.d.comb += bt_w_bit.eq(ba_r_bit | ~bb_r_bit) - else: - assert False - - spec_bt_w_field = Signal(4) - - for i, spec_bt_w_bit in enumerate(spec_bt_w_field): - bt_r_bit = bt_r_field[i] - with m.If(spec_insn.bt[:2] == i): - m.d.comb += spec_bt_w_bit.eq(bt_w_bit) - with m.Else(): - m.d.comb += spec_bt_w_bit.eq(bt_r_bit) - - m.d.comb += [ - spec_cr_r_stb[::-1].bit_select(spec_insn.ba[2:], width=1).eq(1), - spec_cr_r_stb[::-1].bit_select(spec_insn.bb[2:], width=1).eq(1), - spec_cr_w_stb[::-1].bit_select(spec_insn.bt[2:], width=1).eq(1), - spec_cr_w_data[::-1].eq(Repl(spec_bt_w_field, 8)) - ] - - elif isinstance(spec_insn, MCRF): - bfa_r_field = Signal(4) - - m.d.comb += [ - bfa_r_field.eq(self.pfv.cr.r_data[::-1].word_select(spec_insn.bfa, width=4)), - - spec_cr_r_stb[::-1].bit_select(spec_insn.bfa, width=1).eq(1), - spec_cr_w_stb[::-1].bit_select(spec_insn.bf, width=1).eq(1), - spec_cr_w_data[::-1].eq(Repl(bfa_r_field, 8)), - ] - - else: - assert False - - with m.If(self.post.stb & ~self.pfv.intr): - for i in range(8): - spec_cr_w_field = spec_cr_w_data .word_select(i, width=4) - pfv_cr_w_field = self.pfv.cr.w_data.word_select(i, width=4) - - m.d.sync += [ - Assert(spec_cr_r_stb[i].implies(self.pfv.cr.r_stb[i])), - Assert(self.pfv.cr.w_stb[i] == spec_cr_w_stb[i]), - Assert(spec_cr_w_stb[i].implies(pfv_cr_w_field == spec_cr_w_field)), - ] - - return m - - -class CRCheck(PowerFVCheck, name="_insn_cr"): - def __init_subclass__(cls, name, insn_cls): - super().__init_subclass__(name) - cls.insn_cls = insn_cls - - def get_testbench(self, dut, post): - tb_spec = CRSpec(self.insn_cls, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/insn/_fmt.py b/power_fv/checks/insn/_fmt.py deleted file mode 100644 index 1d5f605..0000000 --- a/power_fv/checks/insn/_fmt.py +++ /dev/null @@ -1,324 +0,0 @@ -from amaranth import * -from amaranth.asserts import AnyConst -from amaranth.hdl.ast import ValueCastable - - -__all__ = [ - "Instruction_I", - "Instruction_B", - "Instruction_D_add", "Instruction_D_cmp", - "Instruction_DX", - "Instruction_X_cmp", - "Instruction_XL_bc", "Instruction_XL_crl", "Instruction_XL_crf", - "Instruction_XFX_spr", - "Instruction_XO", - "Instruction_Z23_add", -] - - -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_bc(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(10)) - 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 Instruction_XL_crl(ValueCastable): - po = None - bt = None - ba = None - bb = None - xo = None - _0 = None - - def __init_subclass__(cls, *, po, xo): - cls.po = Const(po, unsigned( 6)) - cls.xo = Const(xo, unsigned(10)) - - def __init__(self): - self.bt = AnyConst(unsigned(5)) - self.ba = AnyConst(unsigned(5)) - self.bb = AnyConst(unsigned(5)) - self._0 = AnyConst(unsigned(1)) - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._0, self.xo, self.bb, self.ba, self.bt, self.po) - - -class Instruction_XL_crf(ValueCastable): - po = None - bf = None - _0 = None - bfa = None - _1 = None - _2 = None - xo = None - _3 = None - - def __init_subclass__(cls, *, po, xo): - cls.po = Const(po, unsigned( 6)) - cls.xo = Const(xo, unsigned(10)) - - def __init__(self): - self.bf = AnyConst(unsigned(3)) - self._0 = AnyConst(unsigned(2)) - self.bfa = AnyConst(unsigned(3)) - self._1 = AnyConst(unsigned(2)) - self._2 = AnyConst(unsigned(5)) - self._3 = AnyConst(unsigned(1)) - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._3, self.xo, self._2, self._1, self.bfa, self._0, self.bf, self.po) - - -class Instruction_D_add(ValueCastable): - po = None - rt = None - ra = None - _i = None - - def __init_subclass__(cls, *, po): - cls.po = Const(po, unsigned(6)) - - def __init__(self): - self.rt = AnyConst(unsigned(5)) - self.ra = AnyConst(unsigned(5)) - self._i = AnyConst(16) - - @property - def si(self): - return self._i.as_signed() - - def ui(self): - return self._i.as_unsigned() - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._i, self.ra, self.rt, self.po) - - -class Instruction_D_cmp(ValueCastable): - po = None - bf = None - _0 = None - l = None - ra = None - _i = None - - def __init_subclass__(cls, *, po): - cls.po = Const(po, unsigned(6)) - - def __init__(self): - self.bf = AnyConst(unsigned(3)) - self._0 = AnyConst(unsigned(1)) - self.l = AnyConst(unsigned(1)) - self.ra = AnyConst(unsigned(5)) - self._i = AnyConst(16) - - @property - def si(self): - return self._i.as_signed() - - def ui(self): - return self._i.as_unsigned() - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._i, self.ra, self.l, self._0, self.bf, self.po) - - -class Instruction_DX(ValueCastable): - po = None - rt = None - d1 = None - d0 = None - xo = None - d2 = None - - def __init_subclass__(cls, *, po, xo): - cls.po = Const(po, unsigned(6)) - cls.xo = Const(xo, unsigned(5)) - - def __init__(self): - self.rt = AnyConst(unsigned( 5)) - self.d1 = AnyConst(unsigned( 5)) - self.d0 = AnyConst(unsigned(10)) - self.d2 = AnyConst(unsigned( 1)) - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self.d2, self.xo, self.d0, self.d1, self.rt, self.po) - - -class Instruction_X_cmp(ValueCastable): - po = None - bf = None - _0 = None - l = None - ra = None - rb = None - xo = None - _1 = None - - def __init_subclass__(cls, *, po, xo): - cls.po = Const(po, unsigned( 6)) - cls.xo = Const(xo, unsigned(10)) - - def __init__(self): - self.bf = AnyConst(unsigned(3)) - self._0 = AnyConst(unsigned(1)) - self.l = AnyConst(unsigned(1)) - self.ra = AnyConst(unsigned(5)) - self.rb = AnyConst(unsigned(5)) - self._1 = AnyConst(unsigned(1)) - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._1, self.xo, self.rb, self.ra, self.l, self._0, self.bf, self.po) - - -class Instruction_XFX_spr(ValueCastable): - po = None - _gpr = None - spr = None - xo = None - _0 = None - - def __init_subclass__(cls, *, po, xo): - cls.po = Const(po, unsigned( 6)) - cls.xo = Const(xo, unsigned(10)) - - def __init__(self): - self._gpr = AnyConst(unsigned( 5)) - self.spr = AnyConst(unsigned(10)) - self._0 = AnyConst(unsigned( 1)) - - @property - def rs(self): - return self._gpr - - @property - def rt(self): - return self._gpr - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._0, self.xo, self.spr, self._gpr, self.po) - - -class Instruction_XO(ValueCastable): - po = None - rt = None - ra = None - rb = None - oe = None - xo = None - rc = None - - def __init_subclass__(cls, *, po, xo, oe=None, rc=None): - cls.po = Const(po, unsigned(6)) - cls.xo = Const(xo, unsigned(9)) - if oe is not None: - cls.oe = Const(oe, unsigned(1)) - if rc is not None: - cls.rc = Const(rc, unsigned(1)) - - def __init__(self): - self.rt = AnyConst(unsigned(5)) - self.ra = AnyConst(unsigned(5)) - self.rb = AnyConst(unsigned(5)) - if self.oe is None: - self.oe = AnyConst(unsigned(1)) - if self.rc is None: - self.rc = AnyConst(unsigned(1)) - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self.rc, self.xo, self.oe, self.rb, self.ra, self.rt, self.po) - - -class Instruction_Z23_add(ValueCastable): - po = None - rt = None - ra = None - rb = None - cy = None - xo = None - _0 = None - - def __init_subclass__(cls, *, po, xo, cy): - cls.po = Const(po, unsigned(6)) - cls.cy = Const(cy, unsigned(2)) - cls.xo = Const(xo, unsigned(8)) - - def __init__(self): - self.rt = AnyConst(unsigned(5)) - self.ra = AnyConst(unsigned(5)) - self.rb = AnyConst(unsigned(5)) - self._0 = AnyConst(unsigned(1)) - - @ValueCastable.lowermethod - def as_value(self): - return Cat(self._0, self.xo, self.cy, self.rb, self.ra, self.rt, self.po) diff --git a/power_fv/checks/insn/_insn.py b/power_fv/checks/insn/_insn.py deleted file mode 100644 index 26b8bce..0000000 --- a/power_fv/checks/insn/_insn.py +++ /dev/null @@ -1,99 +0,0 @@ -from . import _fmt - -# Branches - -class B (_fmt.Instruction_I, po=18, aa=0, lk=0): pass -class BA (_fmt.Instruction_I, po=18, aa=1, lk=0): pass -class BL (_fmt.Instruction_I, po=18, aa=0, lk=1): pass -class BLA (_fmt.Instruction_I, po=18, aa=1, lk=1): pass - -class BC (_fmt.Instruction_B, po=16, aa=0, lk=0): pass -class BCA (_fmt.Instruction_B, po=16, aa=1, lk=0): pass -class BCL (_fmt.Instruction_B, po=16, aa=0, lk=1): pass -class BCLA (_fmt.Instruction_B, po=16, aa=1, lk=1): pass - -class BCLR (_fmt.Instruction_XL_bc, po=19, xo= 16, lk=0): pass -class BCLRL (_fmt.Instruction_XL_bc, po=19, xo= 16, lk=1): pass -class BCCTR (_fmt.Instruction_XL_bc, po=19, xo=528, lk=0): pass -class BCCTRL (_fmt.Instruction_XL_bc, po=19, xo=528, lk=1): pass -class BCTAR (_fmt.Instruction_XL_bc, po=19, xo=560, lk=0): pass -class BCTARL (_fmt.Instruction_XL_bc, po=19, xo=560, lk=1): pass - -# CR - -class CRAND (_fmt.Instruction_XL_crl, po=19, xo=257): pass -class CROR (_fmt.Instruction_XL_crl, po=19, xo=449): pass -class CRNAND (_fmt.Instruction_XL_crl, po=19, xo=225): pass -class CRXOR (_fmt.Instruction_XL_crl, po=19, xo=193): pass -class CRNOR (_fmt.Instruction_XL_crl, po=19, xo= 33): pass -class CRANDC (_fmt.Instruction_XL_crl, po=19, xo=129): pass -class CREQV (_fmt.Instruction_XL_crl, po=19, xo=289): pass -class CRORC (_fmt.Instruction_XL_crl, po=19, xo=417): pass - -class MCRF (_fmt.Instruction_XL_crf, po=19, xo=0): pass - -# Add / Subtract from - -class ADDI (_fmt.Instruction_D_add, po=14): pass -class ADDIS (_fmt.Instruction_D_add, po=15): pass -class ADDPCIS (_fmt.Instruction_DX, po=19, xo= 2): pass -class ADD (_fmt.Instruction_XO, po=31, xo=266, oe=0, rc=0): pass -class ADD_ (_fmt.Instruction_XO, po=31, xo=266, oe=0, rc=1): pass -class ADDO (_fmt.Instruction_XO, po=31, xo=266, oe=1, rc=0): pass -class ADDO_ (_fmt.Instruction_XO, po=31, xo=266, oe=1, rc=1): pass -class ADDIC (_fmt.Instruction_D_add, po=12): pass -class ADDIC_ (_fmt.Instruction_D_add, po=13): pass -class SUBF (_fmt.Instruction_XO, po=31, xo= 40, oe=0, rc=0): pass -class SUBF_ (_fmt.Instruction_XO, po=31, xo= 40, oe=0, rc=1): pass -class SUBFO (_fmt.Instruction_XO, po=31, xo= 40, oe=1, rc=0): pass -class SUBFO_ (_fmt.Instruction_XO, po=31, xo= 40, oe=1, rc=1): pass -class SUBFIC (_fmt.Instruction_D_add, po= 8): pass -class ADDC (_fmt.Instruction_XO, po=31, xo= 10, oe=0, rc=0): pass -class ADDC_ (_fmt.Instruction_XO, po=31, xo= 10, oe=0, rc=1): pass -class ADDCO (_fmt.Instruction_XO, po=31, xo= 10, oe=1, rc=0): pass -class ADDCO_ (_fmt.Instruction_XO, po=31, xo= 10, oe=1, rc=1): pass -class ADDE (_fmt.Instruction_XO, po=31, xo=138, oe=0, rc=0): pass -class ADDE_ (_fmt.Instruction_XO, po=31, xo=138, oe=0, rc=1): pass -class ADDEO (_fmt.Instruction_XO, po=31, xo=138, oe=1, rc=0): pass -class ADDEO_ (_fmt.Instruction_XO, po=31, xo=138, oe=1, rc=1): pass -class SUBFC (_fmt.Instruction_XO, po=31, xo= 8, oe=0, rc=0): pass -class SUBFC_ (_fmt.Instruction_XO, po=31, xo= 8, oe=0, rc=1): pass -class SUBFCO (_fmt.Instruction_XO, po=31, xo= 8, oe=1, rc=0): pass -class SUBFCO_ (_fmt.Instruction_XO, po=31, xo= 8, oe=1, rc=1): pass -class SUBFE (_fmt.Instruction_XO, po=31, xo=136, oe=0, rc=0): pass -class SUBFE_ (_fmt.Instruction_XO, po=31, xo=136, oe=0, rc=1): pass -class SUBFEO (_fmt.Instruction_XO, po=31, xo=136, oe=1, rc=0): pass -class SUBFEO_ (_fmt.Instruction_XO, po=31, xo=136, oe=1, rc=1): pass -class ADDME (_fmt.Instruction_XO, po=31, xo=234, oe=0, rc=0): pass -class ADDME_ (_fmt.Instruction_XO, po=31, xo=234, oe=0, rc=1): pass -class ADDMEO (_fmt.Instruction_XO, po=31, xo=234, oe=1, rc=0): pass -class ADDMEO_ (_fmt.Instruction_XO, po=31, xo=234, oe=1, rc=1): pass -class ADDZE (_fmt.Instruction_XO, po=31, xo=202, oe=0, rc=0): pass -class ADDZE_ (_fmt.Instruction_XO, po=31, xo=202, oe=0, rc=1): pass -class ADDZEO (_fmt.Instruction_XO, po=31, xo=202, oe=1, rc=0): pass -class ADDZEO_ (_fmt.Instruction_XO, po=31, xo=202, oe=1, rc=1): pass -class SUBFME (_fmt.Instruction_XO, po=31, xo=232, oe=0, rc=0): pass -class SUBFME_ (_fmt.Instruction_XO, po=31, xo=232, oe=0, rc=1): pass -class SUBFMEO (_fmt.Instruction_XO, po=31, xo=232, oe=1, rc=0): pass -class SUBFMEO_ (_fmt.Instruction_XO, po=31, xo=232, oe=1, rc=1): pass -class SUBFZE (_fmt.Instruction_XO, po=31, xo=200, oe=0, rc=0): pass -class SUBFZE_ (_fmt.Instruction_XO, po=31, xo=200, oe=0, rc=1): pass -class SUBFZEO (_fmt.Instruction_XO, po=31, xo=200, oe=1, rc=0): pass -class SUBFZEO_ (_fmt.Instruction_XO, po=31, xo=200, oe=1, rc=1): pass -class ADDEX (_fmt.Instruction_Z23_add, po=31, xo=170, cy=0): pass -class NEG (_fmt.Instruction_XO, po=31, xo=104, oe=0, rc=0): pass -class NEG_ (_fmt.Instruction_XO, po=31, xo=104, oe=0, rc=1): pass -class NEGO (_fmt.Instruction_XO, po=31, xo=104, oe=1, rc=0): pass -class NEGO_ (_fmt.Instruction_XO, po=31, xo=104, oe=1, rc=1): pass - -# Compare - -class CMPI (_fmt.Instruction_D_cmp, po=11): pass -class CMPLI (_fmt.Instruction_D_cmp, po=10): pass -class CMP (_fmt.Instruction_X_cmp, po=31, xo= 0): pass -class CMPL (_fmt.Instruction_X_cmp, po=31, xo= 32): pass - -# Move To/From SPR - -class MTSPR (_fmt.Instruction_XFX_spr, po=31, xo=467): pass -class MFSPR (_fmt.Instruction_XFX_spr, po=31, xo=339): pass diff --git a/power_fv/checks/insn/_spr.py b/power_fv/checks/insn/_spr.py deleted file mode 100644 index 972044d..0000000 --- a/power_fv/checks/insn/_spr.py +++ /dev/null @@ -1,165 +0,0 @@ -from amaranth import * -from amaranth.asserts import * - -from .. import PowerFVCheck -from ... import pfv, tb - -from ._fmt import * -from ._insn import * - - -__all__ = ["SPRMoveSpec", "SPRMoveCheck"] - - -class SPRMoveSpec(Elaboratable): - def __init__(self, insn_cls, post): - self.insn_cls = insn_cls - self.pfv = pfv.Interface() - self.post = tb.Trigger(cycle=post) - - def triggers(self): - yield self.post - - # TODO: - # - don't hardcode SPRs, let cores declare what they support. - # - access restrictions (i.e. R/W, privileged) - - def elaborate(self, platform): - m = Module() - - spec_insn = self.insn_cls() - - with m.If(self.post.stb): - m.d.sync += [ - Assume(self.pfv.stb), - Assume(self.pfv.insn[32:] == spec_insn), - ] - - spr = Record([ - ("num", 10), - ("reserved", 1), - ("undefined", 1), - ("pfv", [ - ("r_mask", 64), - ("r_data", 64), - ("w_mask", 64), - ("w_data", 64), - ]), - ]) - - if isinstance(spec_insn, (MTSPR, MFSPR)): - m.d.comb += spr.num.eq(Cat(spec_insn.spr[5:10], spec_insn.spr[0:5])) - else: - assert False - - with m.Switch(spr.num): - for num in range(808, 812): - with m.Case(num): - m.d.comb += spr.reserved.eq(1) - - pfv_sprs = [ - ( 1, self.pfv.xer ), - ( 8, self.pfv.lr ), - ( 9, self.pfv.ctr ), - ( 26, self.pfv.srr0), - ( 27, self.pfv.srr1), - (815, self.pfv.tar ), - ] - - for num, pfv_spr in pfv_sprs: - with m.Case(num): - m.d.comb += [ - spr.pfv.r_mask.eq(pfv_spr.r_mask), - spr.pfv.r_data.eq(pfv_spr.r_data), - spr.pfv.w_mask.eq(pfv_spr.w_mask), - spr.pfv.w_data.eq(pfv_spr.w_data), - ] - - with m.Default(): - m.d.comb += spr.undefined.eq(1) - - with m.If(self.post.stb): - # TODO: turn into assert - m.d.sync += Assume(spr.undefined.implies(self.pfv.intr)) - - # # MSR - # pfv_msr_pr = Signal() - # m.d.comb += pfv_msr_pr.eq(self.pfv.msr.r_data[63 - 49]) - - # with m.If(self.post.stb): - # m.d.sync += Assert(self.pfv.msr.r_mask[63 - 49]) - - # GPR - - spec_rs_r_stb = Signal() - spec_rt_w_stb = Signal() - # spec_rt_w_mask = Signal(64) - spec_rt_w_data = Signal(64) - - if isinstance(spec_insn, MTSPR): - m.d.comb += [ - spec_rs_r_stb.eq(~spr.reserved), - spec_rt_w_stb.eq(0), - ] - - elif isinstance(spec_insn, MFSPR): - m.d.comb += [ - spec_rs_r_stb .eq(0), - spec_rt_w_stb .eq(~spr.reserved), - spec_rt_w_data.eq(spr.pfv.r_data), - ] - - # # In problem state, reserved fields must return 0, so we include them in the mask. - # # In privileged state, reserved fields may return anything. - # with m.If(pfv_msr_pr): - # m.d.comb += spec_rt_w_mask.eq(Repl(1, 64)) - # with m.Else(): - # m.d.comb += spec_rt_w_mask.eq(spr.pfv.r_mask) - - else: - assert False - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert(spec_rs_r_stb.implies(self.pfv.rs.r_stb)), - Assert(self.pfv.rt.w_stb == spec_rt_w_stb), - Assert(spec_rt_w_stb.implies(self.pfv.rt.w_data == (spr.pfv.r_data & spr.pfv.r_mask))), - ] - # with m.If(spec_rt_w_stb): - # for i in range(64): - # with m.If(spr.pfv.w_mask[i]): - # m.d.sync += Assert(self.pfv.rt.w_data[i] == spec_rt_w_data[i]) - - # SPR - - spec_spr_w_stb = Signal() - spec_spr_w_data = Signal(64) - - if isinstance(spec_insn, MTSPR): - m.d.comb += [ - spec_spr_w_stb .eq(1), - spec_spr_w_data.eq(self.pfv.rs.r_data), - ] - elif isinstance(spec_insn, MFSPR): - m.d.comb += spec_spr_w_stb.eq(0) - else: - assert False - - with m.If(self.post.stb & ~self.pfv.intr): - m.d.sync += [ - Assert(spec_spr_w_stb == spr.pfv.w_mask.any()), - Assert((spr.pfv.w_data & spr.pfv.w_mask) == (spec_spr_w_data & spr.pfv.w_mask)), - ] - - return m - - -class SPRMoveCheck(PowerFVCheck, name="_insn_spr"): - def __init_subclass__(cls, name, insn_cls): - super().__init_subclass__(name) - cls.insn_cls = insn_cls - - def get_testbench(self, dut, post): - tb_spec = SPRMoveSpec(self.insn_cls, post) - tb_top = tb.Testbench(tb_spec, dut) - return tb_top diff --git a/power_fv/checks/insn/all.py b/power_fv/checks/insn/all.py deleted file mode 100644 index f9273bc..0000000 --- a/power_fv/checks/insn/all.py +++ /dev/null @@ -1,105 +0,0 @@ -from . import _insn -from ._branch import BranchCheck -from ._cr import CRCheck -from ._addsub import AddSubtractCheck -from ._compare import CompareCheck -from ._spr import SPRMoveCheck - - -# Branches - -class B (BranchCheck, name="insn_b", insn_cls=_insn.B, ): pass -class BA (BranchCheck, name="insn_ba", insn_cls=_insn.BA ): pass -class BL (BranchCheck, name="insn_bl", insn_cls=_insn.BL ): pass -class BLA (BranchCheck, name="insn_bla", insn_cls=_insn.BLA ): pass - -class BC (BranchCheck, name="insn_bc", insn_cls=_insn.BC ): pass -class BCA (BranchCheck, name="insn_bca", insn_cls=_insn.BCA ): pass -class BCL (BranchCheck, name="insn_bcl", insn_cls=_insn.BCL ): pass -class BCLA (BranchCheck, name="insn_bcla", insn_cls=_insn.BCLA ): pass - -class BCLR (BranchCheck, name="insn_bclr", insn_cls=_insn.BCLR ): pass -class BCLRL (BranchCheck, name="insn_bclrl", insn_cls=_insn.BCLRL ): pass -class BCCTR (BranchCheck, name="insn_bcctr", insn_cls=_insn.BCCTR ): pass -class BCCTRL (BranchCheck, name="insn_bcctrl", insn_cls=_insn.BCCTRL): pass -class BCTAR (BranchCheck, name="insn_bctar", insn_cls=_insn.BCTAR ): pass -class BCTARL (BranchCheck, name="insn_bctarl", insn_cls=_insn.BCTARL): pass - -# CR - -class CRAND (CRCheck, name="insn_crand", insn_cls=_insn.CRAND ): pass -class CROR (CRCheck, name="insn_cror", insn_cls=_insn.CROR ): pass -class CRNAND (CRCheck, name="insn_crnand", insn_cls=_insn.CRNAND): pass -class CRXOR (CRCheck, name="insn_crxor", insn_cls=_insn.CRXOR ): pass -class CRNOR (CRCheck, name="insn_crnor", insn_cls=_insn.CRNOR ): pass -class CRANDC (CRCheck, name="insn_crandc", insn_cls=_insn.CRANDC): pass -class CREQV (CRCheck, name="insn_creqv", insn_cls=_insn.CREQV ): pass -class CRORC (CRCheck, name="insn_crorc", insn_cls=_insn.CRORC ): pass - -class MCRF (CRCheck, name="insn_mcrf", insn_cls=_insn.MCRF ): pass - -# Add / Subtract from - -class ADDI (AddSubtractCheck, name="insn_addi", insn_cls=_insn.ADDI ): pass -class ADDIS (AddSubtractCheck, name="insn_addis", insn_cls=_insn.ADDIS ): pass -class ADDPCIS (AddSubtractCheck, name="insn_addpcis", insn_cls=_insn.ADDPCIS ): pass -class ADD (AddSubtractCheck, name="insn_add", insn_cls=_insn.ADD ): pass -class ADD_ (AddSubtractCheck, name="insn_add.", insn_cls=_insn.ADD_ ): pass -class ADDO (AddSubtractCheck, name="insn_addo", insn_cls=_insn.ADDO ): pass -class ADDO_ (AddSubtractCheck, name="insn_addo.", insn_cls=_insn.ADDO_ ): pass -class ADDIC (AddSubtractCheck, name="insn_addic", insn_cls=_insn.ADDIC ): pass -class ADDIC_ (AddSubtractCheck, name="insn_addic.", insn_cls=_insn.ADDIC_ ): pass -class SUBF (AddSubtractCheck, name="insn_subf", insn_cls=_insn.SUBF ): pass -class SUBF_ (AddSubtractCheck, name="insn_subf.", insn_cls=_insn.SUBF_ ): pass -class SUBFO (AddSubtractCheck, name="insn_subfo", insn_cls=_insn.SUBFO ): pass -class SUBFO_ (AddSubtractCheck, name="insn_subfo.", insn_cls=_insn.SUBFO_ ): pass -class SUBFIC (AddSubtractCheck, name="insn_subfic", insn_cls=_insn.SUBFIC ): pass -class ADDC (AddSubtractCheck, name="insn_addc", insn_cls=_insn.ADDC ): pass -class ADDC_ (AddSubtractCheck, name="insn_addc.", insn_cls=_insn.ADDC_ ): pass -class ADDCO (AddSubtractCheck, name="insn_addco", insn_cls=_insn.ADDCO ): pass -class ADDCO_ (AddSubtractCheck, name="insn_addco.", insn_cls=_insn.ADDCO_ ): pass -class ADDE (AddSubtractCheck, name="insn_adde", insn_cls=_insn.ADDE ): pass -class ADDE_ (AddSubtractCheck, name="insn_adde.", insn_cls=_insn.ADDE_ ): pass -class ADDEO (AddSubtractCheck, name="insn_addeo", insn_cls=_insn.ADDEO ): pass -class ADDEO_ (AddSubtractCheck, name="insn_addeo.", insn_cls=_insn.ADDEO_ ): pass -class SUBFC (AddSubtractCheck, name="insn_subfc", insn_cls=_insn.SUBFC ): pass -class SUBFC_ (AddSubtractCheck, name="insn_subfc.", insn_cls=_insn.SUBFC_ ): pass -class SUBFCO (AddSubtractCheck, name="insn_subfco", insn_cls=_insn.SUBFCO ): pass -class SUBFCO_ (AddSubtractCheck, name="insn_subfco.", insn_cls=_insn.SUBFCO_ ): pass -class SUBFE (AddSubtractCheck, name="insn_subfe", insn_cls=_insn.SUBFE ): pass -class SUBFE_ (AddSubtractCheck, name="insn_subfe.", insn_cls=_insn.SUBFE_ ): pass -class SUBFEO (AddSubtractCheck, name="insn_subfeo", insn_cls=_insn.SUBFEO ): pass -class SUBFEO_ (AddSubtractCheck, name="insn_subfeo.", insn_cls=_insn.SUBFEO_ ): pass -class ADDME (AddSubtractCheck, name="insn_addme", insn_cls=_insn.ADDME ): pass -class ADDME_ (AddSubtractCheck, name="insn_addme.", insn_cls=_insn.ADDME_ ): pass -class ADDMEO (AddSubtractCheck, name="insn_addmeo", insn_cls=_insn.ADDMEO ): pass -class ADDMEO_ (AddSubtractCheck, name="insn_addmeo.", insn_cls=_insn.ADDMEO_ ): pass -class ADDZE (AddSubtractCheck, name="insn_addze", insn_cls=_insn.ADDZE ): pass -class ADDZE_ (AddSubtractCheck, name="insn_addze.", insn_cls=_insn.ADDZE_ ): pass -class ADDZEO (AddSubtractCheck, name="insn_addzeo", insn_cls=_insn.ADDZEO ): pass -class ADDZEO_ (AddSubtractCheck, name="insn_addzeo.", insn_cls=_insn.ADDZEO_ ): pass -class SUBFME (AddSubtractCheck, name="insn_subfme", insn_cls=_insn.SUBFME ): pass -class SUBFME_ (AddSubtractCheck, name="insn_subfme.", insn_cls=_insn.SUBFME_ ): pass -class SUBFMEO (AddSubtractCheck, name="insn_subfmeo", insn_cls=_insn.SUBFMEO ): pass -class SUBFMEO_ (AddSubtractCheck, name="insn_subfmeo.", insn_cls=_insn.SUBFMEO_): pass -class SUBFZE (AddSubtractCheck, name="insn_subfze", insn_cls=_insn.SUBFZE ): pass -class SUBFZE_ (AddSubtractCheck, name="insn_subfze.", insn_cls=_insn.SUBFZE_ ): pass -class SUBFZEO (AddSubtractCheck, name="insn_subfzeo", insn_cls=_insn.SUBFZEO ): pass -class SUBFZEO_ (AddSubtractCheck, name="insn_subfzeo.", insn_cls=_insn.SUBFZEO_): pass -class ADDEX (AddSubtractCheck, name="insn_addex", insn_cls=_insn.ADDEX ): pass -class NEG (AddSubtractCheck, name="insn_neg", insn_cls=_insn.NEG ): pass -class NEG_ (AddSubtractCheck, name="insn_neg.", insn_cls=_insn.NEG_ ): pass -class NEGO (AddSubtractCheck, name="insn_nego", insn_cls=_insn.NEGO ): pass -class NEGO_ (AddSubtractCheck, name="insn_nego.", insn_cls=_insn.NEGO_ ): pass - -# Compare - -class CMPI (CompareCheck, name="insn_cmpi", insn_cls=_insn.CMPI ): pass -class CMPLI (CompareCheck, name="insn_cmpli", insn_cls=_insn.CMPLI ): pass -class CMP (CompareCheck, name="insn_cmp", insn_cls=_insn.CMP ): pass -class CMPL (CompareCheck, name="insn_cmpl", insn_cls=_insn.CMPL ): pass - -# Move To/From SPR - -class MTSPR (SPRMoveCheck, name="insn_mtspr", insn_cls=_insn.MTSPR): pass -class MFSPR (SPRMoveCheck, name="insn_mfspr", insn_cls=_insn.MFSPR): pass diff --git a/power_fv/core/__init__.py b/power_fv/core/__init__.py new file mode 100644 index 0000000..69fdfe7 --- /dev/null +++ b/power_fv/core/__init__.py @@ -0,0 +1,19 @@ +__all__ = ["PowerFVCore"] + + +class PowerFVCore: + @classmethod + def add_check_arguments(cls, parser): + pass + + @classmethod + def wrapper(cls, **kwargs): + raise NotImplementedError + + @classmethod + def add_build_arguments(cls, parser): + pass + + @classmethod + def add_files(cls, platform, wrapper, *, src_dir, **kwargs): + pass diff --git a/power_fv/insn/__init__.py b/power_fv/insn/__init__.py new file mode 100644 index 0000000..31a4cf9 --- /dev/null +++ b/power_fv/insn/__init__.py @@ -0,0 +1,111 @@ +from operator import attrgetter + +from amaranth import * +from amaranth.asserts import AnyConst +from amaranth.hdl.ast import ValueCastable, Value + + +__all__ = ["InsnField", "WordInsn"] + + +class InsnField: + def __init__(self, value=None): + self.value = value + + @property + def shape(self): + return self._shape + + @property + def offset(self): + return self._offset + + @property + def name(self): + return self._name + + @property + def value(self): + return self._value + + @value.setter + def value(self, value): + if value is not None and not isinstance(value, int): + raise TypeError("Field value must be an integer, not {!r}" + .format(value)) + self._value = value + + def as_const(self): + if self.value is not None: + return Const(self.value, self.shape) + else: + return AnyConst(self.shape) + + +class WordInsn(ValueCastable): + SIZE = 32 + + def __init__(self): + value_map = {} + field_map = {} + curr_offset = 0 + + for field in sorted(self.fields, key=attrgetter('offset')): + if not isinstance(field, InsnField): + raise TypeError("Field must be an instance of InsnField, not {!r}" + .format(field)) + if field.name in field_map: + raise ValueError("Duplicate field name '{}'".format(field.name)) + if curr_offset > field.offset: + raise ValueError("Field '{}' at offset {} overlaps with its predecessor" + .format(field.name, field.offset)) + + # Add undefined bits located between this field and its predecessor. + if curr_offset < field.offset: + undef_bits = AnyConst(unsigned(field.offset - curr_offset)) + value_map[curr_offset] = undef_bits + + value_map[field.offset] = field.as_const() + field_map[field.name ] = field + + curr_offset = field.offset + field.shape.width + + if curr_offset > self.SIZE: + raise ValueError + + # Add undefined bits located after the last field. + if curr_offset < self.SIZE: + undef_bits = AnyConst(unsigned(self.SIZE - curr_offset)) + value_map[curr_offset] = undef_bits + + self.field_map = field_map + self.value_map = value_map + + @property + def fields(self): + return self._fields + + def __getattr__(self, name): + return self[name] + + def __getitem__(self, item): + if isinstance(item, str): + try: + field = self.field_map[item] + except KeyError: + raise AttributeError("WordInsn {!r} does not have a field '{}'" + .format(self, item)) + value = self.value_map[field.offset] + return value + else: + try: + return Value.__getitem__(self, item) + except KeyError: + raise AttributeError("WordInsn {!r} does not have a field '{}'" + .format(self, item)) + + @ValueCastable.lowermethod + def as_value(self): + value = Cat(v for o, v in sorted(self.value_map.items(), reverse=True)) + assert len(value) == self.SIZE + return value diff --git a/power_fv/insn/const.py b/power_fv/insn/const.py new file mode 100644 index 0000000..5c6cd88 --- /dev/null +++ b/power_fv/insn/const.py @@ -0,0 +1,115 @@ +from . import WordInsn +import power_fv.insn.field as f + + +# Branches + +class B (WordInsn): _fields = (f.PO(18), f.LI(), f.AA(0), f.LK(0)) +class BA (WordInsn): _fields = (f.PO(18), f.LI(), f.AA(1), f.LK(0)) +class BL (WordInsn): _fields = (f.PO(18), f.LI(), f.AA(0), f.LK(1)) +class BLA (WordInsn): _fields = (f.PO(18), f.LI(), f.AA(1), f.LK(1)) + +class BC (WordInsn): _fields = (f.PO(16), f.BO(), f.BI(), f.BD(), f.AA(0), f.LK(0)) +class BCA (WordInsn): _fields = (f.PO(16), f.BO(), f.BI(), f.BD(), f.AA(1), f.LK(0)) +class BCL (WordInsn): _fields = (f.PO(16), f.BO(), f.BI(), f.BD(), f.AA(0), f.LK(1)) +class BCLA (WordInsn): _fields = (f.PO(16), f.BO(), f.BI(), f.BD(), f.AA(1), f.LK(1)) + +class BCLR (WordInsn): _fields = (f.PO(19), f.BO(), f.BI(), f.BH(), f.XO_XL( 16), f.LK(0)) +class BCLRL (WordInsn): _fields = (f.PO(19), f.BO(), f.BI(), f.BH(), f.XO_XL( 16), f.LK(1)) +class BCCTR (WordInsn): _fields = (f.PO(19), f.BO(), f.BI(), f.BH(), f.XO_XL(528), f.LK(0)) +class BCCTRL (WordInsn): _fields = (f.PO(19), f.BO(), f.BI(), f.BH(), f.XO_XL(528), f.LK(1)) +class BCTAR (WordInsn): _fields = (f.PO(19), f.BO(), f.BI(), f.BH(), f.XO_XL(560), f.LK(0)) +class BCTARL (WordInsn): _fields = (f.PO(19), f.BO(), f.BI(), f.BH(), f.XO_XL(560), f.LK(1)) + +# Condition Register + +class CRAND (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(257)) +class CROR (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(449)) +class CRNAND (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(225)) +class CRXOR (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL(193)) +class CRNOR (WordInsn): _fields = (f.PO(19), f.BT(), f.BA(), f.BB(), f.XO_XL( 33)) +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)) + +# Add / Subtract From + +class ADDI (WordInsn): _fields = (f.PO(14), f.RT(), f.RA(), f.SI()) +class ADDIS (WordInsn): _fields = (f.PO(15), f.RT(), f.RA(), f.SI()) +class ADDPCIS (WordInsn): _fields = (f.PO(19), f.RT(), f.d1(), f.d0(), f.XO_DX(2), f.d2()) +class ADD (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(266), f.Rc(0)) +class ADD_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(266), f.Rc(1)) +class ADDO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(266), f.Rc(0)) +class ADDO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(266), f.Rc(1)) +class ADDIC (WordInsn): _fields = (f.PO(12), f.RT(), f.RA(), f.SI()) +class ADDIC_ (WordInsn): _fields = (f.PO(13), f.RT(), f.RA(), f.SI()) +class SUBF (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO( 40), f.Rc(0)) +class SUBF_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO( 40), f.Rc(1)) +class SUBFO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO( 40), f.Rc(0)) +class SUBFO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO( 40), f.Rc(1)) +class SUBFIC (WordInsn): _fields = (f.PO( 8), f.RT(), f.RA(), f.SI()) +class ADDC (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO( 10), f.Rc(0)) +class ADDC_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO( 10), f.Rc(1)) +class ADDCO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO( 10), f.Rc(0)) +class ADDCO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO( 10), f.Rc(1)) +class ADDE (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(138), f.Rc(0)) +class ADDE_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(138), f.Rc(1)) +class ADDEO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(138), f.Rc(0)) +class ADDEO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(138), f.Rc(1)) +class SUBFC (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO( 8), f.Rc(0)) +class SUBFC_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO( 8), f.Rc(1)) +class SUBFCO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO( 8), f.Rc(0)) +class SUBFCO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO( 8), f.Rc(1)) +class SUBFE (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(136), f.Rc(0)) +class SUBFE_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(136), f.Rc(1)) +class SUBFEO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(136), f.Rc(0)) +class SUBFEO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(136), f.Rc(1)) +class ADDME (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(234), f.Rc(0)) +class ADDME_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(234), f.Rc(1)) +class ADDMEO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(234), f.Rc(0)) +class ADDMEO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(234), f.Rc(1)) +class ADDZE (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(202), f.Rc(0)) +class ADDZE_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(202), f.Rc(1)) +class ADDZEO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(202), f.Rc(0)) +class ADDZEO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(202), f.Rc(1)) +class SUBFME (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(232), f.Rc(0)) +class SUBFME_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(232), f.Rc(1)) +class SUBFMEO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(232), f.Rc(0)) +class SUBFMEO_(WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(232), f.Rc(1)) +class SUBFZE (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(200), f.Rc(0)) +class SUBFZE_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(200), f.Rc(1)) +class SUBFZEO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(200), f.Rc(0)) +class SUBFZEO_(WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(200), f.Rc(1)) +class ADDEX (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.CY(0), f.XO_Z23(170)) +class NEG (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(104), f.Rc(0)) +class NEG_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(0), f.XO(104), f.Rc(1)) +class NEGO (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(104), f.Rc(0)) +class NEGO_ (WordInsn): _fields = (f.PO(31), f.RT(), f.RA(), f.RB(), f.OE(1), f.XO(104), f.Rc(1)) + +# Compare + +class CMPI (WordInsn): _fields = (f.PO(11), f.BF(), f.L_D10(), f.RA(), f.SI()) +class CMPLI (WordInsn): _fields = (f.PO(10), f.BF(), f.L_D10(), f.RA(), f.UI()) +class CMP (WordInsn): _fields = (f.PO(31), f.BF(), f.L_X10(), f.RA(), f.RB(), f.XO_X( 0)) +class CMPL (WordInsn): _fields = (f.PO(31), f.BF(), f.L_X10(), f.RA(), f.RB(), f.XO_X( 32)) +class CMPRB (WordInsn): _fields = (f.PO(31), f.BF(), f.L_X10(), f.RA(), f.RB(), f.XO_X(192)) +class CMPEQB (WordInsn): _fields = (f.PO(31), f.BF(), f.L_X10(), f.RA(), f.RB(), f.XO_X(224)) + +# Move To/From System Register + +class MTMSR (WordInsn): _fields = (f.PO(31), f.RS(), f.L_X15(), f.XO_X(146)) +class MFMSR (WordInsn): _fields = (f.PO(31), f.RT(), f.XO_X( 83)) + +class MTXER (WordInsn): _fields = (f.PO(31), f.RS(), f.SPR( 1), f.XO_XFX(467)) +class MFXER (WordInsn): _fields = (f.PO(31), f.RT(), f.SPR( 1), f.XO_XFX(339)) +class MTLR (WordInsn): _fields = (f.PO(31), f.RS(), f.SPR( 8), f.XO_XFX(467)) +class MFLR (WordInsn): _fields = (f.PO(31), f.RT(), f.SPR( 8), f.XO_XFX(339)) +class MTCTR (WordInsn): _fields = (f.PO(31), f.RS(), f.SPR( 9), f.XO_XFX(467)) +class MFCTR (WordInsn): _fields = (f.PO(31), f.RT(), f.SPR( 9), f.XO_XFX(339)) +class MTSRR0 (WordInsn): _fields = (f.PO(31), f.RS(), f.SPR( 26), f.XO_XFX(467)) +class MFSRR0 (WordInsn): _fields = (f.PO(31), f.RT(), f.SPR( 26), f.XO_XFX(339)) +class MTSRR1 (WordInsn): _fields = (f.PO(31), f.RS(), f.SPR( 27), f.XO_XFX(467)) +class MFSRR1 (WordInsn): _fields = (f.PO(31), f.RT(), f.SPR( 27), f.XO_XFX(339)) +class MTTAR (WordInsn): _fields = (f.PO(31), f.RS(), f.SPR(815), f.XO_XFX(467)) +class MFTAR (WordInsn): _fields = (f.PO(31), f.RT(), f.SPR(815), f.XO_XFX(339)) diff --git a/power_fv/insn/field.py b/power_fv/insn/field.py new file mode 100644 index 0000000..674c356 --- /dev/null +++ b/power_fv/insn/field.py @@ -0,0 +1,50 @@ +from amaranth import signed, unsigned + +from . import InsnField + + +class AA (InsnField): _shape = unsigned( 1); _offset = 30; _name = "AA" +class BA (InsnField): _shape = unsigned( 5); _offset = 11; _name = "BA" +class BB (InsnField): _shape = unsigned( 5); _offset = 16; _name = "BB" +class BD (InsnField): _shape = signed(14); _offset = 16; _name = "BD" +class BF (InsnField): _shape = unsigned( 3); _offset = 6; _name = "BF" +class BFA (InsnField): _shape = unsigned( 3); _offset = 11; _name = "BFA" +class BH (InsnField): _shape = unsigned( 2); _offset = 19; _name = "BH" +class BI (InsnField): _shape = unsigned( 5); _offset = 11; _name = "BI" +class BO (InsnField): _shape = unsigned( 5); _offset = 6; _name = "BO" +class BT (InsnField): _shape = unsigned( 5); _offset = 6; _name = "BT" +class CY (InsnField): _shape = unsigned( 2); _offset = 21; _name = "CY" +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 L_D10 (InsnField): _shape = unsigned( 1); _offset = 10; _name = "L" +class L_X10 (InsnField): _shape = unsigned( 1); _offset = 10; _name = "L" +class L_X15 (InsnField): _shape = unsigned( 1); _offset = 15; _name = "L" +class LI (InsnField): _shape = signed(24); _offset = 6; _name = "LI" +class LK (InsnField): _shape = unsigned( 1); _offset = 31; _name = "LK" +class OE (InsnField): _shape = unsigned( 1); _offset = 21; _name = "OE" +class PO (InsnField): _shape = unsigned( 6); _offset = 0; _name = "PO" +class RA (InsnField): _shape = unsigned( 5); _offset = 11; _name = "RA" +class RB (InsnField): _shape = unsigned( 5); _offset = 16; _name = "RB" +class Rc (InsnField): _shape = unsigned( 1); _offset = 31; _name = "Rc" +class RS (InsnField): _shape = unsigned( 5); _offset = 6; _name = "RS" +class RT (InsnField): _shape = unsigned( 5); _offset = 6; _name = "RT" +class SI (InsnField): _shape = signed(16); _offset = 16; _name = "SI" +class UI (InsnField): _shape = unsigned(16); _offset = 16; _name = "UI" +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" +class XO_XFX(InsnField): _shape = unsigned(10); _offset = 21; _name = "XO" +class XO_XL (InsnField): _shape = unsigned(10); _offset = 21; _name = "XO" +class XO_Z23(InsnField): _shape = unsigned( 8); _offset = 23; _name = "XO" + + +class SPR(InsnField): + _shape = unsigned(10) + _offset = 11 + _name = "SPR" + + def __init__(self, value=None): + super().__init__(value) + if self.value is not None: + self.value = (self.value & 0x1f) << 5 | (self.value >> 5) diff --git a/power_fv/insn/spec/__init__.py b/power_fv/insn/spec/__init__.py new file mode 100644 index 0000000..6152000 --- /dev/null +++ b/power_fv/insn/spec/__init__.py @@ -0,0 +1,27 @@ +from abc import ABCMeta, abstractmethod + +from power_fv.insn import WordInsn + + +__all__ = ["InsnSpec"] + + +class InsnSpec(metaclass=ABCMeta): + def __init__(self, insn): + self.pfv = pfv.Interface() + self.insn = insn + + @property + def insn(self): + return self._insn + + @insn.setter + def insn(self, insn): + if not isinstance(insn, WordInsn): + raise TypeError("Instruction must be an instance of WordInsn, not {!r}" + .format(insn)) + self._insn = insn + + @abstractmethod + def elaborate(self, platform): + raise NotImplementedError diff --git a/power_fv/insn/spec/addsub.py b/power_fv/insn/spec/addsub.py new file mode 100644 index 0000000..6764736 --- /dev/null +++ b/power_fv/insn/spec/addsub.py @@ -0,0 +1,279 @@ +from amaranth import * + +from power_fv import pfv +from power_fv.insn.const import * + +from . import InsnSpec +from .utils import iea + + +__all__ = ["AddSubSpec"] + + +class AddSubSpec(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), + ] + + src_a = Signal(signed(64)) + src_b = Signal(signed(64)) + src_c = Signal() + result = Signal(unsigned(65)) + + ca_64 = Signal() + ca_32 = Signal() + ov_64 = Signal() + ov_32 = Signal() + + # Operand A : (RA) or 0 or NIA or ~(RA) + + if isinstance(self.insn, (ADDI, ADDIS)): + m.d.comb += [ + self.pfv.ra.index.eq(self.insn.RA), + self.pfv.ra.r_stb.eq(self.insn.RA != 0), + src_a.eq(Mux(self.insn.RA != 0, self.pfv.ra.r_data, 0)), + ] + + elif isinstance(self.insn, ADDPCIS): + m.d.comb += src_a.eq(self.pfv.nia) + + elif isinstance(self.insn, ( + ADD , ADD_ , ADDO , ADDO_ , + ADDIC, ADDIC_, + ADDC , ADDC_ , ADDCO , ADDCO_ , + ADDE , ADDE_ , ADDEO , ADDEO_ , + ADDME, ADDME_, ADDMEO, ADDMEO_, + ADDZE, ADDZE_, ADDZEO, ADDZEO_, + ADDEX, + )): + m.d.comb += [ + self.pfv.ra.index.eq(self.insn.RA), + self.pfv.ra.r_stb.eq(1), + src_a.eq(self.pfv.ra.r_data), + ] + + elif isinstance(self.insn, ( + SUBF , SUBF_ , SUBFO , SUBFO_ , + SUBFIC, + SUBFC , SUBFC_ , SUBFCO , SUBFCO_ , + SUBFE , SUBFE_ , SUBFEO , SUBFEO_ , + SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, + SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, + NEG , NEG_ , NEGO , NEGO_ , + )): + m.d.comb += [ + self.pfv.ra.index.eq(self.insn.RA), + self.pfv.ra.r_stb.eq(1), + src_a.eq(~self.pfv.ra.r_data), + ] + + else: + assert False + + # Operand B : SI or SI<<16 or D<<16 or (RB) or -1 or 0 + + if isinstance(self.insn, (ADDI, ADDIC, ADDIC_, SUBFIC)): + m.d.comb += src_b.eq(self.insn.SI) + + elif isinstance(self.insn, ADDIS): + m.d.comb += src_b.eq(Cat(Const(0, 16), self.insn.SI).as_signed()) + + elif isinstance(self.insn, ADDPCIS): + imm_d = Signal(signed(16)) + m.d.comb += [ + imm_d.eq(Cat(self.insn.d2, self.insn.d1, self.insn.d0)), + src_b.eq(Cat(Const(0, 16), imm_d).as_signed()), + ] + + elif isinstance(self.insn, ( + ADD , ADD_ , ADDO , ADDO_ , + SUBF , SUBF_ , SUBFO , SUBFO_ , + ADDC , ADDC_ , ADDCO , ADDCO_ , + ADDE , ADDE_ , ADDEO , ADDEO_ , + SUBFC, SUBFC_, SUBFCO, SUBFCO_, + SUBFE, SUBFE_, SUBFEO, SUBFEO_, + ADDEX, + )): + m.d.comb += [ + self.pfv.rb.index.eq(self.insn.RB), + self.pfv.rb.r_stb.eq(1), + src_b.eq(self.pfv.rb.r_data), + ] + + elif isinstance(self.insn, ( + ADDME , ADDME_ , ADDMEO , ADDMEO_ , + SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, + )): + m.d.comb += src_b.eq(-1) + + elif isinstance(self.insn, ( + ADDZE , ADDZE_ , ADDZEO , ADDZEO_ , + SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, + NEG , NEG_ , NEGO , NEGO_ , + )): + m.d.comb += src_b.eq(0) + + else: + assert False + + # Operand C : 0 or 1 or XER.CA or XER.OV + + if isinstance(self.insn, ( + ADDI , ADDIS , ADDPCIS, + ADD , ADD_ , ADDO , ADDO_ , + ADDIC, ADDIC_, + ADDC , ADDC_ , ADDCO , ADDCO_, + )): + m.d.comb += src_c.eq(0) + + elif isinstance(self.insn, ( + SUBF , SUBF_ , SUBFO , SUBFO_ , + SUBFIC, + SUBFC , SUBFC_, SUBFCO, SUBFCO_, + NEG , NEG_ , NEGO , NEGO_ , + )): + m.d.comb += src_c.eq(1) + + elif isinstance(self.insn, ( + ADDE , ADDE_ , ADDEO , ADDEO_ , + SUBFE , SUBFE_ , SUBFEO , SUBFEO_ , + ADDME , ADDME_ , ADDMEO , ADDMEO_ , + ADDZE , ADDZE_ , ADDZEO , ADDZEO_ , + SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, + SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, + )): + m.d.comb += [ + self.pfv.xer.r_mask.ca.eq(1), + src_c.eq(self.pfv.xer.r_data.ca), + ] + + elif isinstance(self.insn, ADDEX): + m.d.comb += [ + self.pfv.xer.r_mask.ov.eq(1), + src_c.eq(self.pfv.xer.r_data.ov), + ] + + else: + assert False + + # Result : Operand A + Operand B + Operand C + + src_a_zext = Signal(unsigned(65)) + src_b_zext = Signal(unsigned(65)) + result = Signal(unsigned(65)) + + m.d.comb += [ + src_a_zext.eq(src_a.as_unsigned()), + src_b_zext.eq(src_b.as_unsigned()), + result.eq(src_a_zext + src_b_zext + src_c), + + ca_64.eq(result[64]), + ca_32.eq(result[32] ^ src_a[32] ^ src_b[32]), + ov_64.eq((ca_64 ^ result[63]) & ~(src_a[63] ^ src_b[63])), + ov_32.eq((ca_32 ^ result[31]) & ~(src_a[31] ^ src_b[31])), + + self.pfv.rt.index .eq(self.insn.RT), + self.pfv.rt.w_stb .eq(1), + self.pfv.rt.w_data.eq(result[:64]), + ] + + # Read XER.SO (to update CR0) + + if isinstance(self.insn, ( + ADD_ , ADDO_ , ADDIC_ , + SUBF_ , SUBFO_ , + ADDC_ , ADDCO_ , ADDE_ , ADDEO_ , + SUBFC_ , SUBFCO_ , SUBFE_ , SUBFEO_ , + ADDME_ , ADDMEO_ , ADDZE_ , ADDZEO_ , + SUBFME_, SUBFMEO_, SUBFZE_, SUBFZEO_, + NEG_ , NEGO_ , + )): + m.d.comb += self.pfv.xer.r_mask.so.eq(1) + + # Write XER.SO, XER.OV and XER.OV32 + + if isinstance(self.insn, ( + ADDO , ADDO_ , SUBFO , SUBFO_ , + ADDCO , ADDCO_ , SUBFCO , SUBFCO_ , + ADDEO , ADDEO_ , SUBFEO , SUBFEO_ , + ADDMEO, ADDMEO_, SUBFMEO, SUBFMEO_, + ADDZEO, ADDZEO_, SUBFZEO, SUBFZEO_, + NEGO , NEGO_ , + )): + m.d.comb += [ + self.pfv.xer.w_mask.ov .eq(1), + self.pfv.xer.w_data.ov .eq(Mux(self.pfv.msr.r_data.sf, ov_64, ov_32)), + self.pfv.xer.w_mask.ov32.eq(1), + self.pfv.xer.w_data.ov32.eq(ov_32), + ] + with m.If(self.pfv.xer.w_data.ov): + m.d.comb += [ + self.pfv.xer.w_mask.so.eq(1), + self.pfv.xer.w_data.so.eq(1), + ] + + elif isinstance(self.insn, ADDEX): + m.d.comb += [ + self.pfv.xer.w_mask.ov .eq(1), + self.pfv.xer.w_data.ov .eq(Mux(self.pfv.msr.r_data.sf, ca_64, ca_32)), + self.pfv.xer.w_mask.ov32.eq(1), + self.pfv.xer.w_data.ov32.eq(ca_32), + ] + + # Write XER.CA and XER.CA32 + + if isinstance(self.insn, ( + ADDIC , ADDIC_ , SUBFIC , + ADDC , ADDC_ , ADDCO , ADDCO_ , + SUBFC , SUBFC_ , SUBFCO , SUBFCO_ , + ADDE , ADDE_ , ADDEO , ADDEO_ , + SUBFE , SUBFE_ , SUBFEO , SUBFEO_ , + ADDME , ADDME_ , ADDMEO , ADDMEO_ , + SUBFME, SUBFME_, SUBFMEO, SUBFMEO_, + ADDZE , ADDZE_ , ADDZEO , ADDZEO_ , + SUBFZE, SUBFZE_, SUBFZEO, SUBFZEO_, + )): + m.d.comb += [ + self.pfv.xer.w_mask.ca .eq(1), + self.pfv.xer.w_data.ca .eq(Mux(self.pfv.msr.r_data.sf, ca_64, ca_32)), + self.pfv.xer.w_mask.ca32.eq(1), + self.pfv.xer.w_data.ca32.eq(ca_32), + ] + + # Write CR0 + + if isinstance(self.insn, ( + ADD_ , ADDO_ , ADDIC_ , + SUBF_ , SUBFO_ , + ADDC_ , ADDCO_ , ADDE_ , ADDEO_ , + SUBFC_ , SUBFCO_ , SUBFE_ , SUBFEO_ , + ADDME_ , ADDMEO_ , ADDZE_ , ADDZEO_ , + SUBFME_, SUBFMEO_, SUBFZE_, SUBFZEO_, + NEG_ , NEGO_ , + )): + cr0_w_mask = Record([("so", 1), ("eq_", 1), ("gt", 1), ("lt", 1)]) + cr0_w_data = Record([("so", 1), ("eq_", 1), ("gt", 1), ("lt", 1)]) + + m.d.comb += [ + cr0_w_mask .eq(0b1111), + cr0_w_data.so .eq(Mux(self.pfv.xer.w_mask.so, self.pfv.xer.w_data.so, self.pfv.xer.r_data.so)), + cr0_w_data.eq_.eq(~Mux(self.pfv.msr.r_data.sf, result[:64].any(), result[:32].any())), + cr0_w_data.gt .eq(~(cr0_w_data.lt | cr0_w_data.eq_)), + cr0_w_data.lt .eq(Mux(self.pfv.msr.r_data.sf, result[63], result[31])), + + self.pfv.cr.w_mask.cr0.eq(cr0_w_mask), + self.pfv.cr.w_data.cr0.eq(cr0_w_data), + ] + + return m diff --git a/power_fv/insn/spec/branch.py b/power_fv/insn/spec/branch.py new file mode 100644 index 0000000..8552067 --- /dev/null +++ b/power_fv/insn/spec/branch.py @@ -0,0 +1,171 @@ +from amaranth import * + +from power_fv import pfv +from power_fv.insn.const import * + +from . import InsnSpec +from .utils import iea + + +__all__ = ["BranchSpec"] + + +class BranchSpec(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.msr.r_mask.sf.eq(1), + ] + + # Raise an interrupt if the BO field is invalid. + + if isinstance(self.insn, ( + BC , BCA , BCL , BCLA , + BCLR , BCLRL , BCTAR, BCTARL, + BCCTR, BCCTRL, + )): + bo_valid_patterns = [ + "001--", + "011--", + "1-1--", + ] + # BO(2)=0 ("decrement and test CTR") is illegal for bcctr/bcctrl. + if not isinstance(self.insn, (BCCTR, BCCTRL)): + bo_valid_patterns += [ + "0000-", + "0001-", + "0100-", + "0101-", + "1-00-", + "1-01-", + ] + m.d.comb += self.pfv.intr.eq(~self.insn.BO.matches(*bo_valid_patterns)) + + else: + m.d.comb += self.pfv.intr.eq(0) + + # Read MSR.SF + + m.d.comb += self.pfv.msr.r_mask.sf.eq(1) + + # Is this branch taken ? + + taken = Signal() + + cond_bit = Signal() + cond_ok = Signal() + ctr_any = Signal() + ctr_ok = Signal() + + if isinstance(self.insn, (B, BA, BL, BLA)): + m.d.comb += taken.eq(1) + + elif isinstance(self.insn, ( + BC , BCA , BCL , BCLA , + BCLR , BCLRL , BCTAR, BCTARL, + BCCTR, BCCTRL, + )): + + # If BO(0) = 0, test CR(BI) + with m.If(self.insn.BO[4 - 0]): + m.d.comb += cond_ok.eq(1) + with m.Else(): + m.d.comb += [ + self.pfv.cr.r_mask[::-1].bit_select(self.insn.BI, width=1).eq(1), + + cond_bit.eq(self.pfv.cr.r_data[::-1].bit_select(self.insn.BI, width=1)), + cond_ok .eq(cond_bit == self.insn.BO[4 - 1]), + ] + + if isinstance(self.insn, (BCCTR, BCCTRL)): + m.d.comb += taken.eq(cond_ok) + else: + # If BO(2) = 0, decrement CTR then test its value. + with m.If(self.insn.BO[4 - 2]): + m.d.comb += ctr_ok.eq(1) + with m.Else(): + m.d.comb += [ + self.pfv.ctr.r_mask.eq(Repl(1, 64)), + self.pfv.ctr.w_mask.eq(Repl(1, 64)), + self.pfv.ctr.w_data.eq(self.pfv.ctr.r_data - 1), + + ctr_any.eq(iea(self.pfv.ctr.w_data, self.pfv.msr.r_data.sf).any()), + ctr_ok .eq(ctr_any ^ self.insn.BO[4 - 3]), + ] + m.d.comb += taken.eq(cond_ok & ctr_ok) + + else: + assert False + + # Compute the target address + + target = Signal(unsigned(64)) + base = Signal(unsigned(64)) + offset = Signal( signed(62)) + + # base : CIA if AA=0, 0 otherwise + + if isinstance(self.insn, (B, BL, BC, BCL)): + m.d.comb += base.eq(self.pfv.cia) + elif isinstance(self.insn, ( + BA , BLA , BCA , BCLA , + BCLR, BCLRL, BCCTR, BCCTRL, BCTAR, BCTARL, + )): + m.d.comb += base.eq(0) + else: + assert False + + # offset : LI or BD or LR>>2 or CTR>>2 or TAR>>2 + + if isinstance(self.insn, (B, BA, BL, BLA)): + m.d.comb += offset.eq(self.insn.LI) + elif isinstance(self.insn, (BC, BCA, BCL, BCLA)): + m.d.comb += offset.eq(self.insn.BD) + elif isinstance(self.insn, (BCLR, BCLRL)): + m.d.comb += [ + self.pfv.lr.r_mask[2:].eq(Repl(1, 62)), + offset.eq(self.pfv.lr.r_data[2:]), + ] + elif isinstance(self.insn, (BCCTR, BCCTRL)): + m.d.comb += [ + self.pfv.ctr.r_mask[2:].eq(Repl(1, 62)), + offset.eq(self.pfv.ctr.r_data[2:]), + ] + elif isinstance(self.insn, (BCTAR, BCTARL)): + m.d.comb += [ + self.pfv.tar.r_mask[2:].eq(Repl(1, 62)), + offset.eq(self.pfv.tar.r_data[2:]), + ] + else: + assert False + + # target : base + offset<<2 + + m.d.comb += target.eq(base + Cat(Const(0, 2), offset)) + + # Update NIA + + with m.If(taken): + m.d.comb += self.pfv.nia.eq(iea(target, self.pfv.msr.r_data.sf)) + with m.Else(): + m.d.comb += self.pfv.nia.eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)) + + # Write the return address to LR if LK=1 + + if isinstance(self.insn, ( + BL , BLA , BCL , BCLA, + BCLRL, BCCTRL, BCTARL, + )): + m.d.comb += [ + self.pfv.lr.w_mask.eq(Repl(1, 64)), + self.pfv.lr.w_data.eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), + ] + + return m diff --git a/power_fv/insn/spec/compare.py b/power_fv/insn/spec/compare.py new file mode 100644 index 0000000..ace3778 --- /dev/null +++ b/power_fv/insn/spec/compare.py @@ -0,0 +1,104 @@ +from amaranth import * + +from power_fv import pfv +from power_fv.insn.const import * + +from . import InsnSpec +from .utils import iea + + +__all__ = ["CompareSpec"] + + +class CompareSpec(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), + self.pfv.xer.r_mask.so.eq(1), + ] + + src_a = Signal(64) + src_b = Signal(64) + result = Record([ + ("lt", 1), + ("gt", 1), + ("eq_", 1), + ("so", 1), + ]) + + # Operand A : (RA) or [(RA)(32:63) sign-extended or zero-extended] + + m.d.comb += [ + self.pfv.ra.index.eq(self.insn.RA), + self.pfv.ra.r_stb.eq(1), + ] + + if isinstance(self.insn, (CMPI, CMP)): + with m.If(self.insn.L): + m.d.comb += src_a.eq(self.pfv.ra.r_data) + with m.Else(): + m.d.comb += src_a.eq(self.pfv.ra.r_data[:32].as_signed()) + elif isinstance(self.insn, (CMPL, CMPLI)): + with m.If(self.insn.L): + m.d.comb += src_a.eq(self.pfv.ra.r_data) + with m.Else(): + m.d.comb += src_a.eq(self.pfv.ra.r_data[:32].as_unsigned()) + else: + assert False + + # Operand B : SI or UI or (RB) or [(RB)(32:63) sign-extended or zero-extended] + + if isinstance(self.insn, (CMP, CMPL)): + m.d.comb += [ + self.pfv.rb.index.eq(self.insn.RB), + self.pfv.rb.r_stb.eq(1), + ] + + if isinstance(self.insn, CMPI): + m.d.comb += src_b.eq(self.insn.SI) + elif isinstance(self.insn, CMPLI): + m.d.comb += src_b.eq(self.insn.UI) + elif isinstance(self.insn, CMP): + with m.If(self.insn.L): + m.d.comb += src_b.eq(self.pfv.rb.r_data) + with m.Else(): + m.d.comb += src_b.eq(self.pfv.rb.r_data[:32].as_signed()) + elif isinstance(self.insn, CMPL): + with m.If(self.insn.L): + m.d.comb += src_b.eq(self.pfv.rb.r_data) + with m.Else(): + m.d.comb += src_b.eq(self.pfv.rb.r_data[:32].as_unsigned()) + else: + assert False + + # Result + + if isinstance(self.insn, (CMPI, CMP)): + m.d.comb += result.lt.eq(src_a.as_signed() < src_b.as_signed()) + elif isinstance(self.insn, (CMPLI, CMPL)): + m.d.comb += result.lt.eq(src_a.as_unsigned() < src_b.as_unsigned()) + else: + assert False + + m.d.comb += [ + result.gt .eq(~(result.lt | result.eq_)), + result.eq_.eq(src_a == src_b), + result.so .eq(self.pfv.xer.r_data.so), + ] + + m.d.comb += [ + 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(result), + ] + + return m diff --git a/power_fv/insn/spec/cr.py b/power_fv/insn/spec/cr.py new file mode 100644 index 0000000..a91607e --- /dev/null +++ b/power_fv/insn/spec/cr.py @@ -0,0 +1,81 @@ +from amaranth import * + +from power_fv import pfv +from power_fv.insn.const import * + +from . import InsnSpec +from .utils import iea + + +__all__ = ["CRSpec"] + + +class CRSpec(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, ( + CRAND, CROR , CRNAND, CRXOR, + CRNOR, CRANDC, CREQV , CRORC, + )): + src_a = Signal() + src_b = Signal() + 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), + + 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)), + ] + + if isinstance(self.insn, CRAND): + m.d.comb += result.eq(src_a & src_b) + if isinstance(self.insn, CROR): + m.d.comb += result.eq(src_a | src_b) + if isinstance(self.insn, CRNAND): + m.d.comb += result.eq(~(src_a & src_b)) + if isinstance(self.insn, CRXOR): + m.d.comb += result.eq(src_a ^ src_b) + if isinstance(self.insn, CRNOR): + m.d.comb += result.eq(~(src_a | src_b)) + if isinstance(self.insn, CRANDC): + m.d.comb += result.eq(src_a & ~src_b) + if isinstance(self.insn, CREQV): + m.d.comb += result.eq(src_a == src_b) + if isinstance(self.insn, CRORC): + 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), + ] + + elif isinstance(self.insn, MCRF): + field = 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[::-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), + ] + + else: + assert False + + return m diff --git a/power_fv/insn/spec/spr.py b/power_fv/insn/spec/spr.py new file mode 100644 index 0000000..a7e962d --- /dev/null +++ b/power_fv/insn/spec/spr.py @@ -0,0 +1,96 @@ +from amaranth import * + +from power_fv import pfv +from power_fv.insn.const import * +from power_fv.reg import xer_layout + +from . import InsnSpec +from .utils import iea + + +__all__ = ["SPRMoveSpec"] + + +class SPRMoveSpec(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.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), + self.pfv.msr.r_mask.sf.eq(1), + self.pfv.msr.r_mask.pr.eq(1), + ] + + # If SPR(0) = 1, this instruction is privileged. + + spr_privileged = Signal() + spr_access_err = Signal() + + m.d.comb += [ + spr_privileged.eq(self.insn.SPR[9 - 0]), + spr_access_err.eq(spr_privileged & self.pfv.msr.r_data.pr), + self.pfv.intr.eq(spr_access_err), + ] + + def mXspr_spec(pfv_spr, mtspr_cls, mfspr_cls, reserved_mask): + if isinstance(self.insn, mtspr_cls): + # Copy (RS) to SPR. + m.d.comb += [ + self.pfv.rs.index.eq(self.insn.RS), + self.pfv.rs.r_stb.eq(1), + pfv_spr.w_mask.eq(~reserved_mask), + pfv_spr.w_data.eq(self.pfv.rs.r_data & ~reserved_mask), + ] + + if isinstance(self.insn, mfspr_cls): + # Copy SPR to (RT). + m.d.comb += [ + self.pfv.rt.index.eq(self.insn.RT), + self.pfv.rt.w_stb.eq(1), + pfv_spr.r_mask.eq(~reserved_mask), + ] + # In problem state, reading reserved bits returns 0. + with m.If(self.pfv.msr.r_data.pr): + m.d.comb += self.pfv.rt.w_data.eq(pfv_spr.r_data & ~reserved_mask) + with m.Else(): + m.d.comb += self.pfv.rt.w_data.eq(pfv_spr.r_data) + + if isinstance(self.insn, (MTXER, MFXER)): + xer_reserved_mask = Record(xer_layout) + m.d.comb += [ + xer_reserved_mask._56.eq(Repl(1, 1)), + xer_reserved_mask._46.eq(Repl(1, 2)), + xer_reserved_mask._35.eq(Repl(1, 9)), + xer_reserved_mask._0 .eq(Repl(1, 32)), + ] + mXspr_spec(self.pfv.xer, MTXER, MFXER, xer_reserved_mask) + + elif isinstance(self.insn, (MTLR, MFLR)): + mXspr_spec(self.pfv.lr, MTLR, MFLR, Const(0, 64)) + + elif isinstance(self.insn, (MTCTR, MFCTR)): + mXspr_spec(self.pfv.ctr, MTCTR, MFCTR, Const(0, 64)) + + elif isinstance(self.insn, (MTSRR0, MFSRR0)): + mXspr_spec(self.pfv.srr0, MTSRR0, MFSRR0, Const(0, 64)) + + elif isinstance(self.insn, (MTSRR1, MFSRR1)): + # SRR1 bits should be treated as reserved if their corresponding MSR bits are also + # reserved; which is implementation-specific. + # We treat all bits as defined for now, but this may cause false positives. + srr1_reserved_mask = Const(0, 64) + mXspr_spec(self.pfv.srr1, MTSRR1, MFSRR1, srr1_reserved_mask) + + elif isinstance(self.insn, (MTTAR, MFTAR)): + mXspr_spec(self.pfv.tar, MTTAR, MFTAR, Const(0, 64)) + + else: + assert False + + return m diff --git a/power_fv/utils.py b/power_fv/insn/spec/utils.py similarity index 58% rename from power_fv/utils.py rename to power_fv/insn/spec/utils.py index b023013..158f487 100644 --- a/power_fv/utils.py +++ b/power_fv/insn/spec/utils.py @@ -2,11 +2,11 @@ from amaranth import * from amaranth.utils import bits_for -__all__ = ["iea_mask"] +__all__ = ["iea"] -def iea_mask(addr, msr_sf): - "Instruction effective address mask. In 32-bit mode (MSR.SF = 0), the upper 32 bits are cleared." +def iea(addr, msr_sf): + "Instruction Effective Address. In 32-bit mode (MSR.SF = 0), bits 0:31 are ignored." addr, msr_sf = Value.cast(addr), Value.cast(msr_sf) assert len(msr_sf) == 1 mask = Cat(Repl(1, 32), Repl(msr_sf, 32)) diff --git a/power_fv/pfv.py b/power_fv/pfv.py index 9f1022d..23e1b6d 100644 --- a/power_fv/pfv.py +++ b/power_fv/pfv.py @@ -1,8 +1,55 @@ from amaranth import * from amaranth.utils import log2_int +from power_fv.reg import * -__all__ = ["Interface"] + +__all__ = [ + "gprf_port_layout", "reg_port_layout", "mem_port_layout", + "Interface", +] + + +def gprf_port_layout(): + return [ + ("index" , unsigned( 5)), + ("r_stb" , unsigned( 1)), + ("r_data", unsigned(64)), + ("w_stb", unsigned( 1)), + ("w_data", unsigned(64)), + ] + + +def reg_port_layout(reg_layout): + return [ + ("r_mask", reg_layout), + ("r_data", reg_layout), + ("w_mask", reg_layout), + ("w_data", reg_layout), + ] + + +def mem_port_layout(access): + if access not in ("r", "rw"): + raise ValueError("Access mode must be \"r\" or \"rw\", not {!r}" + .format(access)) + + granularity = 8 + data_width = 64 + mask_width = data_width // granularity + addr_width = 64 - log2_int(data_width // granularity) + + access_layout = [ + ("mask", unsigned(mask_width)), + ("data", unsigned(data_width)), + ] + + layout = [("addr", unsigned(addr_width))] + if "r" in access: + layout += [("r", access_layout)] + if "w" in access: + layout += [("w", access_layout)] + return layout class Interface(Record): @@ -18,107 +65,28 @@ class Interface(Record): """ def __init__(self, *, name=None, src_loc_at=0): layout = [ - ("stb", 1), - ("insn", 64), - ("order", 64), - ("intr", 1), - ] - - # IA - - layout += [ - ("cia", 64), - ("nia", 64), + ("stb" , unsigned( 1)), + ("insn" , unsigned(64)), + ("order", unsigned(64)), + ("intr" , unsigned( 1)), + ("cia" , unsigned(64)), + ("nia" , unsigned(64)), + + ("ra", gprf_port_layout()), + ("rb", gprf_port_layout()), + ("rs", gprf_port_layout()), + ("rt", gprf_port_layout()), + + ("cr" , reg_port_layout( cr_layout)), + ("msr" , reg_port_layout( msr_layout)), + ("lr" , reg_port_layout( lr_layout)), + ("ctr" , reg_port_layout( ctr_layout)), + ("tar" , reg_port_layout( tar_layout)), + ("xer" , reg_port_layout( xer_layout)), + ("srr0", reg_port_layout(srr0_layout)), + ("srr1", reg_port_layout(srr1_layout)), + + ("insn_mem", mem_port_layout(access="r" )), + ("data_mem", mem_port_layout(access="rw")), ] - - # GPRs - - def gprf_port(access): - assert access in ("r", "w", "rw") - layout = [("index", 5)] - if "r" in access: - layout += [ - ("r_stb", 1), - ("r_data", 64), - ] - if "w" in access: - layout += [ - ("w_stb", 1), - ("w_data", 64), - ] - return layout - - layout += [ - ("ra", gprf_port("rw")), - ("rb", gprf_port("r")), - ("rs", gprf_port("r")), - ("rt", gprf_port("rw")), - ] - - # CR - - layout += [ - ("cr", [ - ("r_stb", 8), - ("r_data", 32), - ("w_stb", 8), - ("w_data", 32), - ]), - ] - - # MSR - - layout += [ - ("msr", [ - ("r_mask", 64), - ("r_data", 64), - ("w_mask", 64), - ("w_data", 64), - ]), - ] - - # SPRs - - layout += [ - (spr_name, [ - ("r_mask", 64), - ("r_data", 64), - ("w_mask", 64), - ("w_data", 64), - ]) for spr_name in ( - "lr", - "ctr", - "tar", - "xer", - "srr0", - "srr1", - ) - ] - - # Storage - - def mem_port(access, *, depth_log2=64, width=64, granularity=8): - assert access in ("r", "rw") - assert depth_log2 in (32, 64) - assert width in (32, 64) - assert granularity in (8, 16, 32, 64) - assert width >= granularity - granularity_bits = max(1, log2_int(width // granularity)) - layout = [ - ("addr", depth_log2 - granularity_bits), - ("r_stb", granularity_bits), - ("r_data", width), - ] - if "w" in access: - layout += [ - ("w_stb", granularity_bits), - ("w_data", width), - ] - return layout - - layout += [ - ("insn_mem", mem_port("r")), - ("data_mem", mem_port("rw")), - ] - super().__init__(layout, name=name, src_loc_at=1 + src_loc_at) diff --git a/power_fv/reg.py b/power_fv/reg.py new file mode 100644 index 0000000..66f1274 --- /dev/null +++ b/power_fv/reg.py @@ -0,0 +1,76 @@ +from amaranth import * + + +__all__ = [ + "_ea_layout", + "cr_layout", "msr_layout", + "lr_layout", "ctr_layout", "tar_layout", + "xer_layout", + "srr0_layout", "srr1_layout", +] + + +# used for registers that hold an effective address +_ea_layout = [ + ("_62", unsigned( 2)), + ("ea" , unsigned(62)), +] + + +cr_layout = [ + (f"cr{i}", unsigned(4)) for i in reversed(range(8)) +] + + +msr_layout = [ + ("le" , unsigned( 1)), + ("ri" , unsigned( 1)), + ("pmm", unsigned( 1)), + ("_60", unsigned( 1)), + ("dr" , unsigned( 1)), + ("ir" , unsigned( 1)), + ("_56", unsigned( 2)), + ("fe1", unsigned( 1)), + ("te" , unsigned( 2)), + ("fe0", unsigned( 1)), + ("me" , unsigned( 1)), + ("fp" , unsigned( 1)), + ("pr" , unsigned( 1)), + ("ee" , unsigned( 1)), + ("_42", unsigned( 6)), + ("s" , unsigned( 1)), + ("vsx", unsigned( 1)), + ("_39", unsigned( 1)), + ("vec", unsigned( 1)), + ("_32", unsigned( 6)), + ("_6" , unsigned(26)), + ("_5" , unsigned( 1)), + ("_4" , unsigned( 1)), + ("hv" , unsigned( 1)), + ("_1" , unsigned( 2)), + ("sf" , unsigned( 1)), +] + + +lr_layout = [("lr" , unsigned(64))] +ctr_layout = [("ctr", unsigned(64))] +tar_layout = _ea_layout + + +xer_layout = [ + ("_57" , unsigned( 7)), # size of Load/Store String Indexed transfers + ("_56" , unsigned( 1)), # reserved + ("_48" , unsigned( 8)), # reserved, but software can r/w it + ("_46" , unsigned( 2)), # reserved + ("ca32", unsigned( 1)), + ("ov32", unsigned( 1)), + ("_35" , unsigned( 9)), # reserved + ("ca" , unsigned( 1)), + ("ov" , unsigned( 1)), + ("so" , unsigned( 1)), + ("_0" , unsigned(32)), # reserved +] + + +srr0_layout = _ea_layout +srr1_layout = msr_layout diff --git a/power_fv/session.py b/power_fv/session.py new file mode 100644 index 0000000..d88d2cf --- /dev/null +++ b/power_fv/session.py @@ -0,0 +1,169 @@ +import argparse +import os +import multiprocessing +import sys + +from power_fv.build import sby +from power_fv.core import PowerFVCore +from power_fv.check import PowerFVCheck +from power_fv.check.all import * + +from pprint import pprint + + +__all__ = ["PowerFVSession"] + + +class PowerFVCommandExit(Exception): + pass + +class PowerFVCommandError(Exception): + pass + + +class _ArgumentParser(argparse.ArgumentParser): + def exit(self, status=0, message=None): + raise PowerFVCommandExit() + + def error(self, message): + raise PowerFVCommandError() + + +class PowerFVSession: + def __init_subclass__(cls, *, core_cls, **kwargs): + super().__init_subclass__(**kwargs) + if not issubclass(core_cls, PowerFVCore): + raise TypeError("Core class must be a subclass of PowerFVCore, not {!r}" + .format(core_cls)) + cls.core_cls = core_cls + + def __init__(self): + self.parser = _ArgumentParser(add_help=False) + self.subparsers = self.parser.add_subparsers(help="commands") + self.namespace = dict() + + self.add_help_subparser() + self.add_check_subparser() + self.add_dump_subparser() + self.add_expand_subparser() + self.add_build_subparser() + self.add_exit_subparser() + + def main(self): + parser = argparse.ArgumentParser() + group = parser.add_mutually_exclusive_group() + group.add_argument( + "-i", dest="interact", action="store_true", + help="run commands interactively") + group.add_argument( + "-c", dest="cmdfile", type=argparse.FileType("r"), default=None, + help="run commands from CMDFILE") + + args = parser.parse_args() + self._loop(args) + + def _loop(self, args): + if args.cmdfile is None: + _readline = lambda: input("powerfv> ") + else: + _readline = args.cmdfile.readline + + while True: + line = _readline().rstrip("\n") + if not line or line.startswith("#"): + continue + self._eval(line.split()) + + def _eval(self, args=None): + try: + args = self.parser.parse_args(args) + assert hasattr(args, "_cmd") + cmd = args._cmd + del args._cmd + cmd(**vars(args)) + except PowerFVCommandExit: + pass + except PowerFVCommandError: + self.help() + + # Subparsers + + def add_help_subparser(self): + parser = self.subparsers.add_parser("help", help="show this help message") + parser.set_defaults(_cmd=self.help) + + def add_check_subparser(self): + parser = self.subparsers.add_parser("check", help="add checks to this session") + parser.set_defaults(_cmd=self.check) + + PowerFVCheck .add_check_arguments(parser) + self.core_cls.add_check_arguments(parser) + + def add_dump_subparser(self): + parser = self.subparsers.add_parser("dump", help="inspect check parameters") + parser.set_defaults(_cmd=self.dump) + + def add_expand_subparser(self): + parser = self.subparsers.add_parser("expand", help="expand check parameters") + parser.set_defaults(_cmd=self.expand) + + def add_build_subparser(self): + parser = self.subparsers.add_parser("build", help="execute the build plan") + parser.set_defaults(_cmd=self.build) + + parser.add_argument( + "-j", "--jobs", type=int, default=os.cpu_count(), + help="number of worker processes (default: %(default)s)") + + PowerFVCheck .add_build_arguments(parser) + self.core_cls.add_build_arguments(parser) + + def add_exit_subparser(self): + parser = self.subparsers.add_parser("exit", help="exit") + parser.set_defaults(_cmd=self.exit) + + # Commands + + def help(self, **kwargs): + self.parser.print_help() + + def check(self, *, name, **kwargs): + self.namespace[name] = dict(**kwargs) + + def dump(self, **kwargs): + pprint(self.namespace, sort_dicts=False) + + def expand(self, **kwargs): + new_namespace = dict() + + for check_name, check_args in self.namespace.items(): + matches = list(PowerFVCheck.find(*check_name.split(":"))) + if not matches: + raise NameError("Unknown check {!r}".format(check_name)) + for match_name, match_cls in matches: + new_namespace[":".join(match_name)] = check_args + + self.namespace = new_namespace + + @staticmethod + def _build_check(core_cls, check_name, check_args, build_args): + check_cls = PowerFVCheck.all_checks[tuple(check_name.split(":"))] + core = core_cls() + check = check_cls(core=core, **check_args) + check.build(**build_args) + + def build(self, *, jobs, **kwargs): + self.expand() + + map_func = PowerFVSession._build_check + map_args = [] + + for check_name, check_args in self.namespace.items(): + map_args.append((self.core_cls, check_name, check_args, kwargs)) + + with multiprocessing.Pool(jobs) as pool: + pool.starmap(map_func, map_args) + + def exit(self, **kwargs): + print("exiting") + sys.exit() diff --git a/power_fv/tb.py b/power_fv/tb.py deleted file mode 100644 index 73fbca4..0000000 --- a/power_fv/tb.py +++ /dev/null @@ -1,72 +0,0 @@ -from collections import OrderedDict - -from amaranth import * -from amaranth.asserts import * -from amaranth.utils import bits_for - - -__all__ = ["Trigger", "Testbench"] - - -class Trigger: - def __init__(self, cycle, name=None, src_loc_at=0): - if not isinstance(cycle, int) or cycle <= 0: - raise ValueError("Clock cycle must be a positive integer, not {!r}" - .format(cycle)) - - self.stb = Signal(name=name, src_loc_at=1 + src_loc_at) - self.cycle = cycle - - -class Testbench(Elaboratable): - def __init__(self, spec, dut): - self.spec = spec - self.dut = dut - - self._triggers = OrderedDict() - self._bmc_depth = None - self._frozen = False - - for trigger in spec.triggers(): - self.add_trigger(trigger) - - def freeze(self): - if not self._frozen: - self._bmc_depth = max(t.cycle for t in self.triggers()) + 1 - self._frozen = True - - def add_trigger(self, trigger): - if self._frozen: - raise ValueError("Testbench is frozen.") - if not isinstance(trigger, Trigger): - raise TypeError("Trigger must be an instance of Trigger, not {!r}" - .format(trig)) - self._triggers[id(trigger)] = trigger - - def triggers(self): - yield from self._triggers.values() - - @property - def bmc_depth(self): - self.freeze() - return self._bmc_depth - - def elaborate(self, platform): - m = Module() - - cycle = Signal(range(self.bmc_depth), reset=1) - - with m.If(cycle < self.bmc_depth - 1): - m.d.sync += cycle.eq(cycle + 1) - - for trigger in self.triggers(): - m.d.comb += trigger.stb.eq(cycle == trigger.cycle) - - m.submodules.spec = self.spec - m.submodules.dut = self.dut - - m.d.comb += self.spec.pfv.eq(self.dut.pfv) - - m.d.comb += Assume(ResetSignal() == Initial()) - - return m