diff options
Diffstat (limited to 'machxo2/examples/README.md')
| -rw-r--r-- | machxo2/examples/README.md | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/machxo2/examples/README.md b/machxo2/examples/README.md index aac80fb4..e940c01c 100644 --- a/machxo2/examples/README.md +++ b/machxo2/examples/README.md @@ -16,7 +16,8 @@ This contains a simple example of running `nextpnr-machxo2`: ports._ All possible inputs and resulting outputs can be tested in reasonable time by - using yosys' built-in SAT solver. + using `yosys`' built-in SAT solver or [`z3`](https://github.com/Z3Prover/z3), + an external SMT solver. As `nextpnr-machxo2` is developed the contents `simple.sh`, `simtest.sh`, and `mitertest.sh` are subject to change. @@ -29,9 +30,15 @@ ways. The `mode` argument to each script- `pack`, `place`, or `pnr`- stop results in `{pack,place,pnr}blinky.json`; `pnr` runs all of the Pack, Place, and Route phases. +`mitertest.sh` requires an additional option- `sat` or `smt`- to choose between +verifying the miter with either yosys' built-in SAT solver, or an external +SMT solver. + To keep file count lower, all yosys scripts are written inline inside the `sh` scripts using the `-p` option. +To clean output files, run: `rm -rf *.dot *.json *.png *.vcd *.smt2 *.log {pack,place,pnr}*.v blinky_simtest*` + ## Environment Variables For Scripts * `YOSYS`- Set to the location of the `yosys` binary to test. Defaults to the |