fix images on docs site

README.md

@@ -1,7 +1,8 @@
 ![](doc/assets/manta.png)
 
 ## Manta: An In-Situ Debugging Tool for Programmable Hardware
-![functional_sim](https://github.com/fischermoseley/manta/actions/workflows/functional_sim.yml/badge.svg)
+![functional_simulation](https://github.com/fischermoseley/manta/actions/workflows/functional_simulation.yml/badge.svg)
+![formal_verification](https://github.com/fischermoseley/manta/actions/workflows/formal_verification.yml/badge.svg)
 ![build_examples](https://github.com/fischermoseley/manta/actions/workflows/build_examples.yml/badge.svg)
 ![build_docs](https://github.com/fischermoseley/manta/actions/workflows/build_docs.yml/badge.svg)
 [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)

doc/block_memory.md

@@ -68,7 +68,7 @@ A Block Memory core is used in the [video_sprite](https://github.com/fischermose
 
 Each Block Memory core is actually a set of 16-bit wide BRAMs with their ports concatenated together, with any spare bits masked off. Here's a diagram:
 
-<img src="/assets/block_memory_architecture.png" alt="drawing" width="800"/>
+![](assets/block_memory_architecture.png)
 
 This has one major consequence: if the core doesn't have a width that's an exact multiple of 16, synthesis engines (Vivado in particular) will throw some warnings as they optimize out the unused bits. This is expected behavior, and while the warnings are a little annoying, not having to manually deal with the unused bits simplifies the implementation immensely. No Python is needed to generate the core, and it'll configure itself just based on Verilog parameters. This turns the block memory core from a complicated conditionally-instantiated beast to a simple ~_100 line_ [Verilog file](https://github.com/fischermoseley/manta/blob/main/src/manta/block_memory.v).
 

doc/examples.md

@@ -1,15 +0,0 @@
-Examples can be found under `examples/` in the GitHub repository. These target the following boards:
-
-### Nexys A7/Nexys4 DDR:
-
-- [io_core_ether](https://github.com/fischermoseley/manta/tree/main/examples/nexys_a7/io_core_ether) and [io_core_uart](https://github.com/fischermoseley/manta/tree/main/examples/nexys_a7/io_core_uart)
-    - These both demonstrate the IO core, connected to a host machine over either UART or Ethernet. This includes a Manta configuration that's synthesized onto the FPGA, and a script run on the host. This script uses Manta's Python API to draw a pattern on the Nexys A7's built-in LED display, and also report the status of the onboard buttons and switches to the user.
-
-- [ps2_logic_analyzer](https://github.com/fischermoseley/manta/tree/main/examples/nexys_a7/ps2_logic_analyzer)
-    -
-
-- [video_sprite_ether] and [video_sprite_uart]
-
-### Icestick
-
-- [io_core](https://github.com/fischermoseley/manta/tree/main/examples/icestick/io_core)

doc/how_it_works.md

@@ -3,7 +3,7 @@
 
 To use Manta, you'll need a host machine with a FPGA development board connected to it over UART or Ethernet. The whole system looks like the following:
 
-<img src="/assets/manta_architecture.png" alt="drawing" width="400"/>
+![](assets/manta_architecture.png){:style="width:80%"}
 
 Manta is operated via its Python API, which communicates with the connected FPGA over an interface API like `pySerial` or `Scapy`. These abstract away the OS device drivers, which function differently depending on the host machine's platform. The OS device drivers ultimately send out bytes to the FPGA, across either a USB or Ethernet cable.
 
@@ -57,9 +57,9 @@ uart:
 This will create a Manta instance with an IO Core and a Logic Analyzer, each containing a number of probes at variable widths. The Manta module itself is provided a 100MHz clock, and communicates with the host over UART running at 3Mbaud.
 
 ## System Architecture
-The logic Manta places on the FPGA consists of a series of cores connected in a chain along a common bus. Each core provides a unique method for interacting with the user’s logic, which it connects to by routing signals, called `probes`, between the user’s logic and the cores that interface with it.
+The logic Manta places on the FPGA consists of a series of cores connected in a chain along a common bus. Each core provides a unique method for interacting with the user’s logic, which it connects to by routing signals (called _probes_) between the user’s logic and the cores that interface with it.
 
-<img src="/assets/bus_architecture.png" alt="drawing" width="400"/>
+![](assets/bus_architecture.png){:style="width:40%"}
 
 These probes are presented as addressable memory, and are be controlled by reading and writing to their corresponing memory - not unlike registers on a microcontroller. Each core is allotted a section of address space at compile time, and operations addressed to a core’s address space control the behavior of the core. These cores are then daisy-chained along an internal bus, which permits a chain arbitrarily many cores to be placed on the bus.
 
@@ -77,16 +77,14 @@ The data bus is designed for simplicity, and consists of five signals used to pe
 
 Each core has a bus input and output port, so that cores can be daisy-chained together. When it receives an incoming bus transaction (signalled by `valid`), the core checks the address on the wire against its own memory space. If the address lies within the core, the core will perform the requested operation against its own memory space. In the case of a read, it places the data at that address on `data`, and in the case of a write, it copies the value of `data` to the specified location in memory. However, if the address lies outside of the memory of the core, then no operations are performed.
 
-<img src="/assets/read_transaction.png" width="350"/>
-<img src="/assets/write_transaction.png" width="350"/>
+![](assets/read_transaction.png){:style="width:49%"}
+![](assets/write_transaction.png){:style="width:49%"}
 
 ## Message Format
 
 Ethernet and UART both allow a stream of bytes to be sent between the host and FPGA, but since they're just interfaces, they don't define how these bytes are structured. As a result, Manta implements its own messaging format, with the following structure:
 
-
-<img src="/assets/uart.png" alt="drawing" width="600"/>
-
+![](assets/uart.png){:style="width:85%"}
 
 Each of these messages is a string of ASCII characters consisting of a preamble, optional address and data fields, and an End of Line (EOL). The preamble denotes the type of operation, _R_ for a read and _W_ for a write. The address and data fields are encoded as hexadecimal digits, represented with the characters 0-9 and A-F in ASCII. As a result, four characters are needed to encode a 16-bit address or 16-bits of data. If the message specifies a write request, then it will contain a data field after the address field. Both request types will conclude with an End of Line, which consists of the two ASCII characters indicating a Carriage Return (CR) and a Line Feed (LF).
 

doc/io_core.md

@@ -97,7 +97,7 @@ While the IO core performs a very, very simple task, it carries a few caveats.
 
 This is done with the architecture shown below:
 
-<img src="/assets/io_core_block_diagram.png" alt="drawing" width="400"/>
+![](assets/io_core_block_diagram.png){:style="width:49%"}
 
 Each of the probes is mapped to a register of Manta's internal memory. Since Manta's internal registers are 16 bits wide, probes less than 16 bits are mapped to a single register, but probes wider than 16 bits require multiple.
 

doc/logic_analyzer.md

@@ -69,7 +69,7 @@ Lastly, if you're not able to express your desired trigger condition in terms of
 ### Trigger Position (optional)
 Sometimes, you care more about what happens before a trigger is met than afterwards, or vice versa. To accomodate this, the logic analyzer has an optional _Trigger Position_ parameter, which sets when probe data is captured relative to the trigger condition being met. This is specified with the `trigger_position` entry in the configuration file, which sets how many samples to save prior to the trigger condition occuring. This is best explained with a picture:
 
-<img src="/assets/trigger_positions.png" alt="drawing" width="800"/>
+![](assets/trigger_positions.png){style="width:90%"}
 
 The windows at the bottom of the diagram show what portions of the timeseries will be captured for different trigger positions. For instance:
 
@@ -134,12 +134,12 @@ This is useful for two situations in particular:
 ## Python API
 The Logic Analyzer core functionality is stored in the `Manta.LogicAnalyzerCore` class in [src/manta/la_core/\_\_init\_\_.py](https://github.com/fischermoseley/manta/blob/main/src/manta/la_core/__init__.py).
 
-At present, this class contains methods used really only for capturing data, and exporting `.vcd` and `.mem` files. It'd be super handy to expose the data from the logic analyzer core in a Pythonic way - which is why the feature is on the [roadmap](roadmap.md)!
+At present, this class contains methods used really only for capturing data, and exporting `.vcd` and `.mem` files. It'd be super handy to expose the data from the logic analyzer core in a Pythonic way - which is why the feature is on the [roadmap](https://github.com/fischermoseley/manta/milestones)!
 
 ## How It Works
 The Logic Analyzer Core's implementation on the FPGA consists of three primary components:
 
-<img src="/assets/manta_logic_analyzer_architecture.png" alt="drawing" width="800"/>
+![](assets/manta_logic_analyzer_architecture.png){style="width:85%"}
 
 - The _Finite State Machine (FSM)_, which controls the operation of the core. The FSM's operation is driven by its associated registers, which are placed in a separate module. This permits simple CDC between the bus and user clock domains.
 - The _Trigger Block_, which generates the core's trigger condition. The trigger block contains a trigger for each input probe, and the registers necessary to configure them. It also contains the $N$-logic gate (either AND or OR) that generates the core's trigger from the individual probe triggers. CDC is performed in exactly the same manner as the FSM. If an external trigger is specified, the trigger block is omitted from the Logic Analyzer Core, and the external trigger is routed to the FSM's `trig` input.

mkdocs.yml

@@ -52,6 +52,7 @@ markdown_extensions:
   - pymdownx.details
   - pymdownx.superfences
   - pymdownx.tilde
+  - attr_list
 
 nav:
     - Home: index.md