Jean-François Nguyen
c90e8fc496
check.storage: allow interrupts during instruction fetches.
2 years ago
Jean-François Nguyen
a3dd57ac46
cores/dinofly: add insn and data storage checks.
2 years ago
Jean-François Nguyen
96878c73da
Add checks for 64-bit Rotate/Shift instructions.
2 years ago
Jean-François Nguyen
eb314fcbf0
check.insn: ignore upper SPR 32-bits when pfv.gpr_width=32.
2 years ago
Jean-François Nguyen
dfcfa3a68b
insn: fix TAR SPR number.
2 years ago
Jean-François Nguyen
be7fdd7aa6
cores/dinofly: update checks.pfv.
2 years ago
Jean-François Nguyen
85a061474e
pfv: add configurable memory alignment constraints.
...
Before this commit, the `mem_aligned` parameter assumed a 64-bit data
bus when set to True.
2 years ago
Jean-François Nguyen
f091fd1977
cores/dinofly: update checks.pfv.
2 years ago
Jean-François Nguyen
139eb488cf
cores/dinofly: drive dbus inputs.
2 years ago
Jean-François Nguyen
0d82a3d13a
insn.spec.compare: ignore upper 32-bits when pfv.gpr_width=32.
2 years ago
Jean-François Nguyen
d611d8c5e1
cores/dinofly: add initial support.
2 years ago
Jean-François Nguyen
28becc090c
pfv: add gpr_width parameter to explore designs with 32-bit GPRs.
2 years ago
Jean-François Nguyen
fa14ed223e
session: fix the testbench name used by build products.
2 years ago
Jean-François Nguyen
84bad74a04
core: remove src_dir from PowerFVCore.add_files().
...
It is implementation-specific, and should instead be defined by derived
classes if needed.
2 years ago
Jean-François Nguyen
a2876b6a95
cores/microwatt: temporarily disable the liveness check.
2 years ago
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).
2 years ago
Jean-François Nguyen
713428146a
README: fix styling, update microwatt URL.
2 years ago
Jean-François Nguyen
5e9006bba9
Update README.
2 years ago
Jean-François Nguyen
cec7240135
core: add PowerFVCore docstrings.
2 years ago
Jean-François Nguyen
e41632d192
pfv: add Interface docstrings.
2 years ago
Jean-François Nguyen
0a9329f431
insn.spec.muldiv: do not treat OE=1 forms as separate operations.
2 years ago
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
