Advanced User Guides - ChairImpSec/PROLEAD GitHub Wiki

Requirements

Writing your own Cell Library

We strive to provide templates for commonly used standard cell libraries in the repository. However, if you need to evaluate a netlist synthesized with a standard cell library that is not included, you will need to create your own library description. The following guide will help you create a custom library description compatible with PROLEAD, ensuring accurate simulation of your netlist.

Note: Once you've completed your custom library description and are satisfied with the results, consider submitting a pull request so others can benefit from your work. The same applies if you find bugs or add missing cells to existing library descriptions.

Specify a New Library

PROLEAD requires the library to be provided as a JSON file. To get started, copy the following code snippet into a new JSON file.

{
  "libraries": [
    {
      "name": "nang45",
      "cells": [...]
    }
  ]
}

You can define multiple libraries within a single JSON file. The libraries array holds the list of these libraries. Each library is a JSON object that includes a unique identifier, name, and a cells array containing the various cells defined by the library. For example, we use the name nang45 for our sample library. To use this library with PROLEAD, specify its name using the command-line parameter, e.g., -n nang45.

Specify a new Cell

The cells array can contain as many gates as needed. Note that every gate instantiated in your netlist must also be defined in your library. The only exception is assign statements, which PROLEAD automatically converts into buffer cells. However, this requires that a buffer cell is defined in your library. Every cell is specified as a JSON object with the following parameters.

Cell Parameter Description
name Every cell needs a unique identifier for PROLEAD's internal computation. The name does not affect the cell's behavior.
aliases A cell with the same functionality may appear under different names in the netlist, for example, when specified with varying drive strengths. All possible identifiers for such a cell need ton be listed here.
type To accurately simulate a cell's functionality, you must specify its type. Valid types include buffer, gate, relaxed_gate, register, and latch. Typically, combinational cells are specified as gate and sequential cells as register. The types gate and relaxed_gate correspond to different evaluation models. For cells labeled as gate, PROLEAD applies the probe-extension procedure from the robust probing model. In contrast, cells labeled as relaxed_gate use the conditional probe-extension procedure defined by the robust but relaxed probing model.
timing If you specify a sequential cell (type: register), you must indicate the clock edge on which the cell should toggle. Valid parameters are rising_edge, falling_edge, and both.
clock If you specify a sequential cell (type: register), it must be driven by a clock signal. This setting designates the port reserved for receiving the clock signal.
inputs All input ports of the cell need to be specified.
outputs All output ports of the cell need to be specified.
equations For each output port, you must define how the cell generates the corresponding output signal. This can be done by either (1) specifying a Boolean equation or (2) providing a lookup table. In both cases, a single string must be supplied for each output, listed in the same order as the output ports.

Additionally, attributes can be defined for a cell, which is common for FPGA cells. All possible attributes must be listed in the cell specification, each with a default value that is used if the attribute is not explicitly set during cell instantiation. Note that attributes have no inherent behavior by default—their functionality must be explicitly implemented by referencing them in the equations array. So far, PROLEAD cannot support string-based attributes. Hence they must be entirely removed from the netlist.

Specify Basic ASIC Cells

As an introductory example, we present the specification of two cells from the Nangate 45nm standard cell library: a combinational cell, specifically a half adder, and a sequential cell, namely a positive-edge-triggered D flip-flop.

Half Adder Cell Specification Pos. Edge Flip-Flop Cell Specification 
        {
          "name": "ha",
          "aliases": ["HA_X1"],
          "type": "gate",
          "inputs": ["A", "B"],
          "outputs": ["CO", "S"],
          "equations": ["A and B", "A xor B"]
        }
 
        {
          "name": "dff",
          "aliases": ["DFF_X1", "DFF_X2", "DFF_X4"],
          "type": "register",
          "timing": "rising_edge",
          "inputs": ["D", "CK"],
          "clock": "CK",
          "outputs": ["Q", "QN"],
          "equations": [
            "((not CK) and Q) or (CK and D)",
            "((not CK) and (not Q)) or (CK and (not D))"
          ]
        }

Specify Parameters for FPGA Cells

The most common use of parameters is in the description of lookup table (LUT) cells for FPGAs. To define the functionality of a LUT cell, you must use an INIT string instead of directly specifying a Boolean function. This INIT string is typically provided as an attribute for each cell instance. Consequently, the INIT variable must also be declared as a parameter in the cell description. For example, see the cell description of a 3-input lookup table. However, parameters can also be integrated directly into Boolean functions, for instance, to invert specific input ports based on attribute values. This approach is demonstrated in the cell description of a D Flip-Flop with Clock Enable and Synchronous Reset (FDPE)."

3-Input Lookup-Table Specification D Flip-Flop with Clock Enable and Synch. Reset Specification 
{
    "name": "LUT3",
    "aliases": ["LUT3"],
    "type": "gate",
    "parameter": [{"name": "INIT","default": "8'h00"}],
    "outputs": ["O"],
    "inputs": ["I0", "I1", "I2"],
    "equations": ["INIT[7:0]"]
}
 
{
    "name": "FDRE",
    "aliases": ["FDRE"],
    "type": "register",
    "timing": "rising_edge",
    "parameter":
        [
            {"name": "INIT", "default": "1'b0"},
            {"name": "IS_C_INVERTED", "default": "1'b0"},
            {"name": "IS_D_INVERTED", "default": "1'b0"},
            {"name": "IS_R_INVERTED", "default": "1'b0"}
        ],
    "inputs": ["C", "CE", "D", "R"],
    "clock": "C",
    "outputs": ["Q"],
    "equations": 
        [
            "(not (R xor IS_R_INVERTED[0])) and (((not CE) and Q) or ((C xor IS_C_INVERTED[0]) and CE and (D xor IS_D_INVERTED[0])))"
        ]
}

When an instance of such a cell appears in the netlist, PROLEAD parses the attributes set for that instance and overrides the corresponding default values defined in the cell description. If an entire parameter, such as an INIT string, is used to solely define an equation, PROLEAD automatically interprets it as a LUT description and converts it into a Boolean function. For any attributes not explicitly set in the instance but defined in the cell description, PROLEAD uses the specified default values.

⚠️ **GitHub.com Fallback** ⚠️