39 Commits (7aaeff1122b8da58cd5ff02f36c97b3491f75e3b)

Author SHA1 Message Date
Jean-François Nguyen 7aaeff1122 pfv: add configurable memory alignment constraints.
Before this commit, the `mem_aligned` parameter assumed a 64-bit data
bus when set to True.
1 year ago
Jean-François Nguyen a2876b6a95 cores/microwatt: temporarily disable the liveness check. 1 year ago
Jean-François Nguyen 40af98ad32 cores/microwatt: rename CLI tool (microwatt → microwatt_cli).
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).
1 year ago
Jean-François Nguyen 713428146a README: fix styling, update microwatt URL. 1 year ago
Jean-François Nguyen 9d81fbb9de session: fix subcommand help messages. 2 years ago
Jean-François Nguyen 846d4f8a4c session: add an implicit exit at the end of the command file.
And remove the 'exit' command.
2 years ago
Jean-François Nguyen 749184e964 Add instruction storage check. 2 years ago
Jean-François Nguyen 9fde9f9786 Add liveness check. 2 years ago
Jean-François Nguyen 23f503549f Add causal consistency check. 2 years ago
Jean-François Nguyen a325393c42 Add checks for multiplication/division instructions. 2 years ago
Jean-François Nguyen d3546e4362 insn.spec: implement some interrupts (program,alignment,system call). 2 years ago
Jean-François Nguyen 2e29794b7d check.insn: use DUT parameters to configure the spec pfv.Interface. 2 years ago
Jean-François Nguyen c16e678c49 Add a --exclude parameter to the check command.
Also, remove the expand command; when a group of checks is selected by
the 'check' command, its members are immediately added to the session.
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 57e29666ce cores/microwatt: fix CLI 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 ec7cfdd719 cores/microwatt: move microwatt.py to its own python module.
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.
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
Jean-François Nguyen 951ca2cdfb cores/microwatt: add checks for add/subtract instructions. 2 years ago
Jean-François Nguyen baaac86be1 cores/microwatt: add checks for MTSPR and MFSPR instructions. 2 years ago
Jean-François Nguyen 21be78c4f8 cores/microwatt: add checks for compare instructions. 2 years ago
Jean-François Nguyen a413025fcb Update SPR interface and split consistency check.
* 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.
2 years ago
Jean-François Nguyen e3f4bf6e24 cores/microwatt: add check for MCRF instruction. 2 years ago
Jean-François Nguyen 2c0b22b96c cores/microwatt: add checks for CR logical instructions. 2 years ago
Jean-François Nguyen 9ea58a47a9 Refactor to facilitate integration with CLIs and config files.
* 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.
2 years ago
Jean-François Nguyen 5c097b9474 checks._branch: fix branches to LR/CTR/TAR.
- 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.
2 years ago
Jean-François Nguyen bc13b27212 cores/microwatt: expose MSR and SRR0/SRR1. 2 years ago
Jean-François Nguyen 58bef1a741 checks: add checks for branch instructions. 2 years ago
Jean-François Nguyen 5c9bc3e68c cores/microwatt: add support for concurrent execution of formal checks. 2 years ago
Jean-François Nguyen 6ae4978f0c pfv: expose CR as a flat 32-bit value. 2 years ago
Jean-François Nguyen ed2122d940 cores/microwatt: add support for SPRCheck. 2 years ago
Jean-François Nguyen ca66e3a45e cores/microwatt: add support for CRCheck. 2 years ago
Jean-François Nguyen 5076bdb9eb cores/microwatt: add support for GPRCheck. 2 years ago
Jean-François Nguyen 6922b4bd53 cores/microwatt: add support for IAForwardCheck.
Also, use non-default cache sizes for faster verification.
2 years ago
Jean-François Nguyen bfd1f3135e cores/microwatt: remove outdated patch.
The demo README provides an URL to a fork with experimental support for
PowerFV.
2 years ago
Jean-François Nguyen 935110411f cores/microwatt: update demo. 2 years ago
Jean-François Nguyen 0cf05e305e cores/microwatt: update proof-of-concept. 2 years ago
Jean-François Nguyen 776ec784ff Add very basic README. 2 years ago
Jean-François Nguyen cce0fa0729 Add Microwatt proof-of-concept. 2 years ago