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