tutorial.md

Tutorial

This tutorial will walk you through generating a sync model and examining its content. As an example we will use the d-element async circuit in the tool's examples directory.

Input Circuit

The content of the input circuit (examples/d-element/circuit.v) are shown below:

// Verilog netlist generated by Workcraft 3 -- https://workcraft.org/
module Untitled (ao, ri, ai, ro);
    input ao, ri;
    output ai, ro;

    NOR2 _U0 (.ON(ai), .A(ao), .B(_U2_QN));
    AND2 _U1 (.O(ro), .A(ri), .B(_U2_QN));
    NC2 _U2 (.QN(_U2_QN), .A(ao), .B(ri));

    // signal values at the initial state:
    // !ai !ro _U2_QN !ao !ri
endmodule

This circuit was generated from a formal specification by Workcraft.

Running the Tool

A synchronous model of the above circuit can be generated by running:

./generator.py examples/d-element/circuit.v > model.v

from the tool's root directory.

Output Circuit

The content of the generated model.v are shown below. The file contains two modules: the sync model circuit_inner and a thin wrapper circuit that provides the same interface as the input circuit.

From a quick look at circuit, the main components of the model are:

• the same logic gates in the input circuit (_U0, _U1 and _U2)
• additional flip-flops to capture wire states (e.g. ao_ff)
• an unbound register fire that determines transition ordering

Read the next subsection for instructions on how to use this circuit in verification.

// vi: set ft=verilog :

module circuit (
        input reset,
        input clk,
        input ao,
        input ri,
        output ai,
        output ro
    );

    // This is a thin wrapper to provide the same interface as the original
    // circuit.

    circuit_inner circuit1 (
        .reset(reset),
        .clk(clk),
        .ao_precap(ao),
        .ri_precap(ri),
        .ai(ai),
        .ro(ro)
    );

endmodule

module circuit_inner (
        input reset,
        input clk,
        input ao_precap,
        input ri_precap,
        output ai,
        output ro
    );

    reg [2:0] fire; // unbound register

    // input signal 'ao' (initial value = 0)

    DFF ao_ff (
        .CK(clk),
        .ST(1'b0),
        .RS(reset),
        .D(ao_precap),
        .Q(ao),
        .ENA(fire == 0)
    );

    // input signal 'ri' (initial value = 0)

    DFF ri_ff (
        .CK(clk),
        .ST(1'b0),
        .RS(reset),
        .D(ri_precap),
        .Q(ri),
        .ENA(fire == 1)
    );

    // internal signal '_U2_QN' (initial value = 1)

    NC2 _U2 (
        .CK(clk),
        .RS(1'b0),
        .ST(reset),
        .PRECAP(_U2_QN_precap),
        .A(ao),
        .B(ri),
        .QN(_U2_QN),
        .ENA(fire == 2)
    );

    // output signal 'ro' (initial value = 0)

    AND2 _U1 (.A(ri), .B(_U2_QN), .O(ro_precap));

    DFF _U1_ff (
        .CK(clk),
        .ST(1'b0),
        .RS(reset),
        .D(ro_precap),
        .Q(ro),
        .ENA(fire == 4)
    );

    // output signal 'ai' (initial value = 0)

    NOR2 _U0 (.A(ao), .ON(ai_precap), .B(_U2_QN));

    DFF _U0_ff (
        .CK(clk),
        .ST(1'b0),
        .RS(reset),
        .D(ai_precap),
        .Q(ai),
        .ENA(fire == 3)
    );

    // Stateless modules

endmodule

Verification

The model above can be used as a drop-in replacement for the input async circuit. Once the model is instantiated in the parent system, system-level properties can be written and checked using standard (sync) verification tools.

To keep things simple, we will verify the model on its own in this tutorial. Also, instead of writing formal properties ourselves, we will use the tool to create a sync specification model of d-element. The specification model (spec model for short) contains a synchronous FSM that can be simulated in tandom with the circuit model to detect transitions that don't conform to specification. To generate this model, run:

./generator.py --spec examples/d-element/spec.sg --output generated examples/d-element/circuit.v

This call is similar to the one before but with two differences:

1. We use --spec to load a Signal Transition specification file (in .sg format)
2. We use --output to write output files to a directory generated instead of printing them on the terminal window

When --spec is used, the tool generates both the circuit and a spec model. The directory generated should now contain two files:

• circuit.v (circuit model)
• spec.v (spec model)

The file spec.v contains two modules: the spec model itself (spec) and a binding module (bind_info). The latter is used by many verification tools to inject verification properties and associated circuitry into a target circuit (it is considered good practice to separate module implementation and verification properties).

Both files can now be passed to a sync formal verification tool to verify spec compliance. If the verification tool does not support loading .lib files, corresponding Verilog files are provided in the directory gates.

As an example, we provide the output log produced by a commercial verification tool running on circuit.v and spec.v:

Verification mode:
  circuit1.u1.persistency_ro : Pass - Trigger: Pass (6)
  circuit1.u1.compliance_ro_rise : Pass - Trigger: Pass (6)
  circuit1.u1.persistency_ai : Pass - Trigger: Pass (16)
  circuit1.u1.persistency__U2_QN : Pass - Trigger: Pass (10)
  circuit1.u1.compliance_ai_fall : Pass - Trigger: Pass (22)
  circuit1.u1.compliance_ai_rise : Pass - Trigger: Pass (16)
  circuit1.u1.deadlock_free : Pass
  circuit1.u1.compliance_ro_fall : Pass - Trigger: Pass (12)
Assertion Summary:
  Total                  :   8
  Pass                   :   8
  Not_Run                :   0

In the above:

• Internal/output signals ro, ai and _U2_QN passed persistency checks
• Output signals ro and ai passed compliance checks
• The circuit passed deadlock checks