====== Hierarchical design of a realistic buck controller ======

In this tutorial we revisit the [[tutorial:design:basic_buck:start|basic buck converter]] and design its controller with a more realistic interpretation of the UV, OC and ZC conditions. 

A common mistake of novice designers is to attempt creating a single monolithic STG capturing the behaviour of the whole circuit. This is infeasible for all but tiny circuits with a handful of signals.


<WRAP tip round center 90%>
The **main learning objective** of this tutorial is the use of //hierarchical decomposition// of the system into modules of manageable size, so that:
  * the overall controller can be specified as several small STGs rather than a big monolithic one which is very challenging for the human designer to create and comprehend;
  * circuit synthesis tools have to deal with smaller STGs, which reduces the risk of memory overflow or timeout due to state space explosion, as well as the risk of logic decomposition failure due to large complex-gates which cannot be decomposed into library gates in a speed-independent way.
</WRAP>

===== Informal specification =====

The system comprises an analog buck and its digital control logic as shown in the following diagram.

{{ schematic_diagram.svg?35% }}

The controller switches the power regulating PMOS and NMOS transistors ON and OFF by means of ''<color blue>gp</color>'' and ''<color blue>gn</color>'' outputs, as a reaction to ''<color red>uv</color>''\ (under-voltage), ''<color red>oc</color>''\ (over-current) and ''<color red>zc</color>''\ (zero-crossing) inputs. These inputs are produced in the analog part by comparators of measured current and voltage levels against reference values (''V_ref'', ''I_max'' and ''I_0'' respectively). These signals may be non-persistent, and so have to be sanitised before letting them into the digital controller.

To prevent a short-circuit, PMOS and NMOS must not be ON at the same time. This should be guaranteed by observing the ''<color red>gp_ack</color>'' and ''<color red>gn_ack</color>'' signals, which indicate when the power transistor threshold levels (''V_pmos'' and ''V_nmos'') are crossed.

The expected behaviour of a buck can be informally specified as follows:

  * While ''<color red>uv</color>'' is low -- wait in [[wp>Three-state_logic|tri-state]] (i.e. both PMOS and NMOS power regulating transistors are OFF).
  * While ''<color red>uv</color>'' is high -- keep performing cycles of charging:
    - A cycle of charging starts at tri-state; both ''<color red>oc</color>'' and ''<color red>zc</color>'' are low.
    - Switch PMOS transistor ON and wait for ''<color red>oc</color>'' to rise.
    - When ''<color red>oc</color>'' is high, switch PMOS transistor OFF.
    - When PMOS is OFF, switch NMOS transistor ON and wait for ''<color red>zc</color>'' to rise.
    - When ''<color red>zc</color>'' is high, switch NMOS transistor OFF and enter tri-state.

===== Decomposition of controller =====

One can notice two distinctive tasks for the controller: selecting the mode of operation (waiting or charging) as a reaction to ''<color red>uv</color>'' and performing a cycle of charging. This observation helps to decompose the controller into two modules, ''CYCLE_CTRL'' and ''CHARGE_CTRL'', communicating by a handshake:

{{ ctrl-top.circuit.svg?50% }}

''CYCLE_CTRL'' is the top-level controller deciding whether to perform a charging cycle and delegating this job to ''CHARGE_CTRL''.

Note that signals ''<color red>uv</color>'', ''<color red>oc</color>'', and ''<color red>zc</color>'' are produced by the analogue part of the buck and thus may be non-persistent. In order to prevent unexpected changes, they have to be sanitised using special [[:a2a:start|analog-to-asynchronous (A2A) components]]:

{{ ctrl-decomposed.circuit.svg?50% }}

For ''<color red>oc</color>'' and ''<color red>zc</color>'' we are only interested in catching their rising edges, therefore a basic ''WAIT'' element is used: 

<WRAP tip round center 90%>
''WAIT'' element works as follows:
  * Upon activation by ''<color red>ctrl+</color>'' it waits for (non-persistent) ''<color red>sig</color>=1'' (may miss short spikes) and latches it as ‘clean’ ''<color blue>san</color>'';
  * ‘Clean’ ''<color red>ctrl</color>'' / ''<color blue>san</color>'' handshake controlled by ‘dirty’ ''<color red>sig</color>''.
</WRAP>

For ''<color red>uv</color>'', however, both rising and falling edges are meaningful. Therefore we use a ''WAIT2'' element:

<WRAP tip round center 90%>
''WAIT2'' element is similar to ''WAIT'' but works with both phases of its (non-persistent) input ''<color red>sig</color>'':
  * after ''<color red>ctrl+</color>'' it waits for ''<color red>sig</color>=1'' (may miss short spikes) and latches it as stable ''<color blue>san</color>=1'';
  * after ''<color red>ctrl-</color>'' it waits for ''<color red>sig</color>=0'' (may miss short spikes) and latches it as stable ''<color blue>san</color>=0''.
</WRAP>

===== Design of controller modules =====


==== CYCLE module ====

''CYCLE'' should capture the following behaviour: 
  * initially ''<color red>uv_san</color>'' is low and controller waits for it to get high;
  * when ''<color red>uv_san</color>'' gets high the controller repeatedly initiates handshakes ''<color blue>chrg_req</color>''/''<color red>chrg_ack</color>'' on its interface to ''CHARGE'', thus instructing  it to perform charging cycles of the buck;
  * when ''<color red>uv_san</color>'' gets low, ''CYCLE'' stops initiating handshakes until ''<color red>uv_san</color>'' goes high again.

Note that there is a race between ''<color red>uv_san</color>'' going low and the decision to start another cycle of charging. When these happen close in time, there is a choice whether to squeeze in another cycle of charging or not. This behaviour is captured by the following STG where this choice is represented using place ''me'' (for //mutual exclusion//).

{{ cycle.stg.svg?35% }}

It is always a good idea to formally verify STG models using //Verification// menu. The above STG is consistent, deadlock-free, and input-proper. However, the output persistency property is violated. Indeed, outputs ''<color blue>uv_ctrl+</color>'' and ''<color blue>chrg_req+</color>'' disable each other. In fact, the choice at place ''me'' is an //arbitrating choice// and has to be implemented using a special component called ''MUTEX'' that can correctly handle the metastable behaviour associated with arbitration.

<WRAP tip center round 90%>
The protocol and circuit notation for ''MUTEX'' are as follows.
<WRAP>
<WRAP column half>
|{{ mutex.stg.svg?33% }}|
|  MUTEX specification  |
</WRAP>
<WRAP column half>
|{{ mutex-box.circuit.svg?50% }}|
|  MUTEX component  |
</WRAP>
</WRAP>
By tagging the choice place as a //Mutex// in the //Property editor//, the designer can prompt Workcraft to implement the associated choice by a ''MUTEX''. Note that the surrounding signals must follow the ''MUTEX'' protocol -- this can be verified via //Verification//->//Mutex place implementability [MPSat]//.
</WRAP>

Tag place ''me'' as a //Mutex// in the ''CYCLE'' STG and verify whether the surrounding signals follow the ''MUTEX'' protocol. In this case the property is violated: ''<color blue>uv_ctrl+</color>'' and ''<color blue>chrg_req+</color>'' (to be implemented by mutex grants) are triggered by ''<color red>uv_san-</color>'' and ''<color red>chrg_ack-</color>'', respectively, i.e. the phases of the signals do not match those in the ''MUTEX'' protocol. Hence we introduce a pair of internal signals which explicitly implement ''MUTEX'' requests with the correct polarity, which satisfies this property:

{{ cycle-mutex.stg.svg?35% }}


<WRAP tip round center 90%>
''CYCLE_CTRL'' module can be simplified by replacing ''WAIT2'' with ''WAIT'' and altering the logic of its operation. However, this is left as a take-home exercise -- this tutorial focuses on modular design, and this change would make ''CYCLE_CTRL'' too simple to justify a separate module.
</WRAP>

<WRAP hide>
++++ Optional optimisation of CYCLE module |

{{ cycle-opt.stg.svg?35% }}

++++
</WRAP>

==== CHARGE module ====

''CHARGE'' should capture the following behaviour:
  * Initially the buck is in the tri-state, i.e. both PMOS and NMOS power regulating transistors are OFF.
  * Upon receiving a request from ''CYCLE'', the PMOS transistor is switched ON and remains ON until OC condition.
  * After that the PMOS is switched OFF, and then NMOS is switched ON and remains ON until ZC condition.
  * Finally NMOS is switched OFF returning the buck to tri-state, and the handshake with ''CYCLE'' is completed.

The idea of the approach below is to start with a small yet meaningful STG capturing the core behaviour but is not necessarily synthesisable. Then we augment and refine it into a synthesisable STG using standard transformations. This way the initial specification is comprehensible for the human designer, and the subsequent design steps can be documented and easily checked.

=== Step 1: Initial design ===

The following STG captures the core behaviour of ''CHARGE''. Note that there are several problems with it:
  * The interface to the two ''WAIT'' elements is not modelled yet, and non-sanitized signals ''<color red>oc</color>'' and ''<color red>zc</color>'' are used instead.
  * The falling edges ''<color red>oc-</color>'' and ''<color red>zc-</color>'' are missing, and so the STG is not consistent.

{{ charge-compr-fr.stg.svg?35% }}

=== Step 2: Inserting the falling edges ===

As signals ''<color red>oc</color>'' and ''<color red>zc</color>'' will eventually be sanitized with the help of ''WAIT'' elements, the designer will ultimately have control of when to start waiting for them and when to reset the ''WAIT'' elements after the rising phases of these signals have been registered. The precise positions of the falling edges of these signals do not matter from the correctness point of view (as long as the consistency property is satisfied and no inputs are delayed), but it makes sense to remove them from critical paths and try to optimise the size of the circuit.

<WRAP center round tip 90%>
It is possible to insert such reset transitions automatically, with the view to satisfy the consistency property and heuristically optimise the quality of the resulting circuit. This functionality is not currently implemented in Workcraft, but accessible by running //Petrify// from the command line. Hopefully one day it will be available from Workcraft GUI...
</WRAP>

The STG below shows one possible way of inserting ''<color red>oc-</color>'' and ''<color red>zc-</color>''. <wrap tip>Note that this exercise is not about circuit optimisation; in practice, one would try to use the flexibility in inserting these signals to simplify the resulting circuit.</wrap>

{{ charge-compr.stg.svg?35% }}

=== Step 3: Sanitizing analogue inputs ===

Signals ''<color red>oc</color>'' and ''<color red>zc</color>'' are generated by the analogue part of the buck and thus there is no guarantee that they are persistent. Hence they have to be sanitised with the help of ''WAIT'' elements before letting them into the digital controller. This is actually a simple transformation: One can view the transitions of these signals as 'collapsed' handshakes with ''WAIT'' elements. Expanding them into proper handshakes can be done by selecting transitions ''<color red>oc+</color>'', ''<color red>oc-</color>'', ''<color red>zc+</color>'', ''<color red>zc-</color>'', and using //Transformations//->//Expand selected handshake transitions...// menu. Note that default suffixes for handshake expansion are ''_req'' and ''_ack'', but these can be changed by the designer, e.g. to ''_ctrl'' and ''_san'' in this case. (Alternatively one can expand handshakes by right-clicking a transition and choosing //Expand handshake transition...// in the popup menu.) The resulting STG is as follows:

{{ charge.stg.svg?35% }}

===== Verification of STG specifications =====

As usual, before proceeding to the synthesis step, one should validate the STG by simulation and formally verify the standard correctness properties (consistency, deadlock freeness, input properness, output persistency, mutex implementability) using //Verification// menu.

For ''CYCLE'' we also need to verify the implementability of the choice place ''me'' by a ''MUTEX'' using //Verification//->//Mutex place implementability [MPSat]// menu. Moreover, pairs of signals ''<color blue>uv_ctrl</color>'' / ''<color red>uv_san</color>'' and ''<color blue>chrg_req</color>'' / ''<color red>chrg_ack</color>'' are expected to form active handshakes, which must be verified as described in the [[tutorial:method:handshake_verification:start|Handshakes Verification tutorial]].

For ''CHARGE'' module we also need to verify the custom property that the power regulating PMOS and NMOS transistors are never ON at the same time, as explained in the [[tutorial:design:basic_buck:start|basic buck tutorial]]. Moreover, pairs of signals ''<color blue>oc_ctrl</color>'' / ''<color red>oc_san</color>'', ''<color blue>zc_ctrl</color>'' / ''<color red>zc_san</color>'', ''<color blue>gp</color>'' / ''<color red>gp_ack</color>'' and ''<color blue>gn</color>'' / ''<color red>gn_ack</color>'' are expected to form active handshakes, and ''<color red>chrg_req</color>'' / ''<color blue>chrg_ack</color>'' a passive handshake, which must be verified as described in the [[tutorial:method:handshake_verification:start|Handshakes Verification tutorial]].

When decomposing a system into smaller modules, there is a new type of problem: One module might produce an output unexpected by another module at that moment. For example, ''CYCLE'' could potentially fire ''<color blue>chrg_req+</color>'' output transition at a moment when ''CHARGE'' is not in a state that enables its ''<color red>chrg_req+</color>'' input transition. Similarly, ''CHARGE'' could potentially fire its ''<color blue>chrg_ack+</color>'' output at a moment when ''CYCLE'' is not enabling its ''<color red>chrg_ack+</color>'' input. Hence, one should verify that the modules //conform// to each other using the //Verification->N-way conformation [MPSat]...// menu. In general, there can be more than two modules interacting in complicated ways, and this check should include them all -- see the [[tutorial:method:hierarchical_design:start|Verification and synthesis of hierarchical designs]] tutorial for more detail.
===== Circuit synthesis and verification =====

Synthesise the STGs for the ''CYCLE'' and ''CHARGE'' modules using either //Technology mapping [Petrify]// or //Technology mapping [MPSat]// command in the //Synthesis// menu.

For ''CYCLE'' the result is the following circuit -- note that a ''MUTEX'' has been inserted automatically. (The name of ''MUTEX'' component and its ports can be adjusted in the //Digital Circuit//->//Mutex name and request-grant pairs// property of global preferences accessible via //Edit//->//Preferences...// menu.)

{{ cycle-tm.circuit.svg?50% }}

Technology mapping of ''CHARGE'' module using yields the following circuit. <wrap important>Note that the solution is not unique, and you may get a different circuit!</wrap> The STG has encoding conflicts (see [[tutorial:method:csc_resolution:start|Resolution of encoding (CSC) conflicts]] tutorial for more details), but Petrify and MPSat backends can resolve them automatically.


{{ CHARGE-tm.circuit.svg?50% }}

Note that automatic circuit layout (accessible via //Tools//->//Graph layout//->//Circuit placement and routing//) will not be as good as the above diagram. You may want to tidy it up manually (make use of //Dissolve joint// and //Straighten connection// commands in the popup menu) or download <wrap download>{{charge-tm.circuit.work}}</wrap>.

Verify these circuits for deadlocks, output persistency and conformation to the initial STGs. Note that in ''CYCLE'', whenever both ''MUTEX'' grants are enabled, firing one of them disables the other. This non-persistency, however, is not reported as a violation of output persistency check as it is correctly handled by ''MUTEX''.

Strategies for initialisation of the ''CYCLE'' and ''CHARGE'' modules are discussed in the [[tutorial:method:initialisation:start|Initialisation of speed-independent circuits]] tutorial.

===== Solutions =====

Download all the Workcraft models discussed in this tutorial here:

<wrap download>{{decomposition.zip|Decomposed buck controller models}}</wrap>

====== ======
{{page>:tutorial:feedback&inline}}