Skip to content

Commit

Permalink
Merge pull request #203 from dlmiles/dlm-202312
Browse files Browse the repository at this point in the history
Tranche 4
  • Loading branch information
Dolu1990 authored Aug 27, 2023
2 parents b2d9e21 + 959b771 commit 66671bf
Show file tree
Hide file tree
Showing 26 changed files with 196 additions and 166 deletions.
3 changes: 0 additions & 3 deletions source/SpinalHDL/Examples/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,6 @@ Examples

.. _example_introduction:

Introduction
============

Examples are split into three kinds:

* Simple examples that could be used to get used to the basics of SpinalHDL.
Expand Down
34 changes: 17 additions & 17 deletions source/SpinalHDL/Formal verification/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ Installing requirements
To install the Symbi-Yosys, you have a few options. You can fetch a precompiled package at:

- https://github.com/YosysHQ/oss-cad-suite-build/releases
- https://github.com/YosysHQ/fpga-toolchain/releases
- https://github.com/YosysHQ/fpga-toolchain/releases (EOL - superseded by oss-cad-suite)

Or you can compile things from scratch :

Expand All @@ -59,10 +59,10 @@ Here is an example of a simple counter and the corresponding formal testbench.
import spinal.core._
//Here is our DUT
class LimitedCounter extends Component{
class LimitedCounter extends Component {
//The value register will always be between [2:10]
val value = Reg(UInt(4 bits)) init(2)
when(value < 10){
when(value < 10) {
value := value + 1
}
}
Expand Down Expand Up @@ -94,9 +94,9 @@ If you want you can embed formal statements directly into the DUT:

.. code-block:: scala
class LimitedCounterEmbedded extends Component{
class LimitedCounterEmbedded extends Component {
val value = Reg(UInt(4 bits)) init(2)
when(value < 10){
when(value < 10) {
value := value + 1
}
Expand Down Expand Up @@ -124,11 +124,11 @@ but you can also use the formal `anyseq`, `anyconst`, `allseq`, `allconst` state

.. code-block:: scala
class LimitedCounterInc extends Component{
class LimitedCounterInc extends Component {
//Only increment the value when the inc input is set
val inc = in Bool()
val value = Reg(UInt(4 bits)) init(2)
when(inc && value < 10){
when(inc && value < 10) {
value := value + 1
}
}
Expand Down Expand Up @@ -160,7 +160,7 @@ For instance we can check that the value is counting up (if not already at 10):
// Check that the value is incrementing.
// hasPast is used to ensure that the past(dut.value) had at least one sampling out of reset
when(pastValid() && past(dut.value) =/= 10){
when(pastValid() && past(dut.value) =/= 10) {
assert(dut.value === past(dut.value) + 1)
}
})
Expand All @@ -172,7 +172,7 @@ Here is an example where we want to prevent the value ``1`` from ever being pres

.. code-block:: scala
class DutWithRam extends Component{
class DutWithRam extends Component {
val ram = Mem.fill(4)(UInt(8 bits))
val write = slave(ram.writePort)
val read = slave(ram.readAsyncPort)
Expand All @@ -186,13 +186,13 @@ Here is an example where we want to prevent the value ``1`` from ever being pres
assumeInitial(ClockDomain.current.isResetActive)
// assume that no word in the ram has the value 1
for(i <- 0 until dut.ram.wordCount){
for(i <- 0 until dut.ram.wordCount) {
assumeInitial(dut.ram(i) =/= 1)
}
// Allow the write anything but value 1 in the ram
anyseq(dut.write)
clockDomain.withoutReset(){ //As the memory write can occur during reset, we need to ensure the assume apply there too
clockDomain.withoutReset() { //As the memory write can occur during reset, we need to ensure the assume apply there too
assume(dut.write.data =/= 1)
}
Expand All @@ -215,7 +215,7 @@ If you want to keep your assertion enabled during reset you can do:

.. code-block:: scala
ClockDomain.current.withoutReset(){
ClockDomain.current.withoutReset() {
assert(wuff === 0)
}
Expand Down Expand Up @@ -244,7 +244,7 @@ If you have a Mem in your design, and you want to check its content, you can do
.. code-block:: scala
// Manual access
for(i <- 0 until dut.ram.wordCount){
for(i <- 0 until dut.ram.wordCount) {
assumeInitial(dut.ram(i) =/= X) //No occurence of the word X
}
Expand Down Expand Up @@ -294,10 +294,10 @@ Formal primitives
- Return True when ``that`` transitioned from True to False
* - ``changed(that : Bool)``
- Bool
- Return True when ``that`` current value changed between comparred to the last cycle
- Return True when ``that`` current value changed between compared to the last cycle
* - ``stable(that : Bool)``
- Bool
- Return True when ``that`` current value didn't changed between comparred to the last cycle
- Return True when ``that`` current value didn't changed between compared to the last cycle
* - ``initstate()``
- Bool
- Return True the first cycle
Expand All @@ -306,13 +306,13 @@ Formal primitives
- Returns True when the past value is valid (False on the first cycle). Recommended to be used with each application of ``past``, ``rose``, ``fell``, ``changed`` and ``stable``.
* - ``pastValidAfterReset()``
- Bool
- Simliar to ``pastValid``, where only difference is that this would take reset into account. Can be understand as ``pastValid & past(!reset)``.
- Simliar to ``pastValid``, where only difference is that this would take reset into account. Can be understood as ``pastValid & past(!reset)``.

Note that you can use the init statement on past:

.. code-block:: scala
when(past(enable) init(False)){ ... }
when(past(enable) init(False)) { ... }
Expand Down
77 changes: 40 additions & 37 deletions source/SpinalHDL/Libraries/Com/usb_device.rst
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@

USB device
============
==========

There is a USB device controller in the SpinalHDL library. In a few bullet points it can be resumed to :
Here exists a USB device controller in the SpinalHDL library.

A few bullet points to summarise support:

- Implemented to allow a CPU to configure and manage the endpoints
- A internal ram which store the endpoints states and transactions descriptors
Expand All @@ -27,23 +29,23 @@ Deployments :


Architecture
--------------
------------

The controller is composed of :

- A few control registers
- A internal ram used to store the endpoint status, the transfer descriptors and the endpoint 0 SETUP data.

A linked list of descriptors for each endpoint in order to handle of the USB IN/OUT transactions and data.
A linked list of descriptors for each endpoint in order to handle the USB IN/OUT transactions and data.

The endpoint 0 manage the IN/OUT transactions like all the other endpoints but has some additional hardware to manage the SETUP transactions :

- Its linked list is cleared on each setup transactions
- The data of the SETUP transaction are stored in a fixed location (SETUP_DATA)
- The data from the SETUP transaction is stored in a fixed location (SETUP_DATA)
- It has a specific interrupt flag for SETUP transactions

Registers
--------------
---------

Note that all registers and memories of the controller are only accessible in 32 bits word access, bytes access isn't supported.

Expand Down Expand Up @@ -79,36 +81,37 @@ finalise the SET_ADDRESS sequance. The controller will then automaticaly turn on
INTERRUPT (0xFF08)
**********************

All bits of this register can be cleared by writing '1' in them.

+--------------+------+-----------+------------------------------------------------------------------+
| Name | Type | Bits | Description |
+==============+======+===========+==================================================================+
| endpoints | RC | 15-0 | Raised when a enpoint generate a interrupt |
+--------------+------+-----------+------------------------------------------------------------------+
| reset | RC | 16 | Raised when a USB reset appeared |
+--------------+------+-----------+------------------------------------------------------------------+
| ep0Setup | RC | 17 | Raised when endpoint 0 receive a setup transaction |
+--------------+------+-----------+------------------------------------------------------------------+
| suspend | RC | 18 | Raised when a USB suspend appeared |
+--------------+------+-----------+------------------------------------------------------------------+
| resume | RC | 19 | Raised when a USB resume appeared |
+--------------+------+-----------+------------------------------------------------------------------+
| disconnect | RC | 20 | Raised when a USB disconnect appeared |
+--------------+------+-----------+------------------------------------------------------------------+
Individual bits of this register can be cleared by writing '1' in them.
Reading this register returns the current interrupt status.

+--------------+-------+-----------+------------------------------------------------------------------+
| Name | Type | Bits | Description |
+==============+=======+===========+==================================================================+
| endpoints | W1C | 15-0 | Raised when an endpoint generates an interrupt |
+--------------+-------+-----------+------------------------------------------------------------------+
| reset | W1C | 16 | Raised when a USB reset occurs |
+--------------+-------+-----------+------------------------------------------------------------------+
| ep0Setup | W1C | 17 | Raised when endpoint 0 receives a setup transaction |
+--------------+-------+-----------+------------------------------------------------------------------+
| suspend | W1C | 18 | Raised when a USB suspend occurs |
+--------------+-------+-----------+------------------------------------------------------------------+
| resume | W1C | 19 | Raised when a USB resume occurs |
+--------------+-------+-----------+------------------------------------------------------------------+
| disconnect | W1C | 20 | Raised when a USB disconnect occurs |
+--------------+-------+-----------+------------------------------------------------------------------+

HALT (0xFF0C)
**********************

This register allow to place a single enpoint in a dormant state in order to ensure atomicity of CPU operations, allowing to do things as read/modify/write on the endpoint registers and descriptors.
The peripheral will return NAK if the given endpoint is addressed by the usb host.
This register allows placement of a single endpoint into a dormant state in order to ensure atomicity of CPU operations, allowing to do things as read/modify/write on the endpoint registers and descriptors.
The peripheral will return NAK if the given endpoint is addressed by the usb host while halt is enabled and the endpoint is enabled.

+-------------------------+------+-----------+------------------------------------------------------------------+
| Name | Type | Bits | Description |
+=========================+======+===========+==================================================================+
| endpointId | WO | 3-0 | The endpoint you want to put in sleep |
+-------------------------+------+-----------+------------------------------------------------------------------+
| enable | WO | 4 | |
| enable | WO | 4 | When set halt is active, when clear endpoint is unhalted. |
+-------------------------+------+-----------+------------------------------------------------------------------+
| effective | RO | 5 | After setting the enable, you need to wait for this bit to be |
| enable | | | set by the hardware itself to ensure atomicity |
Expand Down Expand Up @@ -168,20 +171,20 @@ To get a endpoint responsive you need :
- Set its enable flag to 1

Then the there is a few cases :
- Either you have the stall or nack flag set, and so, the controller will always responde with the corresponding responses
- Either you have the stall or nack flag set, and so, the controller will always respond with the corresponding responses
- Either, for EP0 setup request, the controller will not use descriptors, but will instead write the data into the SETUP_DATA register, and ACK
- Either you have a empty linked list (head==0) in which case it will answer NACK
- Either you have at least one descriptor pointed by head, in which case it will execute it and ACK if all was going smooth

SETUP_DATA (0x0040 - 0x0047)
*********************************

When endpoint 0 receive a SETUP transaction, the data of the transaction will be stored at that place.
When endpoint 0 receives a SETUP transaction, the data of the transaction will be stored in this location.

Descriptors
----------------------------
-----------

Descriptors allows to specify how a endpoint need to handle the data phase of IN/OUT transactions.
Descriptors allows to specify how an endpoint needs to handle the data phase of IN/OUT transactions.
They are stored in the internal ram, can be linked together via their linked lists and need to be aligned on 16 bytes boundaries

+-------------------+------+-----------+------------------------------------------------------------------+
Expand All @@ -191,33 +194,33 @@ They are stored in the internal ram, can be linked together via their linked lis
+-------------------+------+-----------+------------------------------------------------------------------+
| code | 0 | 19-16 | 0xF => in progress, 0x0 => success |
+-------------------+------+-----------+------------------------------------------------------------------+
| next | 1 | 15-4 | Point the the next descriptor |
| next | 1 | 15-4 | Pointer to the next descriptor |
| | | | 0 => nothing, byte address = this << 4 |
+-------------------+------+-----------+------------------------------------------------------------------+
| length | 1 | 31-16 | Number of bytes allocated for the data field |
+-------------------+------+-----------+------------------------------------------------------------------+
| direction | 2 | 16 | '0' => OUT, '1' => IN |
+-------------------+------+-----------+------------------------------------------------------------------+
| interrupt | 2 | 17 | If set, the completion of the descriptor will generate a |
| interrupt | 2 | 17 | If set, the completion of the descriptor will generate an |
| | | | interrupt. |
+-------------------+------+-----------+------------------------------------------------------------------+
| completionOnFull | 2 | 18 | Normaly, a descriptor completion only occure when a USB transfer |
| completionOnFull | 2 | 18 | Normally, a descriptor completion only occurs when a USB transfer|
| | | | is smaller than the maxPacketSize. But if this field is set, |
| | | | then when the descriptor become full is also a considered |
| | | | as a completion event. (offset == length) |
+-------------------+------+-----------+------------------------------------------------------------------+
| data1OnCompletion | 2 | 19 | force the endpoint dataPhase to DATA1 on the completion of the |
| | | | descriptoo |
| | | | descriptor |
+-------------------+------+-----------+------------------------------------------------------------------+
| data | ... | ... | |
+-------------------+------+-----------+------------------------------------------------------------------+

Note, if the controller receive a frame where the IN/OUT does not match the descriptor IN/OUT, the frame will be ignored.
Note, if the controller receives a frame where the IN/OUT does not match the descriptor IN/OUT, the frame will be ignored.

Also, to initialise a descriptor, the CPU should set the code field to 0xF
Also, to initialise a descriptor, the CPU should set the code field to 0xF

Usage
--------------
-----

.. code-block:: scala
Expand Down
16 changes: 9 additions & 7 deletions source/SpinalHDL/Libraries/Com/usb_ohci.rst
Original file line number Diff line number Diff line change
@@ -1,17 +1,19 @@

USB OHCI
============
========

There is a USB OHCi controller (host) in the SpinalHDL library. In a few bullet points it can be resumed to :
Here exists a USB OHCi controller (host) in the SpinalHDL library.

A few bullet points to summarise support:

- It follow the `OpenHCI Open Host Controller Interface Specification for USB` specification (OHCI).
- It is compatible with the upstream linux / uboot OHCI drivers already. (there is also a OHCI driver on tinyUSB)
- This provide USB host full speed and low speed capabilities (12Mbps and 1.5Mbps)
- It is compatible with the upstream linux / uboot OHCI drivers already. (there is also an OHCI driver on tinyUSB)
- This provides USB host full speed and low speed capabilities (12Mbps and 1.5Mbps)
- Tested on linux and uboot
- One controller can host multiple ports (up to 16)
- Bmb memory interface for DMA accesses
- Bmb memory interace for the configuration
- Require a clock for the internal phy which is a multiple of 12 Mhz at least 48 Mhz
- Requires a clock for the internal phy which is a multiple of 12 Mhz at least 48 Mhz
- The controller frequency is not restricted
- No external phy required

Expand All @@ -26,7 +28,7 @@ Limitations :

- Some USB hub (had one so far) do not like having a full speed host with low speed devices attached.
- Some modern devices will not work on USB full speed (ex : Gbps ethernet adapter)
- Require memory coherency with the CPU (or the cpu need to flush his data cache in the driver)
- Require memory coherency with the CPU (or the cpu need to be able to flush its data cache in the driver)

Deployments :

Expand Down Expand Up @@ -71,7 +73,7 @@ Usage
val management = phy.io.management.toIo
}
object UsbHostGen extends App{
object UsbHostGen extends App {
val p = UsbOhciParameter(
noPowerSwitching = true,
powerSwitchingMode = true,
Expand Down
6 changes: 3 additions & 3 deletions source/SpinalHDL/Libraries/EDA/altera/qsysify.rst
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ In the case of a UART controller :

.. code-block:: scala
case class AvalonMMUartCtrl(...) extends Component{
val io = new Bundle{
case class AvalonMMUartCtrl(...) extends Component {
val io = new Bundle {
val bus = slave(AvalonMM(AvalonMMUartCtrl.getAvalonMMConfig))
val uart = master(Uart())
}
Expand All @@ -31,7 +31,7 @@ The following ``main`` will generate the Verilog and the QSys TCL script with i

.. code-block:: scala
object AvalonMMUartCtrl{
object AvalonMMUartCtrl {
def main(args: Array[String]) {
//Generate the Verilog
val toplevel = SpinalVerilog(AvalonMMUartCtrl(UartCtrlMemoryMappedConfig(...))).toplevel
Expand Down
4 changes: 2 additions & 2 deletions source/SpinalHDL/Libraries/Graphics/colors.rst
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ You can use an Rgb bundle to model colors in hardware. This Rgb bundle take as p

.. code-block:: scala
case class RgbConfig(rWidth : Int,gWidth : Int,bWidth : Int){
case class RgbConfig(rWidth : Int,gWidth : Int,bWidth : Int) {
def getWidth = rWidth + gWidth + bWidth
}
case class Rgb(c: RgbConfig) extends Bundle{
case class Rgb(c: RgbConfig) extends Bundle {
val r = UInt(c.rWidth bits)
val g = UInt(c.gWidth bits)
val b = UInt(c.bWidth bits)
Expand Down
Loading

0 comments on commit 66671bf

Please sign in to comment.