diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-03-03 16:34:28 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-03-03 16:34:28 +0100 |
| commit | 707ddb77bcb416399f7c61a2670731adbb97fc83 (patch) | |
| tree | 96cf4b8d730ff63e41cb6b890fe32787ff53d8db /frontends/verific/verificsva.cc | |
| parent | a44e1edaa302539fc1a53bf099c77b8085ed4d79 (diff) | |
| download | yosys-707ddb77bcb416399f7c61a2670731adbb97fc83.tar.gz yosys-707ddb77bcb416399f7c61a2670731adbb97fc83.tar.bz2 yosys-707ddb77bcb416399f7c61a2670731adbb97fc83.zip | |
Add SVA support for sequence OR
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verificsva.cc')
| -rw-r--r-- | frontends/verific/verificsva.cc | 55 |
1 files changed, 33 insertions, 22 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index fd464909f..05d5b6577 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -18,13 +18,36 @@ */ -// SVA Properties Simplified Syntax: +// Currently supported property styles: +// seq +// not seq +// seq |-> seq +// seq |-> not seq +// seq |-> seq until expr +// seq |-> seq until seq.triggered +// seq |-> not seq until expr +// seq |-> not seq until seq.triggered +// +// Currently supported sequence operators: +// expr ##[N:M] seq +// seq or seq +// expr throughout seq +// seq [*N:M] +// +// Notes: +// |-> is a placeholder for |-> and |=> +// "until" is a placeholder for all until operators +// ##[N:M], [*N:M], [=N:M], [->N:M] includes ##N, [*N], [=N], [->N] +// +// ------------------------------------------------------- +// +// SVA Properties Simplified Syntax (essentially a todo-list): // // prop: // not prop // prop or prop // prop and prop -// seq |=> prop +// seq |-> prop // if (expr) prop [else prop] // always prop // prop until prop @@ -45,26 +68,6 @@ // seq [*N:M] // expr [=N:M] // expr [->N:M] -// -// Notes: -// |=> is a placeholder for |-> and |=> -// "until" is a placeholder for all until operators -// ##[N:M], [*N:M], [=N:M], [->N:M] includes ##N, [*N], [=N], [->N] -// -// Currently supported property styles: -// seq -// not seq -// seq |=> seq -// seq |=> not seq -// seq |=> seq until expr -// seq |=> seq until seq.triggered -// seq |=> not seq until expr -// seq |=> not seq until seq.triggered -// -// Currently supported sequence operators: -// ##[N:M] -// [*N:M] -// throughout #include "kernel/yosys.h" @@ -844,6 +847,14 @@ struct VerificSvaImporter return node; } + if (inst->Type() == PRIM_SVA_SEQ_OR) + { + int node = parse_sequence(fsm, start_node, inst->GetInput1()); + int node2 = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm->createLink(node2, node); + return node; + } + if (inst->Type() == PRIM_SVA_THROUGHOUT) { log_assert(get_ast_input1(inst) == nullptr); |