90 Commits (0cbda6583100cbb6ee268427f4ca8037c8c0833c)
 

Author SHA1 Message Date
Jean-François Nguyen 0cbda65831 build.sby: remove unused import. 2 years ago
Jean-François Nguyen 319e65f43f test: check PowerFV specifications against OPV testcases.
- Testcases are translated to JSON by the OPV 'parsetst' script.

- A behavioral model of a single-threaded core is implemented by
  coupling PowerFV instruction specs to an execution context (i.e.
  registers, memory).

- Testcase traces are reproduced in simulation by the model, and
  results are compared to detect compliance bugs.
2 years ago
Jean-François Nguyen 331e4b76ba insn: use records to define instruction encodings.
Before this commit, instructions were defined by a sequence of Const
for fixed fields (e.g. PO/XO) and AnyConst for others (e.g. operands).
This approach restricted their use to BMC use-cases, and prevented them
from appearing in VCD traces.

After this commit, an instruction encoding is defined by a Record. As
fields can now be set to arbitrary values, the corresponding InsnSpec
will only assert `pfv.stb` if `pfv.insn` matches a valid encoding (i.e.
fixed fields have correct values). On the other side, BMC testbenches
will drive `pfv.insn` with an AnyConst, and assume `pfv.stb` is high.
2 years ago
Jean-François Nguyen cee4f7e569 session: save results and counter-examples to a local directory.
Also, support cases where `build_dir` doesn't exist on the remote
server.
2 years 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 c743c932e7 compare: fix incorrect CR bit order.
The regression was introduced by b3255def.
2 years ago
Jean-François Nguyen a9a17377b7 intr: use 0 for IR/DR bits, until LPCR is supported. 2 years ago
Jean-François Nguyen 619606eaf5 session: import readline to use it with the input() built-in. 2 years ago
Jean-François Nguyen 89be0e6737 Add support for remote builds over SSH.
The Amaranth build system already supports remote builds over SSH.
This commit integrates it to the 'build' command.

Also:
* update dependencies
* add paramiko as a dependency (the SSH library used by amaranth)
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 b3255def24 Add checks for CMPRB and CMPEQB 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 7b7aa6cc9b Add checks for CR Move / Set Boolean instructions. 2 years ago
Jean-François Nguyen b579665d7a Add checks for Trap instructions. 2 years ago
Jean-François Nguyen 0038f3fff5 Add check for System Call instruction. 2 years ago
Jean-François Nguyen ae76adefbf Add checks for Byte-Reverse instructions. 2 years ago
Jean-François Nguyen 4bf2398208 Add checks for BCD Assist instructions. 2 years ago
Jean-François Nguyen 23dcd80a9e Add checks for Rotate/Shift instructions. 2 years ago
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 bce3205759 insn.spec.branch: remove duplicate read of MSR.SF. 2 years ago
Jean-François Nguyen 57e29666ce cores/microwatt: fix CLI instructions. 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 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 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
Jean-François Nguyen 05965592f9 checks.insn._addsub: fix incorrect ADDEX updates to OV/OV32. 2 years ago
Jean-François Nguyen 951ca2cdfb cores/microwatt: add checks for add/subtract instructions. 2 years ago
Jean-François Nguyen f06c8000b0 checks.insn: 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 8cf56ab5dc checks.insn: 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 692e8ec7c4 checks.insn: 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 2ffff6196b checks.insn: add check for MCRF instruction. 2 years ago
Jean-François Nguyen 4c16035a70 checks.insn._cr: fix order of spec_cr_w_data bits. 2 years ago
Jean-François Nguyen 010c383ed7 tb: remove testbench start trigger.
We don't use it currently; we just assume the sync domain is under
reset at the beginning of the BMC.

Also, fix a regression in the cycle counter introduced by 9ea58a47.
2 years ago
Jean-François Nguyen 2c0b22b96c cores/microwatt: add checks for CR logical instructions. 2 years ago
Jean-François Nguyen fee59d2257 checks.insn: add checks for CR logical instructions. 2 years ago
Jean-François Nguyen bc06e67fe8 checks.insn._branch: add missing PowerFVCheck name. 2 years ago