From aa731e3ded35a7960cae3fa2ef5d53c4e2a16561 Mon Sep 17 00:00:00 2001 From: Tom Verbeure Date: Tue, 7 Aug 2018 22:22:27 -0700 Subject: [PATCH] Fix minor typos --- docs/config.md | 8 ++++---- docs/examplebugs.md | 2 +- docs/procedure.md | 4 ++-- docs/quickstart.md | 10 +++++----- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/docs/config.md b/docs/config.md index 7460550..5f09637 100644 --- a/docs/config.md +++ b/docs/config.md @@ -47,7 +47,7 @@ fused instructions this is the maximum length of a complete fused instruction. RISCV_FORMAL_COMPRESSED ----------------------- -For cores supporting the RISC-V Compressed ISA is define must be set. +For cores supporting the RISC-V Compressed ISA this define must be set. RISCV_FORMAL_ALIGNED_MEM ------------------------ @@ -75,8 +75,8 @@ RISCV_FORMAL_FAIRNESS --------------------- When checking for liveness of the core, then the peripherals and abstractions -used in the check must guranatee fairness. This macro should be tested by the -peripherals and abstractions to decide if fairness guranatees should be enabled. +used in the check must guarantee fairness. This macro should be tested by the +peripherals and abstractions to decide if fairness guarantees should be enabled. RISCV_FORMAL_VALIDADDR(addr) ---------------------------- @@ -100,7 +100,7 @@ The Verilog file `rvfi_macros.vh` defines a few useful helper macros. RVFI_WIRES, RVFI_OUTPUTS, RVFI_INPUTS, RVFI_CONN ------------------------------------------------ -Macros to declare wires, ouptut ports, or input ports for all `rvfi_*` signals. The last +Macros to declare wires, output ports, or input ports for all `rvfi_*` signals. The last macro is for creating the proper connections on module instances. This macros can be useful for routing the `rvfi_*` signals through the design hierarchy. diff --git a/docs/examplebugs.md b/docs/examplebugs.md index 0bdc1e5..be7583e 100644 --- a/docs/examplebugs.md +++ b/docs/examplebugs.md @@ -4,7 +4,7 @@ Examples of bugs found by riscv-formal This page lists a few examples of common types of bugs found by riscv-formal. -This page is intentionally a bit vague on the details. It's purpose is to give +This page is intentionally a bit vague on the details. Its purpose is to give readers an idea of what kind of bugs can be found with riscv-formal, not to pillory implementations for long fixed bugs. diff --git a/docs/procedure.md b/docs/procedure.md index 521a190..6cf05dc 100644 --- a/docs/procedure.md +++ b/docs/procedure.md @@ -28,13 +28,13 @@ The `pc_fwd` check assumes that the core retires an instruction at the end of th ### Register Checks -This checks if writes to and reads from the register file are consisten with each other, i.e. if the value written to a register matches the value read from the register file by a later instructions. +This checks if writes to and reads from the register file are consistent with each other, i.e. if the value written to a register matches the value read from the register file by a later instructions. This check assumes that the last instruction at the end of the bounded model check, reads a register. It then checks that the value read is consistent with the matching write to the same register by an earlier instruction. ### Causality -The core may retire instructions out-of-order as long as causality is preserved. (This means a regisert write must be retired before the register reads that depend on it.) This check tests if the +The core may retire instructions out-of-order as long as causality is preserved. (This means a register write must be retired before the register reads that depend on it.) This check tests if the instruction stream is causal with respect to registers. ### Liveness diff --git a/docs/quickstart.md b/docs/quickstart.md index e8f2376..2593afb 100644 --- a/docs/quickstart.md +++ b/docs/quickstart.md @@ -22,7 +22,7 @@ If you want to inspect counter example traces you will need [gtkwave](http://gtkwave.sourceforge.net/). Whatever version of gtkwave is pre-packaged in your distribution is probably fine. -If you want to disasample the code executed in the counter example traces you +If you want to disassemble the code executed in the counter example traces you will need an installation of 32 bit [riscv-tools](https://github.com/riscv/riscv-tools), specifically you'll need `riscv32-unknown-elf-gcc` and `riscv32-unknown-elf-objdump` in your `$PATH`. @@ -49,7 +49,7 @@ python3 ../../checks/genchecks.py make -C checks -j$(nproc) ``` -This will run in the order of four CPU hours (AMD Bulldozer at 3.6 GHz). It +This will run on the order of four CPU hours (AMD Bulldozer at 3.6 GHz). It is over 60 individual checks than can all run in parallel if the machine has sufficient memory and cores. So if you run it on a large server you can completely verify the core in just a few minutes. @@ -80,14 +80,14 @@ Or you can simply use gtkwave to display the counter example trace: gtkwave checks/liveness_ch0/engine_0/trace.vcd checks.gtkw ``` -Exercise 2: Build a RVFI Monitor and run it +Exercise 2: Build an RVFI Monitor and run it ------------------------------------------- -A RVFI Monitor can be run side-by-side with your core and will detect when the +An RVFI Monitor can be run side-by-side with your core and will detect when the core violates the ISA spec. RVFI monitors are synthesizable, so in addition to simulation they can also be used in FPGA emulation testing. -Let's built a RVFI Monitor to be used with PicoRV32. PicoRV32 supports the +Let's build an RVFI Monitor to be used with PicoRV32. PicoRV32 supports the rv32ic ISA (`-i rv32ic`), its RVFI port is one channel wide (`-c 1`), and it performs memory operations with word alignment (`-a`):