85 Commits (846d4f8a4cfaac40c271a8f9f3f1a4c770d37d3e)
 

Author SHA1 Message Date
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 bc13b27212 cores/microwatt: expose MSR and SRR0/SRR1. 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 ed2122d940 cores/microwatt: add support for SPRCheck. 3 years ago
Jean-François Nguyen 2988ffc617 checks.spr: add SPRCheck. 3 years ago
Jean-François Nguyen ca66e3a45e cores/microwatt: add support for CRCheck. 3 years ago
Jean-François Nguyen e7e9bb08f0 checks.cr: add CRCheck. 3 years ago
Jean-François Nguyen 5076bdb9eb cores/microwatt: add support for GPRCheck. 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 6922b4bd53 cores/microwatt: add support for IAForwardCheck.
Also, use non-default cache sizes for faster verification.
3 years ago
Jean-François Nguyen e0e434204b checks.ia_fwd: add check. 3 years ago
Jean-François Nguyen bfd1f3135e cores/microwatt: remove outdated patch.
The demo README provides an URL to a fork with experimental support for
PowerFV.
3 years ago
Jean-François Nguyen 935110411f cores/microwatt: update demo. 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 0cf05e305e cores/microwatt: update proof-of-concept. 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 776ec784ff Add very basic README. 3 years ago
Jean-François Nguyen 7051f8db60 Add license. 3 years ago
Jean-François Nguyen 1e93621f95 Use poetry to manage python dependencies. 3 years ago
Jean-François Nguyen cce0fa0729 Add Microwatt proof-of-concept. 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
Toshaan Bharvani 0c7dee878f initial push with a gitignore file
Signed-off-by: Toshaan Bharvani <toshaan@vantosh.com>
3 years ago