diff options
| author | Clifford Wolf <clifford@clifford.at> | 2019-06-19 10:50:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-19 10:50:32 +0200 |
| commit | eb3b9fb24ac6547caa5d4063e61be600fc0d55f5 (patch) | |
| tree | ffb26ba622ba97a52865bdb47002663a23d88df2 | |
| parent | 64947453e22404e570d670416ad66511a799e666 (diff) | |
| parent | addf01d45dd795b4fe711012facbe43dd7c2eae7 (diff) | |
| download | yosys-eb3b9fb24ac6547caa5d4063e61be600fc0d55f5.tar.gz yosys-eb3b9fb24ac6547caa5d4063e61be600fc0d55f5.tar.bz2 yosys-eb3b9fb24ac6547caa5d4063e61be600fc0d55f5.zip | |
Merge pull request #1104 from whitequark/case-semantics
Clarify switch/case semantics in RTLIL
| -rw-r--r-- | kernel/rtlil.cc | 29 | ||||
| -rw-r--r-- | manual/CHAPTER_Overview.tex | 12 |
2 files changed, 40 insertions, 1 deletions
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 790ba52a3..a09f4a0d1 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1381,7 +1381,34 @@ void RTLIL::Module::check() for (auto &it : processes) { log_assert(it.first == it.second->name); log_assert(!it.first.empty()); - // FIXME: More checks here.. + log_assert(it.second->root_case.compare.empty()); + std::vector<CaseRule*> all_cases = {&it.second->root_case}; + for (size_t i = 0; i < all_cases.size(); i++) { + for (auto &switch_it : all_cases[i]->switches) { + for (auto &case_it : switch_it->cases) { + for (auto &compare_it : case_it->compare) { + log_assert(switch_it->signal.size() == compare_it.size()); + } + all_cases.push_back(case_it); + } + } + } + for (auto &sync_it : it.second->syncs) { + switch (sync_it->type) { + case SyncType::ST0: + case SyncType::ST1: + case SyncType::STp: + case SyncType::STn: + case SyncType::STe: + log_assert(!sync_it->signal.empty()); + break; + case SyncType::STa: + case SyncType::STg: + case SyncType::STi: + log_assert(sync_it->signal.empty()); + break; + } + } } for (auto &it : connections_) { diff --git a/manual/CHAPTER_Overview.tex b/manual/CHAPTER_Overview.tex index 2feb0f1cb..1a25c477f 100644 --- a/manual/CHAPTER_Overview.tex +++ b/manual/CHAPTER_Overview.tex @@ -350,6 +350,18 @@ and this bit is a one (the second ``1'').} for {\tt \textbackslash{}reset == 1} sets {\tt \$0\textbackslash{}q[0:0]} to the value of {\tt \textbackslash{}d} if {\tt \textbackslash{}enable} is active (lines $6 \dots 11$). +A case can specify zero or more compare values that will determine whether it matches. Each of the compare values +must be the exact same width as the control signal. When more than one compare value is specified, the case matches +if any of them matches the control signal; when zero compare values are specified, the case always matches (i.e. +it is the default case). + +A switch prioritizes cases from first to last: multiple cases can match, but only the first matched case becomes +active. This normally synthesizes to a priority encoder. The {\tt parallel\_case} attribute allows passes to assume +that no more than one case will match, and {\tt full\_case} attribute allows passes to assume that exactly one +case will match; if these invariants are ever dynamically violated, the behavior is undefined. These attributes +are useful when an invariant invisible to the synthesizer causes the control signal to never take certain +bit patterns. + The lines $13 \dots 16$ then cause {\tt \textbackslash{}q} to be updated whenever there is a positive clock edge on {\tt \textbackslash{}clock} or {\tt \textbackslash{}reset}. |