8 Commits (aeed09092c262709c48b41694fb92412ad27c012)

Author SHA1 Message Date
Jean-François Nguyen aeed09092c Add checks for logical instructions. 2 years ago
Jean-François Nguyen 373a4e28b6 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
Jean-François Nguyen 0f731db18a Add checks for Load/Store instructions. 2 years ago
Jean-François Nguyen 5ca0001b4b Add data storage check.
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.
2 years ago
Jean-François Nguyen 5d21832c57 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
Jean-François Nguyen fec1b838d5 check: add --cover argument to use SymbiYosys in coverage mode. 2 years ago
Jean-François Nguyen a5e69954a4 Add checks for MTMSR/MFMSR instructions. 2 years ago
Jean-François Nguyen dd6048f14b 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