[Experimental][export-smv] Introduce the export-smv tool #67
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
this is the inital commit for the export-smv tool, which converts a canonicalized handshake ir to a smv netlist and a library of dataflow unit written in smv
now support abstract operators and deciders.
this commit adds the smv description of dataflow units that are not parametrized. The implementation of the parametrized units will be generated on the fly.
…ic-mlir into experimental-export-smv
internal pipelines
Jiahui17
changed the title
lucas-rami
reviewed
Mar 11, 2024
| Operation *dst = oprd.getOwner(); | ||
|
|
||
| // Locate value in source results and destination operands | ||
| const size_t resIdx = findIndexInRange(src->getResults(), val); |
There was a problem hiding this comment.
If you are sure that val is the result of an operation you can just do
const size_t resIdx = cast<OpResult>(val).getResultNumber();|
|
||
| // Locate value in source results and destination operands | ||
| const size_t resIdx = findIndexInRange(src->getResults(), val); | ||
| const size_t argIdx = findIndexInRange(dst->getOperands(), val); |
There was a problem hiding this comment.
You can just do
const size_t argIdx = oprd.getOperandNumber();| StringRef unitName = getUniqueName(op); | ||
|
|
||
| os << "VAR " << unitName << " : "; | ||
| if (failed(getUnitType(op, os, timingDB))) { |
|
|
||
| for (auto [idx, arg] : llvm::enumerate(op->getOperands())) { | ||
| os << unitName << "_dataIn" << idx << ", " << unitName << "_pValid" << idx; | ||
| if (idx < op->getNumOperands() - 1) { |
|
|
||
| for (auto [idx, arg] : llvm::enumerate(op->getResults())) { | ||
| os << unitName << "_nReady" << idx; | ||
| if (idx < op->getNumResults() - 1) { |
| return success(); | ||
| } | ||
|
|
||
| LogicalResult getOperatorImpl(unsigned numInputs, unsigned lat, |
There was a problem hiding this comment.
None of the for's in this function need brackets
| os << "DEFINE valid0 := b" << slots - (transp) << ".valid0; \n"; | ||
| os << "DEFINE ready0 := b0.ready0; \n"; | ||
| if (transp) { | ||
| assert(std::size(data) == slots); |
There was a problem hiding this comment.
nit: we use the size() method on vectors across the repository instead of std::size
| assert(nOutputs >= 2 && "received a fork with 0 or 1 output ports!"); | ||
| // interface | ||
| os << "\nMODULE fork_1_" << nOutputs << "(dataIn0, pValid0, "; | ||
| for (unsigned i = 0; i < nOutputs - 1; i++) { |
| } | ||
| os << "nReady" << nOutputs - 1 << ")\n"; | ||
| os << "forkStop := "; | ||
| for (unsigned i = 0; i < nOutputs - 1; i++) { |
| "this file"), | ||
| cl::init("data/components.json"), cl::cat(mainCategory)); | ||
|
|
||
| static size_t findIndexInRange(ValueRange range, Value val) { |
There was a problem hiding this comment.
No longer needed after changes proposed below
…ic-mlir into experimental-export-smv
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces the export-smv tool, which converts a handshake-level IR to the nuXmv input format,
.smv(https://nuxmv.fbk.eu/).This allows us to run model-checking on an abstracted dataflow circuit model.
Example use:
{ exp-export-smv handshake_export.mlir --timing-models=data/components.json; cat data/components.smv } > model.smvPrepare the following nuXmv batch script,
commands.cmdAnd we can launch a verification run by using
nuXmv -int commands.cmdThe current implementation prints a netlist and a library of units in the SMV format to stdout.
Since this language does not support parametrized instantiation, we generate one implementation for each parametrization of a unit, e.g., it generates one implementation for 2-output, 3-output, and 4-output eager fork.