Summary
This issue describes a proposal for the description language defining inter-circuit connections.
The language should be used to connect 2 or more "primitive" sub-circuits to build a circuit again.
The "primitive" circuit description language
Currently the cbmc-gc compiler is used to create a circuit (consisting of AND, XOR, OR and NOT gates). The compiler take (specially prepared) C code and creates the following files:
- output.constants.txt
- output.gate.txt
- output.inputs.partyA.txt
- output.inputs.partyB.txt
- output.inputs.txt
- output.mapping.txt
- output.noob.txt
- output.numberofgates.txt
The format of the files can be found at cbmc-gc doc.
The circuit description
Basically the connection of two gates looks like this:
'GATE_ID' 'GATE_TYPE' 'NUM_OF_PINS' 'WIRE(S)'
For example: 1 AND 2 0:2:0 0:3:1
The 'GATE_ID' isn't defined explicitly, but inferred form the line number - so if you find something like
AND 2 0:2:0 0:3:1
in line 1 of your output.gate.txt, this means: This is a AND-gate with the gate id 1 (because it is in line 1) and 2 wires to pin 0 of gate 2 and pin 1 of gate 3.
Now how can we connect gates of one circuit to the IOPins of another circuit?
The idea of this proposal is this:
Take the general gate description 'GATE_ID' 'GATE_TYPE' 'NUM_OF_PINS' 'WIRE(S)'
and
add a circuit identifier to the gate id of the wire.
A 'WIRE' consist of 'SRC_PIN':'DST_GATE_ID':'DST_PIN' - e.g. 0:2:0
Now we can add circuit identifier - e.g. x (not verify expressive but we can pick better names later) to the 'DST_GATE_ID'.
This looks something like: 0:x.2:0
which means: connect the output pin of the current gate with the input pin 2 of the circuit referred as x.
But how do we refer circuits?
Therefore we use a new file output.circuits.txt which contains the circuit-to-identifier bindings.
This file can contains entires following this pattern:
An 'IDENTIFIER' is a string starting with a letter (a-z,A-Z) and than can consists of (a-z,A-Z,0-9,_).
A 'LINK' is just a file link to the folder containing a circuit (a folder containing output.*.txt files).
The same 'IDENTIFIER' must not appear multiply times in one output.circuits.txt file.
An example for this file:
x=/home/john/Desktop/sum_int32
But how can we feed the output of a sub-circuit back into our current circuit?
This is quite a bit more difficult. Hopefully this can be figured out within the following discussion:
One approach could be to introduce a new gate type accepting output wires of a sub-circuit, but this would change the gate-to-wire semantic.
A different approach could be to define the "sub-circuit output to circuit gate" relationships in a separate file.