====== Digital Circuit plugin ======

{{page>..:core:familiarise_hint&inline}}

This plugin is intended for capturing, simulation and verification of asynchronous digital circuits. For simulation and verification the circuit is automatically translated into a Signal Transition Graph (STG) that allows re-using the features of the [[..:stg:start|STG plugin]].

===== Capturing =====

In order to create a circuit model choose //File->Create work...// menu item and in the //New work// dialogue select //Digital Circuit// as the model type.

==== Functional components ====

The main building blocks of a digital circuit are functional components that can be created with the function generator {{editor_tools-function.png?nolink|[F] Function}}. Initially a generated component has only a single output pin (''<color blue>z0</color>'' by default). New pins can be added through the //Add output// or //Add input// items of the popup menu (accessible by right-clicking the component). The pin name and type can be changed in the property editor -- see //Name// and //I/O type// properties respectively.

{{ component.png?nolink |Generating a new component}}

Initially the output pin has neither set nor reset functions assigned. The set/reset functions can be specified by selecting the output pin and entering the corresponding [[..:boolean_expression|Boolean expressions]] in the //Set function// and //Reset function// entries of the property editor. Note that if a component has a single output pin (which if is the majority of logic gates) then the set/reset functions can be also modified in the properties of the component.

{{ function.png?nolink |Assigning set/reset functions}}

A component visualisation is defined by its //Render type// selected in the property editor, as follows:

  * //Box// -- the component is visualises as a box with explicitly named pins and their set and reset functions rendered next to them. This render type is convenient when a component has more than one output or its set/reset functions are too complex.

  * //Gate// -- the set and reset functions of a single component output are visualised using the traditional graphical mnemonics for Boolean operations. The obtained result is free of textual information (even the pins are not labelled) and therefore is usually easier to comprehend. Rendering a component as gate is convenient when it has a single output with relatively simple set/reset functions. This is the default rendering type with the following visualisation rules:
    * If both set and reset functions are specified then the component is rendered as a C-element. 
    * If only the set function is specified, then the reset function is assumed to be complimentary and the component is rendered as a combinational gate (possibly with several layers of logic). 
    * If the component cannot be rendered as a gate, e.g. because its set function is not empty or it has several output pins, then the //Box// visualisation is used.

{{ function-render_type.png?nolink |Function rendered as a gate and as a box}}

<WRAP info round>
Usually it is not necessary to explicitly create input pins. When a //Set function// or //Reset function// is entered for an output pin, the missing input pins are automatically created for all the literals in the [[..:boolean_expression|Boolean expressions]]. Note that the input pins do not disappear if they become unneeded after modification of the set/reset functions. You may need to manually remove those pins by first selecting them and then pressing <key>Delete</key> button.
</WRAP>
==== Input and output ports ====

Other building blocks of a digital circuit are its primary input and output ports. These are used to interact with the circuit environment. The ports are created with the port generator {{editor_tools-port.png?nolink|[P] Input/Output port}} -- just activate this editor tool and click the editor panel in a position you want to place the port. By default an output port is created, however, if you hold <key>Shift</key> while clicking the editor panel then an input port is created. Note that you can change the of existing port //I/O type// in the property editor too.

{{ ports.png?nolink |Input and output ports}}

==== Connections ====

When the connection tool {{..:core:editor_tools-connect.png?nolink|[C] Connect}} is active you can connect  the pins of the circuit components and primary ports. The output pins and the input ports can be connected either to the input pins or to the output ports. Several connections may start at the same output pin or an input port, however, only a single connection can end up at an input pin or an output port.  If an incorrect connection is attempted (e.g. a connection from an input pin to an output port or more than one connections to an input pin) then a warning message will be issued.

{{ connection-invalid.png?nolink |Invalid connection}}

In order to reduce the number of arcs going from the same output pin (or an input port) and simplify the layout of the connection arc, one can "fork" the wires -- just start a connection from an existing wire and a joint point will be automatically created. New connections can be also started from the existing joint points.

{{ connection-fork.png?nolink |Connections with forks}}

===== Editing =====

For editing the model activate the selection tool {{..:core:editor_tools-select.png?nolink|[S] Select}}. All the standard editing features (select, drag-and-drop, delete, copy, undo, group, etc.) work the same -- see generic help on [[..:core:tool_controls#Selection controls|Selection controls]] and [[..:core:property_editor|Property editor]] for details. 

Similar to all the other models, textual comments can be created by activating the {{..:core:editor_tools-text_note.png?nolink|[N] Text Note}} tool and clicking the editor panel in the position you want to put the text. Double-click on the note box to edit its text label in-place or do it through the property editor panel when the note is selected.

===== Simulation =====

For simulation of a Digital Circuit model activate the simulation tool {{..:core:editor_tools-simulate.png?nolink|[M] Simulate}}. The enabled pins and ports are highlighted and can be activated by clicking them. The simulation tool controls provide the means for analysis and navigation through the simulation trace, see generic help on [[..:core:tool_controls#Simulation controls]] for details. The circuit simulation is just an abstraction over the simulation of an automatically generated STG representation of the circuit components. Therefore all the specifics of [[..:stg:start#Simulation|STG simulation]] also apply to the Digital Circuit plugin.

The state of circuit's signals is visualised by colouring the corresponding pins and wires either <color blue>blue</color> (for logical ''0'') or <color red>red</color> (logical ''1''). Circuit pins associated with excited signals are highlighted and can be clicked to progress to the next state.

By default the circuit driver pins (input ports and the gate output contacts) are initialised to logical ''0''. This may lead to some of the circuit internal signals being excited when the simulation begins, e.g. the output ''out0'' is ''0'', but evaluates to ''1'' (first transition in the simulation trace). There are two ways to change the initial values to the circuit signals:
  * A driver pin can be set to logical ''1'' by ticking the //Init to one// property of the pin.
  * Alternatively, in simulation mode, when a desired association of signal values is reached, this state can be saved as the initial state of the circuit by pressing this button -- {{..:core:tool_controls-simulate-save_state.png?nolink|Save current state as initial}}.

{{ simulation.png?nolink |Circuit simulation}}

A circuit simulation trace can be converted to a //Digital Timing Diagram// by the generator of trace diagram {{..:core:tool_controls-simulate-generate_trace_diagram.png?nolink|Generate trace diagram}}. The order, visibility, and color of signal waveforms are specified in the signal state table -- see [[..:stg:start#Simulation|STG simulation]] help for details.

{{ simulation-trace_diagram.png?nolink |Timing diagram for circuit simulation trace}}

===== Verification =====

Verification of a digital circuit is usually made in the context of its environment. The environment can be described as an STG and attached to the circuit model using the property editor when no nodes are selected. 

When a verification task is issued via the //Verification// menu, the circuit is first translated into an STG that is subsequently composed with the STG of the environment. The resultant STG is used for verification of the desired properties:

  * //Conformation [MPSat]// -- verify if the circuit conforms to the environment   specification.
  * //Deadlock freeness [MPSat]// -- verify if the circuit is deadlock-free.
  * //Output persistency [MPSat]// -- verify if the circuit is output-persistent.
  * //Conformation, deadlock freeness, output persistency (reuse unfolding) [MPSat]// -- verify if the circuit conforms to the environment specification, is deadlock-free and output-persistent under the given environment.

====== ======
{{page>initialisation&inline}}

Consider our slightly modified circuit example with a zero delay inverter inserted before a NAND gate input. All the signals (except for the output of zero delay inverter) are initially //expected// (but not //guaranteed//!) to be ''0'', i.e. none of the driver pins have their //Init to one// property set.  Let us explore initialisation strategies by activating //Initialisation analyser// {{editor_tools-initialisation_analysis.png?nolink|[I] Initialisation analyser}}:

{{ initialisation-undefined.png?nolink |Undefined initialisation state}}

Notice that zero delay inverter is shaded in <color grey>grey</color> and its initial state cannot be forced, i.e. it is a don't touch component. As no //Forced init// property is set there is no //propagated// initial state, however, gate ''g0'' is highlighted in <color magenta>magenta</color> as //problematic//. Indeed, its output //expected// initial state is //low//, but its Boolean function evaluates to //high// when applied to the expected state of inputs. To resolve such initialisation problem the initial state of problematic pins have to be //forced//. Click gate ''g0'' of press {{tool_controls-initialisation-problematic.png?nolink|Force init output pins with problematic initial state}} button to set //Force init// property of ''g0'' output pin -- its highlighting color should change to <color orange>orange</color> indicating that it is the designers responsibility to force this gate to the expected state.

Let us assume that circuit's environment //forces// all the input ports to be in the //expected// state and indicate this by setting their //Forced init// property. This can be achieved by either clicking each input port, or by pressing {{tool_controls-initialisation-input_port.png?nolink|Force init all input ports (environment responsibility)}} button. The result should be as follows:

{{ initialisation-forced.png?nolink |Forced initial state}}

One can see that the C-element ''g1'' has been properly initialised via its inputs -- it is highlighted in <color green>green</color>. The output of ''g0'' is forced to its initial state -- it is highlighted in <color orange>orange</color>.

Now the circuit does not have any initialisation conflicts, however, its gate ''g0'' needs to be explicitly reset. This can be done automatically by pressing either //Insert reset (active-high)// or //Insert reset (active-low)// button. Here is a result of inserting active-high reset -- ''g0'' function is automatically modified to be resetable to ''0'', an input port ''<color red>reset</color>'' is added and connected to the new pin of ''g0'':

{{ initialisation-reset.png?nolink |Insertion of reset logic}}

Now the circuit is correctly initialised via its primary inputs -- all the gates are highlighted in <color lime>green</color> to indicate this. Note that the newly inserted ''<color red>reset</color>'' port is constrained by its set and reset functions, therefore the circuit can be verified against the original environment STG without reset signal.

====== ======
{{page>loop_breaking&inline}}