power-fv/cores/microwatt/README.md

## Additional prerequisites

- [ghdl](https://github.com/ghdl/ghdl) with the LLVM or GCC backend
- [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin)


Get Microwatt:

```
git clone git@git.openpower.foundation:jfng/microwatt -b powerfv src
```

## Usage

### Enter/exit the Python virtualenv

```
poetry shell

python microwatt.py -h

exit
```

### Run commands from a file

```
python microwatt.py -c checks.pfv
```

### Run commands interactively

```
python microwatt.py -i
```
Add very basic README. 2 years ago			`## Additional prerequisites`

			`- [ghdl](https://github.com/ghdl/ghdl) with the LLVM or GCC backend`
			`- [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin)`

Add Microwatt proof-of-concept. 2 years ago
cores/microwatt: update demo. 2 years ago			`Get Microwatt:`

cores/microwatt: update proof-of-concept. 2 years ago			```
cores/microwatt: move microwatt.py to its own python module. Also: * update dependencies. * add amaranth-soc as a dependency, in order to reuse its bus interfaces (e.g. Wishbone). * add a `prog` argument to PowerFVSession that overrides the name of its CLI. 2 years ago			`git clone git@git.openpower.foundation:jfng/microwatt -b powerfv src`
cores/microwatt: update proof-of-concept. 2 years ago			```

			`## Usage`

cores/microwatt: add support for concurrent execution of formal checks. 2 years ago			`### Enter/exit the Python virtualenv`

cores/microwatt: update proof-of-concept. 2 years ago			```
cores/microwatt: update demo. 2 years ago			`poetry shell`
cores/microwatt: update proof-of-concept. 2 years ago
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates). 2 years ago			`python microwatt.py -h`
cores/microwatt: update proof-of-concept. 2 years ago
			`exit`
			```

In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates). 2 years ago			`### Run commands from a file`
cores/microwatt: update proof-of-concept. 2 years ago
cores/microwatt: update demo. 2 years ago			```
In-depth refactoring, improved user interface. * A PowerFVSession class provides a REPL interface. Functionality is split into commands (e.g. add checks, build) which can be provided interactively or from a file. See cores/microwatt for an example of its integration. * Instruction specifications are now separated from verification testbenches. An InsnSpec class provides a behavioral model using the same PowerFV interface as a core. This interface is output-only for a core, but bidirectional for the InsnSpec: - fields related to context (e.g. read data) are inputs, - fields related to side-effects (e.g. write strobes) are outputs. The testbench is responsible for driving inputs to the same values as the core, then check outputs for equivalence. This decoupling provides a path towards using PowerFV in simulation. * Instruction encodings are now defined by their fields, not their format (which was problematic e.g. X-form has dozens of variants). Field declarations can be preset to a value, or left undefined. In the latter case, they are implicitly cast to AnyConst (which is useful for arbitrary values like immediates). 2 years ago			`python microwatt.py -c checks.pfv`
			```

			`### Run commands interactively`

			```
			`python microwatt.py -i`
Add Microwatt proof-of-concept. 2 years ago			```