Fix minor typos

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.
 

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.
 

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

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`):