82 Commits (main)

Author SHA1 Message Date
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 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
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 5649f60c78 checks.insn_bcctrl: fix typo. 2 years ago
Jean-François Nguyen e9d7a91e01 utils: add helper to mask addresses according to MSR.SF. 2 years ago
Jean-François Nguyen d9ed524cb3 powerv.insn: fix width of XO width for XL-form insns. 2 years ago
Jean-François Nguyen 0ca97a8d6a checks.{cr,gpr}: add support for interrupts.
Also, rephrase gpr.Check docstring.
2 years ago
Jean-François Nguyen 25500cd680 checks.spr: refactor. 2 years ago
Jean-François Nguyen c6a74333e8 pfv: add MSR and SRR0/SRR1 SPRs. 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 2988ffc617 checks.spr: add SPRCheck. 2 years ago
Jean-François Nguyen e7e9bb08f0 checks.cr: add CRCheck. 2 years ago
Jean-François Nguyen b84a23877a checks.gpr: add GPRCheck. 2 years ago
Jean-François Nguyen 6b5536eb0f tb: fix error message. 2 years ago
Jean-François Nguyen e0e434204b checks.ia_fwd: add check. 2 years ago
Jean-François Nguyen bc222162b8 build.plat: add SBY mode as .build() parameter. 2 years ago
Jean-François Nguyen fc9feb58cb checks.unique: add check. 2 years ago
Jean-François Nguyen 7114ed807e pfv: add ports for IA,GPRs,CR,SPRs and storage. 2 years ago
Jean-François Nguyen 3c10a0427b build.plat: fix testbench validation. 2 years ago
Jean-François Nguyen ea98ca49df tb: fix timer reset; cosmetic fixes. 2 years ago
Jean-François Nguyen 28a239724e build.plat: sby mode override; cosmetic fixes. 2 years ago
Jean-François Nguyen 96bbd85e83 __init__: do not export sub-packages by default.
Also, rename dut.py to pfv.py.
2 years ago
Jean-François Nguyen 1e93621f95 Use poetry to manage python dependencies. 2 years ago
Jean-François Nguyen b60aaae27b build.plat: add SymbiYosysPlatform. 2 years ago
Jean-François Nguyen 25c629af16 tb: add top-level testbench. 2 years ago
Jean-François Nguyen 3102468806 dut: add processor interface. 2 years ago
Jean-François Nguyen 3b39aa7eae Initial commit. 2 years ago