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:

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.

Now let us automatically insert active-low reset signal by clicking Insert reset (active-low) button. By default the reset port is called reset, but this can be changed via Digital Circuit→Reset port name of global properties. The modified circuit should look as follows:

Note that now only reset port is forced to its initial state and the rest of CYCLE circuit is correctly initialised.

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:

Two gates, _U5 and _U12, exhibit initialisation problem and need to be forced to the correct initial state. Indeed, C-element _U5 has its inputs in the opposite initial values, so cannot evaluate its output to any particular value. Similarly, gate _U12 has a feedback loop on one of its inputs and cannot be initialised to a correct state via its other inputs.

Click on each of these gates or press button to indicate that we will take care of explicitly initialising them – the gates will turn orange and the shape of their output pins will change to diamonds:

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:

In order to automatically insert active-low reset logic into the CHARGE component just press Insert reset (active-low) button. A reset pin will be added to _U5 C-element and a NAND2B gate will be added to the output of _U12 gate, both connected to the reset port:

Note that translation of a C-element into its init-low/init-high counterpart is defined by the following settings in Digital Circuit global preferences (accessible via Edit→Preferences…):

• Rules for init-low gates as comma-separated list original_gate→replacemant_gate(init_pin)
• Rules for init-high gates as comma-separated list original_gate→replacemant_gate(init_pin)

Default rules are C2→C2R(R), NC2→NC2R(R) and C2→C2S(S), NC2→NC2S(S), respectively. These define translation of C2 (positive C-element) and C2N (negative C-element) into their init-low (with reset pin R) and init-high (with set pin S) variants. The user can modify these rules to match C-element names in their library and/or to add translation rules for other resetable gates.

Use Initialisation analyser to check that it is sufficient to force only reset, chrg_req, oc_san, and zc_san inputs for correctly initialisation of CHARGE circuit.

An alternative way to reset the _U5 C-element is by forcing both its inputs to 0 (this may be useful if there is no C-element with reset pin in your library). This can be achieved by inserting a buffer in front of the C-element input that is expected to be high (right-click on the wire and select Insert buffer command in the popup menu) and setting initial state of the buffer output to low (clear its Init to one property). Now both inputs of the C-element are expected to be initially low and therefore its output evaluates 0.

In this particular case, a delay in the fork branch does not cause a problem, as can be confirmed by verifying the circuit correctness after the buffer insertion. As an experiment, try to delay the other branches of this fork and see if this breaks any correctness properties.

Note that the newly inserted buffer g0 exhibits a conflict of initialisation – its input is initially high, while the output is expected to be low. Therefore, the output of the buffer must be forced to the correct initial state by setting its Force init property). The complete alternative initialisation scheme should look as follows:

Insertion of the active-low reset yields the following circuit:

Here the buffer g0 is converted to an AND2 gate whose one input is connected to the reset port. The gate is forced low during reset and behaves as a buffer otherwise.

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.

The obtained circuits have an extra reset 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 reset goes high, the circuit starts its normal speed-independent operation.

This behaviour of reset is automatically imposed as follows:

• Its Init to one property is set to false (unchecked), thus specifying that reset is initially low.
• Its Set function is assigned to 1 and Reset function is assigned to 0, thus denoting that reset is only allowed to go high and then never go low again.

The circuits with reset 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.

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

cycle-tm-reset.v

// Verilog netlist generated by Workcraft 3 (Return of the Hazard), version 3.2.3
module CYCLE (chrg_ack, chrg_req, uv_ctrl, uv_san, reset);
    input chrg_ack, uv_san, reset;
    output chrg_req, uv_ctrl;
    wire me_r1_rst_ON, me_r2_rst_ON;
 
    NAND2 me_r1_rst (.ON(me_r1_rst_ON), .A(uv_san), .B(reset));
    NOR2B me_r2_rst (.ON(me_r2_rst_ON), .AN(reset), .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 !reset
endmodule

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 Circuit→Gate library for technology mapping property of global settings (accessible via Edit→Preferences… menu).

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

cycle-tm-reset-tsmc.v

// Verilog netlist generated by Workcraft 3 (Return of the Hazard), version 3.2.3
module CYCLE (chrg_ack, chrg_req, uv_ctrl, uv_san, reset);
    input chrg_ack, uv_san, reset;
    output chrg_req, uv_ctrl;
    wire me_r1_rst_ON, me_r2_rst_ON;
 
    ND2D1 me_r1_rst (.ZN(me_r1_rst_ON), .A1(uv_san), .A2(reset));
    INR2D1 me_r2_rst (.ZN(me_r2_rst_ON), .A1(reset), .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 !reset
endmodule

Download all the Workcraft models discussed in this tutorial here:

Circuit models (37 KiB)