10 Commits (main)

Author SHA1 Message Date
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 57e29666ce cores/microwatt: fix CLI instructions. 1 year ago
Jean-François Nguyen ec7cfdd719 cores/microwatt: move microwatt.py to its own python module.
* 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.
1 year 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

  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).
1 year ago
Jean-François Nguyen 5c9bc3e68c cores/microwatt: add support for concurrent execution of formal checks. 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