Skip to content

Example 2. SignalFlow

Jump to bottom
Xinran Liu edited this page Jul 9, 2021 · 28 revisions

So far we have demonstrated the declarations of data constructors, conformance constraints, model assertions and aliases in the first example. Now let’s move on and talk a bit about rules and querying models in this signal flow domain:

domain SignalFlow
{

  Parameter ::= new (name: String, id: String, dataType: String, initValue: String, size: Integer).
  ParamFlow ::= new (name: String, id: String, src: Parameter, dst: Parameter).

  Processing ::= Primitive + Compound.
  Primitive  ::= new (name: String, id: String, function: String).
  Compound   ::= new (name: String, id: String).
  ProcessingParent ::= new (child: Processing, parent: Compound).

  Port   ::= Input + Output.
  Input  ::= new (name: String, id: String, parent: Processing).
  Output ::= new (name: String, id: String, parent: Processing).

  // Flows and their parents
  Flow ::= new (id: String, src: Port, dst: Port).
  FlowParent ::= new (child: Flow, parent: Compound).

  // Hardware
  HardwareModel ::= new (name: String, id: String).
  HWNode ::= new (name: String, id: String).

  // Hardware connections
  HWConn ::= new (id: String, src: HWNode, dst: HWNode).
  ProcessingConn ::= new (id: String, src: Processing, dst: HWNode).

  badFlow ::= (flow: Flow).

  // A constraint to check if a Flow is legal
  // A flow can only go between ports whose "grandparents" are the same element or with only one level's gap
  // 1. Find a Flow
  // 2. Find the src of the Flow and dst of the Flow
  // 3. Get the parent of the parent of the src
  // 4. Get the parent of the parent of the dst
  // 5. Check that those two elements are the same or with only one level's gap
  badFlow(f) :- f is Flow,
			src = f.src, dst = f.dst,
			p1 = src.parent, p2 = dst.parent,
			ProcessingParent(p1, com1),
			ProcessingParent(p2, com2),
			com1 != com2,
			no ProcessingParent(com1, com2),
			no ProcessingParent(com2, com1).

   conforms no badFlow(f).
}

In a signal flow, we have primitive processes and compound processes. Primitive processes can implement elementary computations and compound processes can contain signals, primitives and/or other compound processes. “Bad flows” are the ones that skipped more than one level in the signal flow hierarchy and we should be avoiding them. To deal with this conditional statement, we write powerful domain constraints by the computed properties, which we call rules. A basic rule has the following syntax:

 head :- body.

The body part can contain anything a query can contain. The head part is a sequence of constructor applications applied to constants and variables. A rule means: “Whenever the body is provable for some variable assignment, then the head is also provable for that variable assignment.” Thus, a rule is a logical statement, but it can also be executed (like a query) to grow the set of provable values. So if the parents of the parents of the input and output are not the same or parent-child relation, then they must be bad flows with at least two level gap in the signal flow hierarchy.

model FMRadio of SignalFlow
{


 //Primitives and Compounds
 receiver is Compound("FM Receiver", "/00000").

 speakers is Primitive("Speakers", "/00000/00000", "CollectAudio").
 primitive is Primitive("Primitive", "/00000/00001", "Unknown").
 localOscillator is Primitive("Local Oscllator", "/00000/00002", "Oscllator").
 lowPassFilter is Primitive("LowPass Filter", "/00000/00003", "Filter").
 gain is Primitive("Gain", "/00000/00004", "Unknown").
 usrp is Primitive("USRP Source", "/00000/00005", "Source").


 mixer is Compound("Mixer", "/00000/00006").
 squelch is Compound("Squelch", "/00000/00007").
 display is Compound("FFT Dispaly", "/00000/00008").
 demod is Compound("WBFM Demod", "/00000/00009").

 threshold is Primitive("Threshold", "/00000/00007/00000", "Threshold").
 placeHolder is Primitive("PlaceHolder", "/00000/00009/00000", "PlaceHolder").
 multiply is Primitive("Multiply", "/00000/00006/00000", "Multiply").





  //Parent-child relations.
  ProcessingParent(speakers, receiver).
  ProcessingParent(primitive, receiver).
  ProcessingParent(localOscillator, receiver).
  ProcessingParent(lowPassFilter, receiver).
  ProcessingParent(gain, receiver).
  ProcessingParent(usrp, receiver).

  ProcessingParent(mixer, receiver).
  ProcessingParent(squelch, receiver).
  ProcessingParent(display, receiver).
  ProcessingParent(demod, receiver).


  ProcessingParent(threshold, squelch).
  ProcessingParent(placeHolder, demod).
  ProcessingParent(multiply, mixer).



  //An input in Primitive
  input is Input("Input", "/00000/00001/00000", primitive).




  // A flow from an output in Primitve to an input in Speakers
  output is Output("Output", "/00000/00001/00001", primitive).
  audio0 is Input("Audio", "/00000/00000/00000", speakers).

  f0 is Flow("/00000/00010", output, audio0).




  // A flow from an output in Gain to an input in Speakers
  out0 is Output("Out", "/00000/00004/00000", gain).

  f1 is Flow("/00000/00011", out0, audio0).




  // A flow from an output in WBFM Demod to an input in Gain
  audio1 is Output("Audio", "/00000/00009/00000", demod).
  in0 is Input("In", "/00000/00004/00001", gain).

  f2 is Flow("/00000/00012", audio1, in0).




  // A flow from an output in Squelch to an input in WBFM Demod
  out1 is Output("Out", "/00000/00007/00000", squelch).
  if0 is Input("IF", "/00000/00009/00001", demod).

  f3 is Flow("/00000/00013", out1, if0).




  // A flow from an output in LowPass Filter to an input in Squelch
  out2 is Output("Out", "/00000/00003/00000", lowPassFilter).
  in1 is Input("In", "/00000/00007/00001", squelch).

  f4 is Flow("/00000/00014", out2, in1).




  // A flow from an output in LowPass Filter to an input in FFT Display
  ch2 is Input("Ch2", "/00000/00008/00000", display).

  f5 is Flow("/00000/00015", out2, ch2).




  // A flow from an output in Mixer to an input in LowPass Filter
  if1 is Output("IF", "/00000/00006/00000", mixer).
  in2 is Input("In", "/00000/00003/00001", lowPassFilter).

  f6 is Flow("/00000/00016", if1, in2).




  // A flow from an output in USRP Source to an input in Mixer
  bb is Output("BB", "/00000/00005/00000", usrp).
  rf is Input("RF", "/00000/00006/00001", mixer).

  f7 is Flow("/00000/00017", bb, rf).




  // A flow from an output in USRP Source to an input in FFT Display
  ch1 is Input("Ch1", "/00000/00008/00001", display).

  f8 is Flow("/00000/00018", bb, ch1).




  // A flow from an output in Local Oscillator to an input in Mixer
  lo0 is Output("LO", "/00000/00002/00000", localOscillator).
  lo1 is Input("LO", "/00000/00006/00002", mixer).

  f9 is Flow("/00000/00019", lo0, lo1).




  // Flows inside Squelch
  in3 is Input("In", "/00000/00007/00000/00000", threshold).
  out3 is Output("Out", "/00000/00007/00000/00001", threshold).

  f10 is Flow("/00000/00007/00010", in1, in3).
  f11 is Flow("/00000/00007/00011", out3, out1).




  // Flows inside Mixer
  a is Input("a", "/00000/00006/00000/00000", multiply).
  b is Input("b", "/00000/00006/00000/00001", multiply).
  y is Output("y", "/00000/00006/00000/00002", multiply).

  f12 is Flow("/00000/00006/00010", rf, a).
  f13 is Flow("/00000/00006/00011", lo1, b).
  f14 is Flow("/00000/00006/00012", y, if1).




  // Flows inside WBFM Demod
  in4 is Input("In", "/00000/00009/00000/00000", placeHolder).
  out4 is Output("Out", "/00000/00009/00000/00001", placeHolder).

  f15 is Flow("/00000/00009/00010", if0, in4).
  f16 is Flow("/00000/00009/00011", out4, audio1).



  //Parents of flows
  FlowParent(f0, receiver).
  FlowParent(f1, receiver).
  FlowParent(f2, receiver).
  FlowParent(f3, receiver).
  FlowParent(f4, receiver).
  FlowParent(f5, receiver).
  FlowParent(f6, receiver).
  FlowParent(f7, receiver).
  FlowParent(f8, receiver).
  FlowParent(f9, receiver).
  FlowParent(f10, squelch).
  FlowParent(f11, squelch).
  FlowParent(f12, mixer).
  FlowParent(f13, mixer).
  FlowParent(f14, mixer).
  FlowParent(f15, demod).
  FlowParent(f16, demod).




  //Parameters
  ifFreq0 is Parameter("IFFreq", "/00000/00020", "Integer", "0", 1).
  ifFreq1 is Parameter("IF Frequency", "/00000/00002/00020", "Integer", "0", 1).

  samplingRate0 is Parameter("SamplingRate", "/00000/00021", "Integer", "0", 1).
  samplingRate1 is Parameter("SamplingRate", "/00000/00002/00021", "Integer", "0", 1).
  samplingRate2 is Parameter("SamplingRate", "/00000/00008/00020", "Integer", "0", 1).
  samplingRate3 is Parameter("SamplingRate", "/00000/00005/00020", "Integer", "0", 1).

  centeFreq0 is Parameter("CenterFreq", "/00000/00022", "Integer", "0", 1).
  centeFreq1 is Parameter("CenterFreq", "/00000/00005/00021", "Integer", "0", 1).

  rxGain0 is Parameter("RxGain", "/00000/00023", "Integer", "0", 1).
  rxGain1 is Parameter("RxGain", "/00000/00005/00022", "Integer", "0", 1).

  cutOff0 is Parameter("CutOff", "/00000/00024", "Integer", "0", 1).
  cutOff1 is Parameter("CutOff", "/00000/00003/00000", "Integer", "0", 1).

  audioRate0 is Parameter("AudioRate", "/00000/00025", "Integer", "0", 1).
  audioRate1 is Parameter("AudioRate", "/00000/00000/00020", "Integer", "0", 1).
  audioRate2 is Parameter("AudioRate", "/00000/00009/00020", "Integer", "0", 1).

  moduletionIndex0 is Parameter("ModuletionIndex", "/00000/00026", "Integer", "0", 1).
  moduletionIndex1 is Parameter("ModuletionIndex", "/00000/00009/00021", "Integer", "0", 1).

  gain0 is Parameter("Gain", "/00000/00027", "Integer", "0", 1).
  gain1 is Parameter("Gain", "/00000/00004/00020", "Integer", "0", 1).

  sqLevel is Parameter("SQLevel", "/00000/00028", "Integer", "0", 1).
  level0 is Parameter("Level", "/00000/00007/00020", "Integer", "0", 1).
  level1 is Parameter("Level", "/00000/00007/00000/000020", "Integer", "0", 1).




  //Parameter Flows
  ParamFlow("Level", "00000/00007/00030", level0, level1).

  ParamFlow("IFFreq", "00000/00030", ifFreq0, ifFreq1).

  ParamFlow("SamplingRate", "00000/00031", samplingRate0, samplingRate1).
  ParamFlow("SamplingRate", "00000/00032", samplingRate0, samplingRate2).
  ParamFlow("SamplingRate", "00000/00033", samplingRate0, samplingRate3).

  ParamFlow("CenterFreq", "00000/00034", centeFreq0, centeFreq1).

  ParamFlow("RxGain", "00000/00035", rxGain0, rxGain1).

  ParamFlow("CutOff", "00000/00036", cutOff0, cutOff1).

  ParamFlow("AudioRate", "00000/00037", audioRate0, audioRate1). 
  ParamFlow("AudioRate", "00000/00038", audioRate0, audioRate2).

  ParamFlow("ModulationIndex", "00000/00039", moduletionIndex0, moduletionIndex1).

  ParamFlow("Gain", "00000/00040", gain0, gain1).

  ParamFlow("Level", "00000/00041", sqLevel, level0).

 }

To understand how a model contains a set of assertions, create a file called SignalFlow.4ml and copy the code in this example. A query operation tests if a property is provable on a model. Follow these steps to test if this model contains a Compound “Mixer”:

 []> load SignalFlow.4ml


 []> query FMRadio Compound("Mixer", _)


 []> ls tasks
Id Kind Status Result Started Duration
0 Query Done true 7/7/2021 10:34 PM 0.15s

The first command line loads and compiles the file SignalFlow.4ml. The second command line starts a query operation on the model FMRadio and tests for the property Compound("Mixer", _). If Compound("Mixer", _) is provable in FMRadio then this query operation returns true; otherwise it returns false. Starting a query spawns a new background task that may take some time to complete. The Id of the newly created task is reported (e.g. Id 0). Line 7 causes the status of all tasks to be displayed. Line 11 shows that the query completed with the result true.

Model conformance can also be checked using query operations. Run the following query to see the model FMRadio is conformed to its domain:

 []> query FMRadio SignalFlow.conforms
Id Kind Status Result Started Duration
1 Query Done true 7/7/2021 10:42 PM 0.12s

The result is true so FMRadio satisfies all the conformance constraints.

Clone this wiki locally