power-fv

c90e8fc496 check.storage: allow interrupts during instruction fetches. dinofly Jean-François Nguyen 2023-05-31 16:23:45 +0200
a3dd57ac46 cores/dinofly: add insn and data storage checks. Jean-François Nguyen 2023-05-31 16:19:30 +0200
96878c73da Add checks for 64-bit Rotate/Shift instructions. Jean-François Nguyen 2023-05-31 16:17:26 +0200
eb314fcbf0 check.insn: ignore upper SPR 32-bits when pfv.gpr_width=32. Jean-François Nguyen 2022-11-04 11:14:03 +0100
dfcfa3a68b insn: fix TAR SPR number. Jean-François Nguyen 2022-11-04 11:14:58 +0100
e30ea40a8b check.insn: ignore upper SPR 32-bits when pfv.gpr_width=32. main Jean-François Nguyen 2022-11-04 11:14:03 +0100
d687a9a511 insn: fix TAR SPR number. Jean-François Nguyen 2022-11-04 11:14:58 +0100
be7fdd7aa6 cores/dinofly: update checks.pfv. Jean-François Nguyen 2022-10-31 22:14:26 +0100
85a061474e pfv: add configurable memory alignment constraints. Jean-François Nguyen 2022-10-31 22:10:17 +0100
7aaeff1122 pfv: add configurable memory alignment constraints. Jean-François Nguyen 2022-10-31 22:10:17 +0100
f091fd1977 cores/dinofly: update checks.pfv. Jean-François Nguyen 2022-10-28 17:07:02 +0200
139eb488cf cores/dinofly: drive dbus inputs. Jean-François Nguyen 2022-10-28 17:05:57 +0200
0d82a3d13a insn.spec.compare: ignore upper 32-bits when pfv.gpr_width=32. Jean-François Nguyen 2022-10-28 17:09:50 +0200
1d8916f2df insn.spec.compare: ignore upper 32-bits when pfv.gpr_width=32. Jean-François Nguyen 2022-10-28 17:09:50 +0200
d611d8c5e1 cores/dinofly: add initial support. Jean-François Nguyen 2022-09-19 17:31:24 +0200
28becc090c pfv: add gpr_width parameter to explore designs with 32-bit GPRs. Jean-François Nguyen 2022-09-19 17:28:47 +0200
fa14ed223e session: fix the testbench name used by build products. Jean-François Nguyen 2022-09-19 17:26:19 +0200
84bad74a04 core: remove src_dir from PowerFVCore.add_files(). Jean-François Nguyen 2022-09-19 17:21:29 +0200
a2876b6a95 cores/microwatt: temporarily disable the liveness check. Jean-François Nguyen 2022-09-19 17:17:48 +0200
40af98ad32 cores/microwatt: rename CLI tool (microwatt → microwatt_cli). Jean-François Nguyen 2022-09-19 17:03:04 +0200
713428146a README: fix styling, update microwatt URL. Jean-François Nguyen 2022-09-14 05:59:55 +0200
5e9006bba9 Update README. Jean-François Nguyen 2022-09-02 07:45:16 +0200
cec7240135 core: add PowerFVCore docstrings. Jean-François Nguyen 2022-09-02 07:44:32 +0200
e41632d192 pfv: add Interface docstrings. Jean-François Nguyen 2022-09-02 07:44:04 +0200
0a9329f431 insn.spec.muldiv: do not treat OE=1 forms as separate operations. Jean-François Nguyen 2022-09-02 07:40:36 +0200
0cbda65831 build.sby: remove unused import. Jean-François Nguyen 2022-08-24 13:06:23 +0200
319e65f43f test: check PowerFV specifications against OPV testcases. Jean-François Nguyen 2022-08-24 12:12:58 +0200
331e4b76ba insn: use records to define instruction encodings. Jean-François Nguyen 2022-08-24 11:04:10 +0200
cee4f7e569 session: save results and counter-examples to a local directory. Jean-François Nguyen 2022-08-08 17:59:07 +0200
9d81fbb9de session: fix subcommand help messages. Jean-François Nguyen 2022-08-08 17:16:39 +0200
846d4f8a4c session: add an implicit exit at the end of the command file. Jean-François Nguyen 2022-08-06 14:34:03 +0200
c743c932e7 compare: fix incorrect CR bit order. Jean-François Nguyen 2022-08-06 06:07:04 +0200
a9a17377b7 intr: use 0 for IR/DR bits, until LPCR is supported. Jean-François Nguyen 2022-08-06 06:03:41 +0200
619606eaf5 session: import readline to use it with the input() built-in. Jean-François Nguyen 2022-07-28 15:44:21 +0200
89be0e6737 Add support for remote builds over SSH. Jean-François Nguyen 2022-07-26 13:01:31 +0200
749184e964 Add instruction storage check. Jean-François Nguyen 2022-07-26 12:56:17 +0200
9fde9f9786 Add liveness check. Jean-François Nguyen 2022-07-25 15:26:24 +0200
23f503549f Add causal consistency check. Jean-François Nguyen 2022-07-25 15:19:24 +0200
a325393c42 Add checks for multiplication/division instructions. Jean-François Nguyen 2022-07-25 15:16:52 +0200
b3255def24 Add checks for CMPRB and CMPEQB instructions. Jean-François Nguyen 2022-07-25 15:11:22 +0200
d3546e4362 insn.spec: implement some interrupts (program,alignment,system call). Jean-François Nguyen 2022-07-25 15:08:33 +0200
2e29794b7d check.insn: use DUT parameters to configure the spec pfv.Interface. Jean-François Nguyen 2022-07-25 14:59:04 +0200
c16e678c49 Add a --exclude parameter to the check command. Jean-François Nguyen 2022-07-25 13:53:19 +0200
7b7aa6cc9b Add checks for CR Move / Set Boolean instructions. Jean-François Nguyen 2022-07-18 15:14:33 +0200
b579665d7a Add checks for Trap instructions. Jean-François Nguyen 2022-07-18 15:11:38 +0200
0038f3fff5 Add check for System Call instruction. Jean-François Nguyen 2022-07-18 15:09:52 +0200
ae76adefbf Add checks for Byte-Reverse instructions. Jean-François Nguyen 2022-07-18 15:07:42 +0200
4bf2398208 Add checks for BCD Assist instructions. Jean-François Nguyen 2022-07-18 15:05:54 +0200
23dcd80a9e Add checks for Rotate/Shift instructions. Jean-François Nguyen 2022-07-18 15:03:27 +0200
aeed09092c Add checks for logical instructions. Jean-François Nguyen 2022-07-18 14:58:48 +0200
373a4e28b6 pfv.Interface: add support for skipping instructions. Jean-François Nguyen 2022-07-18 14:46:55 +0200
bce3205759 insn.spec.branch: remove duplicate read of MSR.SF. Jean-François Nguyen 2022-07-18 14:43:09 +0200
57e29666ce cores/microwatt: fix CLI instructions. Jean-François Nguyen 2022-07-18 14:40:19 +0200
0f731db18a Add checks for Load/Store instructions. Jean-François Nguyen 2022-07-13 20:58:56 +0200
5ca0001b4b Add data storage check. Jean-François Nguyen 2022-07-13 20:48:58 +0200
5d21832c57 pfv.Interface: simplify memory port. Jean-François Nguyen 2022-07-13 20:36:12 +0200
fec1b838d5 check: add --cover argument to use SymbiYosys in coverage mode. Jean-François Nguyen 2022-07-13 20:33:36 +0200
ec7cfdd719 cores/microwatt: move microwatt.py to its own python module. Jean-François Nguyen 2022-07-13 20:23:34 +0200
a5e69954a4 Add checks for MTMSR/MFMSR instructions. Jean-François Nguyen 2022-07-07 12:48:27 +0200
dd6048f14b In-depth refactoring, improved user interface. Jean-François Nguyen 2022-07-07 12:25:00 +0200
05965592f9 checks.insn._addsub: fix incorrect ADDEX updates to OV/OV32. Jean-François Nguyen 2022-06-08 16:06:34 +0200
951ca2cdfb cores/microwatt: add checks for add/subtract instructions. Jean-François Nguyen 2022-06-07 19:13:48 +0200
f06c8000b0 checks.insn: add checks for add/subtract instructions. Jean-François Nguyen 2022-06-07 19:12:39 +0200
baaac86be1 cores/microwatt: add checks for MTSPR and MFSPR instructions. Jean-François Nguyen 2022-05-31 23:33:31 +0200
8cf56ab5dc checks.insn: add checks for MTSPR and MFSPR instructions. Jean-François Nguyen 2022-05-31 23:32:46 +0200
21be78c4f8 cores/microwatt: add checks for compare instructions. Jean-François Nguyen 2022-05-31 23:30:19 +0200
692e8ec7c4 checks.insn: add checks for compare instructions. Jean-François Nguyen 2022-05-31 23:29:15 +0200
a413025fcb Update SPR interface and split consistency check. Jean-François Nguyen 2022-05-31 22:48:59 +0200
e3f4bf6e24 cores/microwatt: add check for MCRF instruction. Jean-François Nguyen 2022-05-26 00:55:00 +0200
2ffff6196b checks.insn: add check for MCRF instruction. Jean-François Nguyen 2022-05-26 00:54:34 +0200
4c16035a70 checks.insn._cr: fix order of spec_cr_w_data bits. Jean-François Nguyen 2022-05-26 00:53:14 +0200
010c383ed7 tb: remove testbench start trigger. Jean-François Nguyen 2022-05-26 00:35:12 +0200
2c0b22b96c cores/microwatt: add checks for CR logical instructions. Jean-François Nguyen 2022-05-25 19:51:19 +0200
fee59d2257 checks.insn: add checks for CR logical instructions. Jean-François Nguyen 2022-05-25 19:49:06 +0200
bc06e67fe8 checks.insn._branch: add missing PowerFVCheck name. Jean-François Nguyen 2022-05-25 19:45:52 +0200
9ea58a47a9 Refactor to facilitate integration with CLIs and config files. Jean-François Nguyen 2022-05-24 16:26:27 +0200
5c097b9474 checks._branch: fix branches to LR/CTR/TAR. Jean-François Nguyen 2022-05-19 16:35:20 +0200
5649f60c78 checks.insn_bcctrl: fix typo. Jean-François Nguyen 2022-05-19 16:22:17 +0200
e9d7a91e01 utils: add helper to mask addresses according to MSR.SF. Jean-François Nguyen 2022-05-19 16:20:44 +0200
d9ed524cb3 powerv.insn: fix width of XO width for XL-form insns. Jean-François Nguyen 2022-05-19 16:19:17 +0200
0ca97a8d6a checks.{cr,gpr}: add support for interrupts. Jean-François Nguyen 2022-05-19 16:17:54 +0200
25500cd680 checks.spr: refactor. Jean-François Nguyen 2022-05-19 16:16:41 +0200
bc13b27212 cores/microwatt: expose MSR and SRR0/SRR1. Jean-François Nguyen 2022-05-19 16:16:14 +0200
c6a74333e8 pfv: add MSR and SRR0/SRR1 SPRs. Jean-François Nguyen 2022-05-19 16:14:37 +0200
58bef1a741 checks: add checks for branch instructions. Jean-François Nguyen 2022-05-16 18:04:51 +0200
5c9bc3e68c cores/microwatt: add support for concurrent execution of formal checks. Jean-François Nguyen 2022-05-16 17:56:48 +0200
6ae4978f0c pfv: expose CR as a flat 32-bit value. Jean-François Nguyen 2022-05-16 17:52:30 +0200
ed2122d940 cores/microwatt: add support for SPRCheck. Jean-François Nguyen 2022-05-11 00:13:33 +0200
2988ffc617 checks.spr: add SPRCheck. Jean-François Nguyen 2022-05-10 23:30:30 +0200
ca66e3a45e cores/microwatt: add support for CRCheck. Jean-François Nguyen 2022-05-10 19:52:25 +0200
e7e9bb08f0 checks.cr: add CRCheck. Jean-François Nguyen 2022-05-10 19:50:56 +0200
5076bdb9eb cores/microwatt: add support for GPRCheck. Jean-François Nguyen 2022-05-10 19:48:53 +0200
b84a23877a checks.gpr: add GPRCheck. Jean-François Nguyen 2022-05-10 19:46:36 +0200
6b5536eb0f tb: fix error message. Jean-François Nguyen 2022-05-05 20:51:10 +0200
6922b4bd53 cores/microwatt: add support for IAForwardCheck. Jean-François Nguyen 2022-05-05 20:43:26 +0200
e0e434204b checks.ia_fwd: add check. Jean-François Nguyen 2022-05-05 20:41:49 +0200
bfd1f3135e cores/microwatt: remove outdated patch. Jean-François Nguyen 2022-05-05 20:28:59 +0200
935110411f cores/microwatt: update demo. Jean-François Nguyen 2022-04-15 16:21:16 +0200
bc222162b8 build.plat: add SBY mode as .build() parameter. Jean-François Nguyen 2022-04-15 16:07:53 +0200
fc9feb58cb checks.unique: add check. Jean-François Nguyen 2022-04-15 16:05:11 +0200

Commit Graph Select branches Hide Pull Requests dinofly main Mono Color

Commit Graph

Select branches

Hide Pull Requests

dinofly

main