Buck converter is a voltage step down and current step up converter. It comprises an analogue buck and its digital control logic as shown in the following diagram. Your task in this tutorial is to formally specify, synthesise and verify the control circuitry of the buck.

The controller switches the power regulating PMOS and NMOS transistors ON and OFF as a reaction to under-voltage (UV), over-current (OC) and zero-crossing (ZC) conditions. These conditions are detected and signalled by a set of specialised sensors implemented as comparators of measured current and voltage levels against some reference values (V_ref, I_max and I_0 respectively). Note that the gp and gn signals are buffered to drive the very large power regulating transistors (occupy more than 50% of the buck area) and their effect on the buck can be significantly delayed. Therefore, the controller is explicitly notified (by the gp_ack and gn_ack signals) when the power transistor threshold levels (Th_pmos and Th_nmos) are crossed.

The operation of a buck is usually specified in an intuitive, but rather informal way, e.g. by enumerating the possible sequences of detected conditions and describing the intended reaction to them, as in the following phase diagram.

This specification shows the alternation of the UV and OC conditions which are handled by switching the power regulating PMOS and NMOS transistors of the buck ON and OFF. Detection of the ZC condition after UV does not change this behaviour, however, if ZC is detected before UV then both the PMOS and NMOS transistors remain OFF until the UV event.

It is important to note that in order to avoid a short-circuit the PMOS and NMOS transistors of the buck must never be ON at the same time.

According to the phase diagram there are three distinctive scenarios to capture:

• no ZC – UV happens without ZC;
• late ZC – UV is followed by ZC;
• early ZC – UV happens after ZC.

Let us first capture the no ZC scenario as an STG.

Detailed instructions

The resulting STG listing the sequence of signal events for this scenario is shown in the following diagram. Save this model as buck-scenario1_no_zc.stg.work file.

The scenario for late ZC is formalised in a very similar way. Both phases of ZC just happen concurrently with switching NMOS transistor OFF and PMOS transistor ON. Save the no ZC model with new name buck-scenario2_late_zc.stg.work and modify it according to the late ZC scenario.

Detailed instructions

The resulting STG should look similar to the following diagram. Do not forget to save the work!

The scenario for early arrival of ZC is a bit different. Here the NMOS transistor needs to be switched OFF as soon as ZC is detected, without waiting for UV. However, switching the PMOS transistor ON is still delayed till UV condition.

Save the late ZC model under new name buck-scenario3_early_zc.stg.work and do the necessary changes for the early ZC scenario.

Detailed instructions

The modified STG should look similar to the following diagram.

In order to produce an implementation capable of handling all the scenarios, these STGs need to be merged into a single specification. One can see that all three STGs have ‘compatible’ initial states, that is all common input and output signals have the same initial values. Therefore one can merge the initially marked places in the three STGs and obtain a combined specification for buck control.

• Create a new STG work called buck-scenarios_merged.stg.work.
• Copy and paste the three scenarios into it.
• Select the three initially marked places (by holding Shift and clicking them with the mouse) and merge them into a single place using Transformations→Merge selected places.

The STG combining all three scenarios should look like the following diagram. Do not forget to save the work!

Once the initially marked places are merged, one can notice that three transitions oc- leading to it can also be merged because their preceding states are ‘compatible’. This process continues with signal event gn_ack+, and so on, ‘zipping’ the common paths of the STGs together. The simplified STG specification of the buck control is as follows; save it as buck-simplified.stg.work file.

Note that this STG is just a cosmetic improvement over the previous one and so this step does not affect the verification and synthesis. However, it does improve the visual representation making the STG more comprehensible, and thus it is important from the designer's perspective.

Activate the simulation tool and exercise the obtained STG model. Click one of the enabled signal transitions (they are highlighted in orange) to evaluate the STG into the next state. Make sure the simulation traces correspond to those intended by the informal specification of the phase diagram.

Before proceeding to the synthesis step verify that the STG specification satisfies the following Verification properties using Verification menu:

• Deadlock freeness – every reachable marking enables at least one transition.
• Consistency – the '+' and '-' transitions of every signal alternate in every execution, always starting with the same sign.
• Input properness – an input cannot be disabled by an output or internal signal, and cannot be triggered by an internal signal.
• Output persistency – an enabled output or internal signal cannot be disabled by any other signal.
• Output determinacy – the STG is not self-contradictory, i.e. one cannot find a pair of traces having a common prefix, with one of them requiring and the other forbidding to produce a particular output after this prefix; note that for non-deterministic STGs like this one this propery is essential.

These are basic soundness properties which should be satisfied by most models – Verification menu has an entry that can check all these properties with a single click.

The pairs of signals gp / gp_ack and gn / gn_ack must follow the handshake protocol, and so these two handshakes must be verified as described in the Handshakes Verification tutorial. Note that these handshakes are active, as the controller initiates them, and that the initial state of the gn / gn_ack handshake is such that its first half is already complete.

Another property one must verify is that PMOS and NMOS transistors are never ON simultaneously (which would lead to a short-circuit), i.e. that signals gp and gn are never high at the same time. This custom property can be formulated as a reachability analysis problem using Reach language:

• Open the REACH assertion dialog by selecting Verification→REACH assertion [MPSat]… menu.
• In MPSat settings set the Mode into STG reachability analysis and the Solution into minimise cost function.
• Enter a Reach predicate specifying the short-circuit condition: both gp and gn signals are high – $S"gp" & $S"gn". Here "gp" and "gn" are the names of the signals, operator S turns a string into a signal with that name, operator $ gives the value of a signal in the state to be reached, and & is Boolean AND.
• Select unsatisfiable to denote that the property holds if predicate is unsatisfiable.
• Save this property as a preset for future use, e.g. under the name short circuit check.

The whole REACH assertion dialog should look as follows.

When you click the   OK   button the STG will be searched for a state where the Reach predicate evaluates to True. If such a state exists then the Reach predicate is satisfiable and the property is violated; else the property holds. If the property is violated then a trace leading to a problematic state is reported. This trace can be simulated to diagnose the problem and correct it at the level of STG specification. The minimise cost function setting ensures that this violation trace is as short as possible, which helps debugging.

Note that the property that signals gp and gn are never high at the same time is not sufficient to guarantee the absence of short-circuits. Indeed, the PMOS and NMOS transistors are big and slow, and so if e.g. gp+ happens immediately after gn-, a transient short-circuit may be possible even though the property holds. In fact, the signals gp_ack and gn_ack were introduced specifically to detect the completion of the switching of the corresponding transistors, making it possible to avoid such short-circuits. Hence, a stronger correctness property ensuring that gp cannot be high whenever gn or gn_ack is high, and similarly gn cannot be high whenever gp or gp_ack is high, can be formulated as ($S"gp" | $S"gp_ack") & ($S"gn" | $S"gn_ack"), where | is Boolean OR. Verify that this stronger property also holds for the above STG model.

The STG specification can now be synthesised into an asynchronous circuit implementation either with MPSat or Petrify back-end tools via Synthesis menu. For example, the following Petrify's complex-gate implementation can be obtained by choosing Synthesis→Complex gate [Petrify]:

Note that the solution is not unique and you may get a slightly different one. In particular, instead of the NOR gate Petrify is likely to output an AND gate with three input ‘bubbles’ – this can be fixed by right-clicking the gate and selecting Propagate inversion through gate from the popup menu. Save this circuit with the name buck-cg-petrify.circuit.work.

Activate the simulation tool and simulate the captured complex gate implementation of the buck control. Ports, pins and wires are colour-coded: blue means low level and red means high level of the signal. Excited pins and ports are highlighted in orange.

Click an excited pin to toggle its logical value – the circuit will evaluate to the next state where new set of signals will be enabled. The sequence of signal events is recorded in the simulation trace and can be subsequently replayed for analysing the circuit's behaviour.

Verify that the circuit conforms to the environment specification, is free from deadlocks and output persistent. All these verification steps can be run via Verification→Conformation, deadlock freeness, output persistency (reuse unfolding) [MPSat] menu.

When synthesising a complex-gate implementation with MPSat (via Complex gate [MPSat] menu) the circuit looks as follows (after some manual editing):

Note that the gate computing gp now has feedback, which suggests that it may be advantageous to implement gp by a latch (i.e. a state-holding element) rather than a combinational gate. Below we explore some such implementations.

The standard-C architecture (a.k.a. “monotonic covers”) is shown in the picture below. It uses a C-element as the state-holding element that is driven by two combinational gates computing the Set and (inverted) Reset functions of the implemented signal. The Set and Reset functions are mutually exclusive, i.e. they are never 1 at the same time; hence, due to the Reset function being inverted, the inputs of the C-element cannot be 10 (combinations 00, 01, and 11 are possible).

The standard-C implementation of the buck STG can be synthesised using Synthesis→Standard C-element [MPSat] menu. By inspecting the resulting circuit (not shown) one can see that:

• There is no benefit in implementing gn using standard-C architecture, as the original complex-gate implementation is simpler. (In some situations, e.g. if there are only 2-input gates/latches in the gate library, this standard-C implementation may come useful.)
• The standard-C implementation of gp is nicer than the complex-gate one, in particular it does away with that ugly 4-input gate that may be absent from the gate library.

By selecting the complex-gate implementation of gn and the standard-C one of gp the following hybrid circuit is obtained:

Complex-gate and standard-C syntheses are oblivious to the gate library – the implementations they yield are Boolean functions of arbitrary complexity. These functions are often too large to be implemented by a single gate available in the gate library. Unfortunately, breaking up a complex-gate into smaller ones, when performed naïvely, generally yields an incorrect circuit – this happens due to the delays associated with the outputs of the newly introduced gates. In fact, logic decomposition in the context of speed-independent circuits (see the Logic decomposition and technology mapping tutorial) is a very difficult problem, that cannot always be solved. Petrify and MPSat backend tools do a good job in many situations, but occasionally they fail to converge to a solution and a manual intervention by the designer is required.

The decomposed and mapped implementation of the buck STG can be synthesised using Synthesis→Technology mapping [Petrify] or Synthesis→Technology mapping [MPSat] menu. E.g. Petrify's solution, after some manual editing, is as follows (note that the solution is not unique and you may get a slightly different one):

The circuit is now mapped – the gate labels correspond to the gate names in the library. The two inverters are shown with a dotted line through – this is because they have the Zero delay property expressing the assumption that their delays are negligible. This is usually unproblematic as long as such input inverters are placed next to the main gate, but in some situations this assumption may be questionable; moreover, this assumption introduces extra constraints that have to be satisfied during placing and routing.

Let us try to decompose the implementation of gp into gates/latches with at most two inputs. In the Edit→Preferences dialog, select External tools→MPSat synthesis and tick the Edit additional parameters before every call checkbox. Then select Synthesis→Technology mapping [MPSat]. A dialog box will pop up asking for extra command line parameters to pass to MPSat – type -g2 to restrict MPSat to gates/latches with at most two inputs. The following implementation of gp can then be computed (note that solution is not unique and you may get a slightly different one).

This solution happens to have no input inverters, and so no timing assumptions have to be made. Verify this circuit w.r.t. the original STG as described above for the complex-gate implementation.

Download all the Workcraft models discussed in this tutorial here:

Buck control models (88 KiB)