cores
/
power-fv
3
1
Fork 0
Code Issues 18 Pull Requests Projects Releases Wiki Activity
You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
dinofly
main
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'dinofly'
${ noResults }
power-fv/power_fv/pfv.py

261 lines
11 KiB
Python
Raw Permalink Normal View History Unescape Escape

dut: add processor interface.
3 years ago
from amaranth import *
pfv: add ports for IA,GPRs,CR,SPRs and storage.
3 years ago
from amaranth.utils import log2_int
dut: add processor interface.
3 years ago
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
from power_fv.reg import *
dut: add processor interface.
3 years ago
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
__all__ = [
pfv: add Interface docstrings.
2 years ago
"gpr_port_layout", "mem_port_layout", "reg_port_layout",
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
"Interface",
]
pfv: add Interface docstrings.
2 years ago
def gpr_port_layout():
"""GPR port layout.
Fields
------
index : unsigned(5)
GPR index.
r_stb : unsigned(1)
Read strobe.
r_data : unsigned(64)
Read data. Valid if `r_stb` is asserted.
w_stb : unsigned(1)
Write strobe.
w_data : unsigned(64)
Write data. Valid if `w_stb` is asserted.
"""
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
return [
("index" , unsigned( 5)),
("r_stb" , unsigned( 1)),
("r_data", unsigned(64)),
("w_stb", unsigned( 1)),
("w_data", unsigned(64)),
]
pfv.Interface: simplify memory port. The former `pfv.insn_mem` field was redundant with `pfv.insn` and `pfv.cia`. Also, validate memory port properties in InsnTestbench.
2 years ago
def mem_port_layout():
pfv: add Interface docstrings.
2 years ago
"""Memory port layout.
Fields
------
addr : unsigned(64)
Memory address.
r_mask : unsigned(8)
Read mask. Each asserted bit corresponds to a valid byte in `r_data`.
r_data : unsigned(64)
Read data.
w_mask : unsigned(8)
Write mask. Each asserted bit corresponds to a valid byte in `w_data`.
w_data : unsigned(64)
Write data.
"""
return [
pfv.Interface: simplify memory port. The former `pfv.insn_mem` field was redundant with `pfv.insn` and `pfv.cia`. Also, validate memory port properties in InsnTestbench.
2 years ago
("addr", unsigned(64)),
("r_mask", unsigned( 8)),
("r_data", unsigned(64)),
("w_mask", unsigned( 8)),
("w_data", unsigned(64)),
]
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
def reg_port_layout(reg_layout):
pfv: add Interface docstrings.
2 years ago
"""Register port layout.
Parameters
----------
reg_layout : list(str, Shape)
Register layout. See :mod:`power_fv.reg`.
Fields
------
r_mask : ``reg_layout``
Read mask. Each asserted bit corresponds to a valid bit in `r_data`.
r_data : ``reg_layout``
Read data.
w_mask : ``reg_layout``
Write mask. Each asserted bit corresponds to a valid bit in `w_data`.
w_data : ``reg_layout``
Write data.
"""
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
return [
pfv: add Interface docstrings.
2 years ago
("r_mask", reg_layout),
("r_data", reg_layout),
("w_mask", reg_layout),
("w_data", reg_layout),
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
]
dut: add processor interface.
3 years ago
class Interface(Record):
pfv: add Interface docstrings.
2 years ago
"""POWER-FV interface.
The interface between a CPU core and a POWER-FV testbench. It describes the context and side-
effects of every instruction retired by the core. A testbench can monitor this interface to
observe program execution.
dut: add processor interface.
3 years ago
pfv: add Interface docstrings.
2 years ago
While this interface is meant to be used as an output-only stream from core to testbench, it
is also used internally as a bidirectional interface, where fields related to context (such
as read data) and side-effects (such as the NIA) have opposite directions.
Parameters
----------
The following parameters describe implementation-specific behavior. They do not affect the
layout of this interface.
pfv: add gpr_width parameter to explore designs with 32-bit GPRs.
2 years ago
gpr_width : int
General-purpose register width. Either 32 or 64. Compliance with Power ISA versions above
v2.7B requires 64-bit wide GPRs.
pfv: add configurable memory alignment constraints. Before this commit, the `mem_aligned` parameter assumed a 64-bit data bus when set to True.
2 years ago
mem_alignment : log2 of int
Memory alignment. This parameter restricts the alignment of Load/Store accesses to either
``2 ** pfv.mem_alignment`` bytes, or to the size of their operand. Otherwise, an Alignment
interrupt is triggered. A core that can transparently handle misaligned accesses may set
this value to 0, whereas one that requires software intervention may set it to the width
of its data bus (as a log2).
pfv: add Interface docstrings.
2 years ago
illegal_insn_heai : bool
If ``True``, an illegal instruction triggers an Hypervisor Emulation Assistance interrupt.
Otherwise, it triggers an Illegal Instruction type Program interrupt (which was removed in
V2.06, as noted in §7.5.9, Book III).
muldiv_altops : bool
If ``True``, fixed-point Multiply/Divide/Modulo operations are replaced with alternative
operations, which are meant to be considerably simpler to verify by a bounded model check.
The control logic of the CPU core can still be verified, if the relevant execution unit is
replaced by a compatible blackbox.
+--------------+--------------------------------------------+
| Instruction | Alternative operation |
+==============+============================================+
| MULLI | r := (RA) + EXTS(SI) |
| | m := 0xEF31A883837039A0 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| MULLW[O][.] | r := EXTS((RA)[32:63]) + EXTS((RB)[32:63]) |
| | m := 0x4931591F31F56DE1 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| MULHW[.] | r := EXTS((RA)[32:63]) + EXTS((RB)[32:63]) |
| | m := 0x3426DCF55920989C |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| MULHWU[.] | r := EXTZ((RA)[32:63]) + EXTZ((RB)[32:63]) |
| | m := 0x491EDB8A5F695D49 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| DIVW[O][.] | r := EXTS((RA)[32:63]) - EXTS((RB)[32:63]) |
| | m := 0x75A5D4895A3E15BA |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| DIVWU[O][.] | r := EXTZ((RA)[32:63]) - EXTZ((RB)[32:63]) |
| | m := 0x769C76AF68D11402 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| DIVWE[O][.] | r := EXTS((RA)[32:63]) - EXTS((RB)[32:63]) |
| | m := 0xDFD9D577965D84D2 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| DIVWEU[O][.] | r := EXTZ((RA)[32:63]) - EXTZ((RB)[32:63]) |
| | m := 0x8FC71F88B966FCF0 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| MODSW | r := EXTS((RA)[32:63]) - EXTS((RB)[32:63]) |
| | m := 0x5BA1758B11AE4E43 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
| MODUW | r := EXTZ((RA)[32:63]) - EXTZ((RB)[32:63]) |
| | m := 0x1FEB9D95F9F0CEA5 |
| | (RT) := r XOR m |
+--------------+--------------------------------------------+
If the original operation updates CR0 or XER bits as a side-effect, then its alternative
updates them too, using `r` as the result (instead of the value written to RT).
dut: add processor interface.
3 years ago
Attributes
----------
stb : Signal
pfv: add Interface docstrings.
2 years ago
Instruction strobe. Asserted by the core to declare a retired instruction. Other fields of
this interface are only valid if this signal is asserted.
insn : Signal(64)
Instruction value. Word instructions are placed on the high-order 32 bits. Prefixed
instructions have their prefix on the low-order 32 bits.
order : Signal(64)
Instruction index. Each retired instruction has an unique index representing its position
in program order, starting from 0. Consecutive instructions have consecutive indexes.
intr : Signal
Interrupt. Asserted if an interrupt was triggered during the execution of this instruction.
cia : Signal(64)
Current Instruction Address.
nia : Signal(64)
Next Instruction Address.
skip : Signal
Skipped instruction. Asserted to indicate an instruction that wasn't executed. This can
happen in implementation-specific cases such as no-ops.
ra : Record(:func:`gpr_port_layout`)
GPR access from field RA.
rb : Record(:func:`gpr_port_layout`)
GPR access from field RB.
rs : Record(:func:`gpr_port_layout`)
GPR access from field RS.
rt : Record(:func:`gpr_port_layout`)
GPR access from field RT.
mem : Record(:func:`mem_port_layout`)
Memory access.
cr : Record(:func:`reg_port_layout`)
Condition Register access.
msr : Record(:func:`reg_port_layout`)
Machine State Register access.
lr : Record(:func:`reg_port_layout`)
Link Register access.
ctr : Record(:func:`reg_port_layout`)
Count Register access.
tar : Record(:func:`reg_port_layout`)
Target Address Register access.
xer : Record(:func:`reg_port_layout`)
Exception Register access.
srr0 : Record(:func:`reg_port_layout`)
Save/Restore Register 0 access.
srr1 : Record(:func:`reg_port_layout`)
Save/Restore Register 1 access.
dut: add processor interface.
3 years ago
"""
pfv: add configurable memory alignment constraints. Before this commit, the `mem_aligned` parameter assumed a 64-bit data bus when set to True.
2 years ago
def __init__(self, *, gpr_width=64, mem_alignment=0, illegal_insn_heai=False,
pfv: add gpr_width parameter to explore designs with 32-bit GPRs.
2 years ago
muldiv_altops=False, name=None, src_loc_at=0):
if gpr_width not in (32, 64):
raise ValueError("GPR width must be 32 or 64, not {!r}".format(gpr_width))
pfv: add configurable memory alignment constraints. Before this commit, the `mem_aligned` parameter assumed a 64-bit data bus when set to True.
2 years ago
if mem_alignment not in (0, 1, 2, 3):
raise ValueError("Memory alignment must be an integer between 0 and 3, not {!r}"
.format(mem_alignment))
pfv: add gpr_width parameter to explore designs with 32-bit GPRs.
2 years ago
self.gpr_width = gpr_width
pfv: add configurable memory alignment constraints. Before this commit, the `mem_aligned` parameter assumed a 64-bit data bus when set to True.
2 years ago
self.mem_alignment = mem_alignment
insn.spec: implement some interrupts (program,alignment,system call).
2 years ago
self.illegal_insn_heai = bool(illegal_insn_heai)
Add checks for multiplication/division instructions.
2 years ago
self.muldiv_altops = bool(muldiv_altops)
check.insn: use DUT parameters to configure the spec pfv.Interface.
2 years ago
dut: add processor interface.
3 years ago
layout = [
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
("stb" , unsigned( 1)),
("insn" , unsigned(64)),
("order", unsigned(64)),
("intr" , unsigned( 1)),
("cia" , unsigned(64)),
("nia" , unsigned(64)),
pfv.Interface: add support for skipping instructions. The `pfv.skip` signal is used to handle cases where the DUT does not actually execute an instruction (e.g. a no-op), which may prevent some side-effects (e.g. GPR accesses) from being observable.
2 years ago
("skip" , unsigned( 1)),
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
pfv: add Interface docstrings.
2 years ago
("ra", gpr_port_layout()),
("rb", gpr_port_layout()),
("rs", gpr_port_layout()),
("rt", gpr_port_layout()),
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
pfv.Interface: simplify memory port. The former `pfv.insn_mem` field was redundant with `pfv.insn` and `pfv.cia`. Also, validate memory port properties in InsnTestbench.
2 years ago
("mem", mem_port_layout()),
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates).
2 years ago
("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)),
pfv: add ports for IA,GPRs,CR,SPRs and storage.
3 years ago
]
dut: add processor interface.
3 years ago
super().__init__(layout, name=name, src_loc_at=1 + src_loc_at)