Refactor MPSat plugin
Currently MPSat plugin contains interface to MPSat for synthesis and verification. This creates a dependency loop between MpsatPlugin and CircuitPlugin. The former requires CircuitPlugin for synthesis, while the latter requires MpsatPlugin for verification. Also Punf and Pcomp interfaces are part of MpastPlugin and make it too heavy.
A solution is to split MpastPlugin into:
* MpsatSynthesisP
* MpsatVerificati
* PunfPlugin
* PcompPlugin
Blueprint information
- Status:
- Complete
- Approver:
- None
- Priority:
- Medium
- Drafter:
- Danil Sokolov
- Direction:
- Needs approval
- Assignee:
- Danil Sokolov
- Definition:
- Approved
- Series goal:
- None
- Implementation:
- Implemented
- Milestone target:
- 3.0.6
- Started by
- Danil Sokolov
- Completed by
- Danil Sokolov
Whiteboard
Work Items
Work items:
Extract MpsatVerificati
Extract MpsatSynthesisP
Extract PunfPlugin: DONE
Extract PcompPlugin: DONE
Extend Verilog parset for assign statements: DONE
Distinguish cg, gC and stdC assign statements: DONE
Tidy up circuit layout (self-loops and port alignment): DONE