====== Initialisation of speed-independent circuits ====== In this tutorial we will use ''CYCLE'' and ''CHARGE'' modules developed in the [[tutorial:design:hierarchical_buck:start|Hierarchical design of a realistic buck controller]] tutorial. The top-level schematic of the controller is as follows: {{ top-level.circuit.svg?50% }} 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'' | {{cycle.stg.work}} | {{cycle-tm.circuit.work}} | | ''CHARGE'' | {{charge.stg.work}} | {{charge-tm.circuit.work}} | ====== ====== {{page>:help:circuit:initialisation&inline}} ===== 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. {{ CYCLE-tm-analysis.circuit.png?nolink |Initialisation of the CYCLE circuit}} 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: {{ cycle-tm-analysis-reset.circuit.png?nolink |Initialisation of the CYCLE circuit - Reset}} Note that now only ''reset'' port is forced to its initial state and the rest of ''CYCLE'' circuit is correctly initialised. 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: {{ CYCLE-tm-analysis-conflict.circuit.png?nolink |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: {{ charge-tm-analysis-step1.circuit.png?nolink |Initialisation of the CHARGE circuit - Step 1}} 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 {{help:circuit:tool_controls-initialisation-problematic.png?nolink|Force init output pins with problematic initial state}} 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: {{ charge-tm-analysis-step2.circuit.png?nolink |Initialisation of the CHARGE circuit - Step 2}} 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: {{ charge-tm-analysis-step3.circuit.png?nolink |Initialisation of the CHARGE circuit - Step 3}} 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: {{ charge-tm-analysis-reset.circuit.png?nolink |Initialisation of the CHARGE circuit - Reset}} 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// {{help:circuit:editor_tools-initialisation_analysis.png?nolink|[I] 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. ==== Alternative reset insertion ==== 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''. 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, 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: {{ charge-tm-analysis-alt.circuit.png?nolink |Alternative initialisation of the CHARGE circuit}} Insertion of the active-low reset yields the following circuit: {{ charge-tm-analysis-alt-reset.circuit.png?nolink |Alternative initialisation of the CHARGE circuit - Reset}} 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. ===== 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 ''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. ===== Exporting to Verilog ===== 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: // 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: // 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 ===== Solutions ===== Download all the Workcraft models discussed in this tutorial here: {{initialisation.zip|Circuit models}} ====== ====== {{page>:tutorial:feedback&inline}}