Convert the Boolean equations synthesised from STGs into Digital Circuits
Parse synthesis output of Petrify and MPSat tools and create a Digital Circuits for the Boolean equations. Note there may be several solutions proposed by the synthesis tools, the easiest option is to generate a separate circuit for each solution.
Blueprint information
- Status:
- Complete
- Approver:
- Danil Sokolov
- Priority:
- Medium
- Drafter:
- Danil Sokolov
- Direction:
- Needs approval
- Assignee:
- None
- Definition:
- Obsolete
- Series goal:
- None
- Implementation:
-
Not started
- Milestone target:
- None
- Started by
- Completed by
- Danil Sokolov
Related branches
Related bugs
Sprints
Whiteboard
Example outputs for C-element synthesis
# Petrify complex gate synthesis:
#######
-------
| Input -> Input Delays: |
-------
Average delay = 1.00 events
Worst-case delay = 1.00 events
Input events with worst-case delay: a+ a- b+ b-
> Input events preceding a+: a-(1) b-(1)
> Input events preceding a-: a+(1) b+(1)
> Input events preceding b+: a-(1) b-(1)
> Input events preceding b-: a+(1) b+(1)
=======
# Gates for signal x #
=======
x' = b' (a' + x') + x' a'
[x] = x' (output inverter)
> triggers(SET): (a-,b-) -> x-
> triggers(RESET): (a+,b+) -> x+
> 10 transistors (5 n, 5 p) + 1 inverters
> Estimated delay: rising = 25.46, falling = 26.83
> Speed independent (no timing assumptions)
x = b (a + x) + x a
> triggers(SET): (a+,b+) -> x+
> triggers(RESET): (a-,b-) -> x-
> 10 transistors (5 n, 5 p) + 3 inverters
> Estimated delay: rising = 41.00, falling = 31.29
> Speed independent (no timing assumptions)
=======
| Selected circuit |
=======
x' = b' (a' + x') + x' a'
[x] = x' (output inverter)
> triggers(SET): (a-,b-) -> x-
> triggers(RESET): (a+,b+) -> x+
> 10 transistors (5 n, 5 p) + 1 inverters
> Estimated delay: rising = 25.46, falling = 26.83
# EQN file for model /tmp/STG3756291
# Generated by petrify 4.2 (compiled 15-Oct-03 at 3:06 PM)
# Outputs between brackets "[out]" indicate a feedback to input "out"
# Estimated area = 5.00
INORDER = a b x;
OUTORDER = [x];
[x] = b (a + x) + a x;
# No set/reset pins required.
# Petrify generalised C-element synthesis:
#######
-------
| Input -> Input Delays: |
-------
Average delay = 1.00 events
Worst-case delay = 1.00 events
Input events with worst-case delay: a+ a- b+ b-
> Input events preceding a+: a-(1) b-(1)
> Input events preceding a-: a+(1) b+(1)
> Input events preceding b+: a-(1) b-(1)
> Input events preceding b-: a+(1) b+(1)
=======
# Gates for signal x #
=======
SET(x') = a' b'
RESET(x') = a b
[x] = x' (output inverter)
> triggers(SET): (a-,b-) -> x-
> triggers(RESET): (a+,b+) -> x+
> 4 transistors (2 n, 2 p) + 1 inverters
> Estimated delay: rising = 23.96, falling = 24.12
> Speed independent (no timing assumptions)
=======
| Selected circuit |
=======
SET(x') = a' b'
RESET(x') = a b
[x] = x' (output inverter)
> triggers(SET): (a-,b-) -> x-
> triggers(RESET): (a+,b+) -> x+
> 4 transistors (2 n, 2 p) + 1 inverters
> Estimated delay: rising = 23.96, falling = 24.12
# EQN file for model /tmp/STG2705798
# Generated by petrify 4.2 (compiled 15-Oct-03 at 3:06 PM)
# Outputs between brackets "[out]" indicate a feedback to input "out"
# Estimated area = 9.00
INORDER = a b x;
OUTORDER = [x];
[0] = a b;
[1] = a' b';
[x] = [1]' ([0] + x) + x [0]; # mappable onto gC
# No set/reset pins required.
## MPSat complex gate synthesis
#######
file: /tmp/unfolding1
Unfolding statistics: |B|=10 |E|=6 |C|=1 |BE|=8 |EB|=8
The net is (dynamically) conflict-free: optimized method is used.
SOLUTION 1:
Signal x (cost 5)
Triggers (underapproxima
Context: x
Equation (5 lits): x (b + a) + a b
Equations derived (literals=5)
Original Num Var/Cl/Lit 7/18/46
SAT/Total time: 0.00/0.00
Work Items
Work items:
Parser for Petrify synthesis output: TODO
Parser for MPSat synthesis output: TODO
