diff options
| author | Clifford Wolf <clifford@clifford.at> | 2019-11-22 16:11:56 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2019-11-22 16:11:56 +0100 |
| commit | db323685a4357ae0a04a8def9de29ef3a8ba16c2 (patch) | |
| tree | 9f4ec5ae19c28ff6c54fa01fd464cce130acafe2 /frontends/verific/verificsva.cc | |
| parent | e93e4a7a2c6875e87b7e2635470cf02aa45af23a (diff) | |
| download | yosys-db323685a4357ae0a04a8def9de29ef3a8ba16c2.tar.gz yosys-db323685a4357ae0a04a8def9de29ef3a8ba16c2.tar.bz2 yosys-db323685a4357ae0a04a8def9de29ef3a8ba16c2.zip | |
Add Verific support for SVA nexttime properties
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verificsva.cc')
| -rw-r--r-- | frontends/verific/verificsva.cc | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 225fd3e4a..49c0c40ac 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -36,6 +36,8 @@ // basic_property: // sequence // not basic_property +// nexttime basic_property +// nexttime[N] basic_property // sequence #-# basic_property // sequence #=# basic_property // basic_property or basic_property (cover only) @@ -1264,6 +1266,26 @@ struct VerificSvaImporter return node; } + if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + log_assert(sva_low == sva_high); + + int node = start_node; + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + return parse_sequence(fsm, node, inst->GetInput()); + } + if (inst->Type() == PRIM_SVA_SEQ_CONCAT) { const char *sva_low_s = inst->GetAttValue("sva:low"); |