User Tools

Site Tools


Initialisation of speed-independent circuits

In this tutorial we will use CYCLE and CHARGE modules developed in the Hierarchical design of a realistic buck controller tutorial. The top-level schematic of the controller is as follows:


Circuit implementations of CYCLE and CHARGE modules and also STG specifications of their contract with environment (which will be used for circuit verification) can be downloaded here:

Module name STG specification Circuit implementation
CYCLE (3 KiB) (3 KiB)
CHARGE (4 KiB) (7 KiB)

Initialisation analyser

Initialisation (or reset) of a speed-independent circuit is an important part of the design process because a circuit can malfunction if its initial state is incorrect. Note that the initialisation phase of a speed-independent circuit does not have to be speed-independent: It is assumed that there is a special reset signal that is generated externally and behaves as follows:

  • When the power is connected, reset is low.
  • It stays low for sufficiently long time to complete the initialisation of all gates.
  • Eventually reset goes high, at which point the circuit is already correctly initialised and the normal speed-independent operation begins.
  • reset stays high for the whole time of circuit normal operation.

There are several ways of circuit initialisation that can be used in combination:

  • Rely on the initial state of some of the inputs (which are guaranteed to be correctly initialised by the environment). They propagate through some of the logic gates to initialise some of the internal and output signals.
  • Substitute some of the gates with ones containing an extra input that can act as a set or reset pin.
  • Insert additional gates to explicitly initialise the internal and output signals. Such gates will act as buffers during the normal operation, so one has to be careful not to break any isochronic forks.

Initialisation analyser [I] Initialisation analyser tool is designed to aid the decision of how to reset these modules. The tool uses Init to one and Forced init properties of circuit signals (i.e. primary input ports and output pins of circuit components):

  • Init to one property defines the initial state of the signal. If a circuit is synthesised by one of the backend tools, then the initial state of all its signals is set automatically. However, if the circuit is manually altered, then the designer is responsible for specifying the initial states of the signals.
  • Forced init property defines if the signal is known to be in a correct initial state. For a primary input it means the environment takes care of initialising the signal to its expected state. For a component output pin it means that the necessary circuitry will be added to properly initialise that pin.

These properties can be viewed and modified in the Property editor when an input port or an output pin is selected. Note that selecting a single-output component (i.e. a gate) also reveals these properties of its only output pin.

Initialisation analyser uses these properties as follows. It considers the signals whose Forced init property is set as initialised, while the remaining signals are assumed as uninitialised. The tool tries to evaluate each uninitialised signal on the Init to one property of initialised signals. If the Boolean value of a signal can be derived, then it is said to have propagated initial state and the signal is also considered initialised. The tool repeats evaluation of uninitialised signals until no further progress can be made, i.e. no new initialised signals can be obtained. At this stage, if some signals are still uninitialised it means Forced init property of the circuit signals needs to be adjusted, until all the signals are successfully initialised.

If the propagated initial state of a signal does not match its Init to one property, then the signal is said to have initialisation conflict – this often indicates a mistake, e.g. incorrect initial value of the signal. However, there are legitimate situations where such conflicts can occur – most likely such a signal needs to be explicitly initialised by setting its Forced init property.

Initialisation analyser visualises the initialisation state using the Gate highlight legend shown in the Tool controls:

By default the highlighting scheme is as follows (the colours can be adjusted in the preferences of digital circuit model – see Edit→Preferences…→Models→Digital Circuit):

  • The wires and pins of initialised signals are coloured red (if Init to one property is set) or blue (if Init to one is not set). Wires and pins of uninitialised signals are coloured black.
  • Components whose initial state cannot be determined via propagation of forced signals are not highlighted (i.e. remain white).
  • In case of initialisation conflicts, the problematic gates are highlighted magenta.
  • Output pins whose Forced init property is set are visualised by diamond shape and their components are highlighted orange.
  • Correctly initialised components are highlighted green.

Force init pins table enumerates the pins whose Forced init property is set. Note that Forced init property of a signal can be toggled while in Initialisation analyser tool by clicking the corresponding input port, output pin, or a gate. This enables convenient exploration of possible reset strategies. The tool also provides several ways of changing Force init property for a group of contacts:

  • Clear force init from all input ports and component outputs - Unset Forced init property for all input ports and component outputs.
  • Toggle force init for all input ports (environment responsibility) - Toggle Forced init property for all input ports. Note that it is the environment responsibility to guarantee the correct initialisation of primary inputs whose Forced init property is set.
  • Toggle force init for all self-loops - Toggle Forced init property for all component outputs with self-loops.
  • Toggle force init for all sequential gates - Toggle Forced init property for outputs of all sequential gates.
  • Remove force init from pins if redundant for initialisation - Unset Forced init property of the component outputs if they are redundant for the circuit initialisation.
  • Add force init to pins if necessary to complete initialisation - Set Forced init property of component outputs as necessary to complete initialisation of the circuit.

Circuit initialisation comprises three steps:

  1. Reset exploration – Decide which signals should be forced to the initial state, so that the correct initial values propagate to the remaining circuit components. Selecting a good set of forced signals is a creative process with multiple optimisation targets (avoiding critical paths, circuit size, gate complexity, etc.) and relies on designer experience.
  2. Reset insertion – Insert the reset port reset, set its Init to one property according to the reset active state (false for active low, true for active high), and use it to initialise all the signals that have Force init property set.
  3. Reset validation – Clear Force init property of all component pins and input ports, set Force init property for the reset port, and check that all the circuit components are correctly initialised.

Initialisation of CYCLE module

For initialisation of CYCLE we cannot rely on any inputs. Indeed, the WAIT2 element on uv_ctrl/uv_san interface does not have an explicit reset and the initialisation of CYCLE component on chrg_req/chrg_ack is not yet considered. The two inverters me_r1 and me_r2 on the MUTEX inputs are good candidates for introducing reset – click both of them to indicate their force initialisation (notice the diamond shape of their forcefully initialised output pins). As the result MUTEX grants get initialised in their correct initial states.

Initialisation of the CYCLE circuit

Now let us alter the circuit schematic and insert active-low reset signal nrst. This step will be automated in the future version of Workcraft, but currently we have to do it manually:

  • Insert a new input port nrst and make sure its initial state is low, i.e. its Init to one property is unchecked.
  • The output of inverter me_r1 needs to be initially high. This can be achieved by replacing this inverter by a NAND2 gate (set function for ON output is (A*B)') with one of its inputs connected to nrst.
  • The output of me_r2 inverter is initially low, therefore it should be replaced by a NOR2B gate (set function for ON output is (AN' + B)') whose inverted input is driven by nrst.

The modified circuit should look as follows (reset wires and modified gates are coloured dark green):


Use Initialisation analyser [I] Initialisation analyser to check that it is sufficient to set nrst low to force this amended CYCLE circuit to its initial state: Remove Forced init flag from me_r1 and me_r2 gates by clicking these gates, then click nrst port to indicate that it is guaranteed to be low. All the gates should be highlighted in green indicating their correct initialisation:

Initialisation of the CYCLE circuit - Reset

Also observe that when nrst goes high the circuit becomes equivalent to the original one.

Initialisation conflict happens when the Boolean function of the gate evaluates to a state that is different from the expected state of a signal. Such gates are highlighted in magenta. For example, if in CYCLE module one relies on input chrg_ack whose initial state is 0, then the inverter me_r2 evaluates to 1 which is different from the required initial state of this signal:

Initialisation of the CYCLE circuit - Conflict

In such situations the problemetic gate must be explicitly initialised to the required state. The user is expected to set Forced init flag on such a gate by clicking it in the Initialisation analysis tool.

Initialisation of CHARGE module

For initialisation of CHARGE module one can already rely on CYCLE module initialising chrg_req input to 0. Click on this input port to indicate that its initial state is guaranteed by the environment. The gates which are initialised correctly through this input will be highlighted in green:

Initialisation of the CHARGE circuit - Step 1

There is a combinational loop in this circuit that needs explicit initialisation – the one with _U12 gate. Click this gate to indicate that we will take care of explicitly initialising it – the gate will turn orange and its output pin will change its shape to a diamond:

Initialisation of the CHARGE circuit - Step 2

Now consider C-element _U5. Its inputs have the opposite initial values, so cannot force its output to any particular value, i.e. it needs to be forced to its initial value. Click on this C-element to indicate explicit initialisation – it will be highlighted in orange and its output will change its shape to a diamond:

Initialisation of the CHARGE circuit - Step 3

Let us see how the remaining gates can be initialised. Note that both oc_ctrl and zc_ctrl outputs are now successfully initialised to 0. At the top level, these signals interface the WAIT elements that produce oc_san and zc_san inputs, respectively. As WAIT element resets its san output when its ctrl input is low, signals oc_san and zc_san are guaranteed to be initially low – click these inputs to indicate this. Now the whole CHARGE module is initialised, provided that gates _U5 and _U12 (highlighted in orange) are explicitly reset:

Initialisation of the CHARGE circuit - Step 4

As we found a strategy to fully initialise the CHARGE component, let us implement it at the gate-level. The following changes are required:

  • Replace C-element _U5 with a resetable C-element – change its label from C2 to C2R, modify its Set function to A * B * RN, and Reset function to (A + B)' + RN'.
  • Change the type (i.e. the Label property) of gate _U12 from OAI22 to OAI221 and modify its Set function to ((A1 + A2) * (B1 + B2) * C)'.
  • Insert a new input port nrst whose initial state is low, i.e. Init to one property is not ticked.
  • Connect nrst to the RN pin of _U5 and to the C pin of _U12.

The CHARGE component with the initialisation circuitry looks as follows (the initialisation wires and modified gates are coloured dark green):


Again, use Initialisation analyser [I] Initialisation analyser to check that all the gates are correctly initialised by forcing only nrst, chrg_req, oc_san, and zc_san inputs. For this remove Forced init flag from the gates _U5 and _U12 by clicking them; also click nrst port to denote it is guaranteed to be low. All the gates should be highlighted in green indicating their correct initialisation:

Initialisation of the CHARGE circuit - Reset

Observe that when nrst is high, the circuit becomes equivalent to the original one.

Alternative reset insertion

An alternative way to reset the _U5 C-element is by forcing both its inputs to 0. This can be achieved by inserting an AND2 gate (set function for O output is A * B) in the wire between _U12 and _U5 gates and connecting nrst to one of its inputs:


It is not safe to insert a gate into a fork branch, as the fork ceases to be isochronic thus potentially breaking the speed-independence of the circuit. Such modifications must be verified.

Note, however, that inserting a new gate into the ‘trunk’ of a fork, before branching, is safe, as the resulting delay can be conceptually added to the delay of the driving gate.

In this particular case, a delay in the fork branch does not cause a problem – this can be checked by inserting a buffer into this branch (right-click on the wire and select Insert buffer command in the popup menu) and verifying that conformation, deadlock freeness, input properness, output persistency, and mutex implementability still hold. When verifying the circuit do not forget to set its Environment property so it points to the correct STG specification of CHARGE module (this can be done via the Property editor of the model). As an experiment, try to delay the other branches of this fork and see if this breaks any correctness properties.

Cyclic dependencies

When initialising a circuit composed from several blocks, one has to make sure that there are no cyclic dependencies during the initialisation.

For examples, CYCLE and CHARGE communicate via a handshake. Suppose CYCLE relies on its input chrg_ack to initialise chrg_req, and CHARGE relies on it input chrg_req to initialise chrg_ack. This creates a cyclic dependency and the resulting circuit will not initialise reliably.

Verification of circuits with initialisation

The obtained circuits have an extra nrst input. It is initially low and expected to stay low for sufficiently long to initialise all the gates into their expected initial states – note that the initialisation phase is not speed-independent (and not expected to be). When nrst goes high, the circuit starts its normal speed-independent operation.

This behaviour of nrst can be modelled by editing its properties as follows:

  • Uncheck Init to one property to specify that nrst is initially low.
  • Assign Set function to 1 to denote that nrst is only allowed to go high.

Now the circuits can be verified for deadlocks, output persistency, and conformation to the original STGs in the usual way via Verification menu. Do this for both CYCLE and CHARGE modules.

Exporting to Verilog

Both CYCLE and CHARGE modules are mapped to a gate library and correctly initialised. Now they can be exported to Verilog for the remaining stages of the design flow using FileExport.v (Workcraft Verilog serialiser) menu. Here is a result of exporting the CYCLE module:

// Verilog netlist generated by Workcraft 3 (Return of the Hazard), version 3.2.0
module CYCLE (chrg_ack, chrg_req, uv_ctrl, uv_san, nrst);
    input chrg_ack, uv_san, nrst;
    output chrg_req, uv_ctrl;
    NAND2 me_r1_rst (.ON(me_r1_rst_ON), .A(uv_san), .B(nrst));
    NOR2B me_r2_rst (.ON(me_r2_rst_ON), .AN(nrst), .B(chrg_ack));
    MUTEX me (.r1(me_r1_rst_ON), .g1(uv_ctrl), .r2(me_r2_rst_ON), .g2(chrg_req));
    // signal values at the initial state:
    // me_r1_rst_ON !me_r2_rst_ON uv_ctrl !chrg_req !chrg_ack !uv_san !nrst

The produced Verilog inherits the names of gates and pins as they are defined in the Property editor for the corresponding nodes. The specifications of these gates are taken by the technology mapping backend from the library/workcraft.lib GenLib file by default. A custom GenLib file can be supplied via Digital CircuitGate library for technology mapping property of global settings (accessible via EditPreferences… menu).

These names can also be substituted by providing a conversion file in the Digital CircuitSubstitution rules for export property of global preferences. For example, libraries/workcraft-tsmc_ghp.cnv file has the rules to convert librarys/workcraft.lib gates to match the naming convention of TSMC GHP library. For CYCLE module the produced TSMC-compatible Verilog is as follows:

// Verilog netlist generated by Workcraft 3 (Return of the Hazard), version 3.2.0
module CYCLE (chrg_ack, chrg_req, uv_ctrl, uv_san, nrst);
    input chrg_ack, uv_san, nrst;
    output chrg_req, uv_ctrl;
    ND2D1 me_r1_rst (.ZN(me_r1_rst_ON), .A1(uv_san), .A2(nrst));
    INR2D1 me_r2_rst (.ZN(me_r2_rst_ON), .A1(nrst), .B1(chrg_ack));
    MUTEX me (.r1(me_r1_rst_ON), .g1(uv_ctrl), .r2(me_r2_rst_ON), .g2(chrg_req));
    // signal values at the initial state:
    // me_r1_rst_ON !me_r2_rst_ON uv_ctrl !chrg_req !chrg_ack !uv_san !nrst


Download all the Workcraft models discussed in this tutorial here:

Circuit models (36 KiB)


Comments or suggestions for improving this tutorial
104 -10 = 
  • As discussed in, by default, the headers in included pages start one level lower than the last header in the current page. This can be tweaked by adding an empty header above the include:\\
    ====== ======

  • For offline help generation the content of feedback page should be temporary wrapped in <WRAP hide>. Note that the headers still propagate to the table of contents even if inside the hidden wrap. Therefore the Feedback title needs to be converted to something else, e.g. to code by adding two spaces in front.