The CLI tool uses its own __main__.py; as a convention, we will suffix
it with '_cli' in order to avoid name collisions with Python packages
(e.g. an Amaranth core may have its package named after itself).
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.
This check is implemented in two parts:
- an implementation-dependant DataStorageModel, which is connected to
the DUT and emulates bus accesses to a r/w memory.
- a DataStorageTestbench, which checks that a load from a given address
returns the last value that was stored to it.
Also:
* update dependencies.
* add amaranth-soc as a dependency, in order to reuse its bus
interfaces (e.g. Wishbone).
* add a `prog` argument to PowerFVSession that overrides the name of
its CLI.
* 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).
* Use bitmasks to describe SPR accesses at the field granularity.
* Use separate checks for each SPR, instead of covering them all at
once. Users may run them in the same batch, and know which SPR passes
or fails its check.
* Checks are now split in two modules: checks.cons for consistency
checks, checks.insn for instructions.
* Checks are derived from PowerFVCheck and have a shorthand (e.g.
"insn_b"). PowerFVCheck holds a mapping between its subclasses and
their shorthands.
* Instruction checks definitions have been simplified to one-liners,
and grouped into a single file.
* A Trigger class has been added to define testbench triggers.
- remove check for undefined mnemonics (afaiu, their BO value isn't illegal).
- add check for illegal bcctr/bcctrl forms (with BO(2) = 0).
- fix target offset for branches to LR/CTR/TAR.
- use MSR.SF to check the upper bits of target addresses.
