Examples

Rc filter

A first-order RC low-pass ahead of an ADC, and one question about it, asked twice. It is the smallest board that shows a constraint nobody can decide getting decided: by a simulator, through the commit gate, and then by nothing more than the evaluator.

the interconnect view — The interconnect view

The program

rc_filter.py puts 10 kOhm and 10 nF between two connectors and requires the -3 dB corner to lie between 1.5 and 1.7 kHz. The corner is a parameter with no value, because nothing on the page has measured it; the constraint over it is undecided, and fang check says so.

The question is declared beside the requirement it serves, with its bench in full: 1 V driven into the input, an AC sweep from 10 Hz to 1 MHz, and the two connectors deliberately left out. The corner is where the output falls through 1/sqrt(2) of the input.

corner_check = Simulates(
    "corner_spec",
    measures={"corner": Crossing("adc.line", level=707.1 * mV, edge="falling")},
    supplies={"source.line": 1 * V},
    analysis=ACSweep(variation="dec", points=100, start="10", stop="1meg"),
    abstracted=("source", "adc"),
)

Simulates has no result argument. A question’s result is produced by a run; a program that tries to state one is refused.

What comes out

4 parts, 3 nets, 37 entities, 2 checks, none failed and both undecided, until the question is answered.

out/verification.txt is the file to read. On the elaborated program the constraint is undecided, so the question routes to the circuit level and ngspice answers it: 1590 Hz, inside the band, PASS. The measurement re-enters as a transaction (the corner set to an inferred value whose source is the run’s evidence) and the gate’s constraint check decides the constraint. Asked again on that committed head, the same question is answered at the equation level: the evaluator already decides the constraint, so nothing runs.

out/rc_filter.net, out/netlist.txt
out/checks.txt: the two constraints over the corner, undecided
out/graph.txt, out/rationale.md

The listing gives three significant figures and no tool version, so it stays put when ngspice moves a number in its fourth figure. The evidence keeps every figure ngspice printed, the version, the hash of the deck, and the assumptions and coverage gaps listed above.

Running it

fang verify examples/rc_filter/rc_filter.py                 # nothing persists
fang build  examples/rc_filter/rc_filter.py
fang verify examples/rc_filter/rc_filter.py --commit        # the corner enters the workspace
fang verify examples/rc_filter/rc_filter.py                 # answered at the equation level

fang verify needs ngspice on the path. Without it the question is reported unsupported, by name, and nothing else answers it.

The whole program

"""A first-order RC low-pass, and one question about it asked twice.
Show 14 more lines

An anti-aliasing filter ahead of an ADC: 10 kOhm and 10 nF put the -3 dB
corner at 1 / (2 pi R C), about 1.59 kHz, and the requirement holds it between
1.5 and 1.7 kHz. The program declares the corner as a parameter with no value,
because nothing on this page has measured it, and a question that measures it:
an AC sweep with 1 V driven into the input, the corner being where the output
falls through 1/sqrt(2) of that.

The first `fang verify` finds the constraint undecided and routes the question
to the circuit level, where ngspice answers it; the measurement comes back
through the commit gate. Asked again on the committed head, the same question
is answered at the equation level: the evaluator already decides the
constraint, so nothing runs.
"""

from fang.interfaces import AnalogIn, AnalogOut, Pin, PinMap
from fang.lang import Parameter, Part, System, V, kHz, kOhm, mV, nF, require
from fang.parts import Capacitor, Resistor
from fang.rationale import Calculates, Requires
from fang.simulation import ACSweep
from fang.verification import Crossing, Simulates


class SignalIn(Part):
    """Where the signal arrives: a tip, and a sleeve that is ground."""

    designator_prefix = "J"

    line = AnalogOut()

    TIP = Pin("TIP", role="analog", number="1")
    SLEEVE = Pin("SLEEVE", role="ground", number="2")

    pinmap = PinMap({"line.signal": "TIP", "line.ref": "SLEEVE"})


class AdcInput(Part):
    """Where the filtered signal leaves for the converter."""

    designator_prefix = "J"

    line = AnalogIn()

    SIG = Pin("SIG", role="analog", number="1")
    GND = Pin("GND", role="ground", number="2")

    pinmap = PinMap({"line.signal": "SIG", "line.ref": "GND"})


class RCFilter(System):
    """The filter, the requirement on its corner, and the question that
    measures it."""

    corner_spec = Requires(
        "The anti-aliasing filter's -3 dB corner lies between 1.5 kHz and 1.7 kHz",
        validation="simulation",
    )
    by_hand = Calculates(
        "f_c = 1 / (2 pi R C)",
        inputs=("r", "c"),
        result="1.59 kHz for 10 kOhm and 10 nF",
        requirements=("corner_spec",),
    )

    # No value: the program does not know it, and a number written here would
    # be a claim rather than a measurement.
    corner = Parameter("Hz", description="the -3 dB corner, as measured")

    source = SignalIn(package="PinHeader_1x02_P2.54mm")
    adc = AdcInput(package="PinHeader_1x02_P2.54mm")
    r = Resistor(resistance=10 * kOhm, package="R_0603")
    c = Capacitor(capacitance=10 * nF, package="C_0603")

    # The bench, in full: 1 V into the input, a sweep from 10 Hz to 1 MHz, and
    # the two connectors left out -- they carry the signal and do nothing to it.
    corner_check = Simulates(
        "corner_spec",
        measures={"corner": Crossing("adc.line", level=707.1 * mV, edge="falling")},
        supplies={"source.line": 1 * V},
        analysis=ACSweep(variation="dec", points=100, start="10", stop="1meg"),
        abstracted=("source", "adc"),
    )

    def architecture(self):
        self.source.line.signal >> self.r.p1
        self.r.p2 >> self.c.p1
        self.c.p2 >> self.source.line.ref
        self.adc.line.signal >> self.c.p1
        self.adc.line.ref >> self.c.p2

    def constraints(self):
        require(self.corner >= 1.5 * kHz)
        require(self.corner <= 1.7 * kHz)

The files it writes

The parts, then the nets and the pads on them.

C1     10 nF            Package:C_0603
J1     AdcInput         Package:PinHeader_1x02_P2.54mm
J2     SignalIn         Package:PinHeader_1x02_P2.54mm
R1     10 kOhm          Package:R_0603
Net-(C1-Pad1)            C1.1 J1.SIG R1.2
Net-(C1-Pad2)            C1.2 J1.GND J2.SLEEVE
Net-(J2-PadTIP)          J2.TIP R1.1

Every check that ran, and every one left undecided.

UNDECIDED constraint: declared on BLK-42978eb8675a
UNDECIDED constraint: declared on BLK-42978eb8675a
2 checks, 0 failed, 2 undecided

What the elaborated graph contains, by entity kind.

    1  block
    1  calculation
    4  component
   10  connection
    2  constraint
    3  interface
    8  pin
    6  port
    1  requirement
    1  verification
   37  total
snapshot sha256:f00cdf8504de5fd30b9f7c48c7e47422dedc8143eb1948bb899831f732f1eb08

All of it, including the KiCad netlist, is in examples/rc_filter/out/. Rebuild it with:

fang build examples/rc_filter/rc_filter.py