diff options
| author | Jannis Harder <me@jix.one> | 2022-05-31 17:47:07 +0200 |
|---|---|---|
| committer | George Rennie <georgerennie@gmail.com> | 2022-06-18 18:19:26 +0100 |
| commit | e39c422734219bb0601827cb7c1d081f7ac7817b (patch) | |
| tree | 6ddf17cbfe324654ea51f9127b3988edc326c5e2 | |
| parent | c659bd18786633c52d42b5966627d39d99ae89e3 (diff) | |
| download | yosys-e39c422734219bb0601827cb7c1d081f7ac7817b.tar.gz yosys-e39c422734219bb0601827cb7c1d081f7ac7817b.tar.bz2 yosys-e39c422734219bb0601827cb7c1d081f7ac7817b.zip | |
chformal: Test -coverprecond and reuse the src attribute
| -rw-r--r-- | passes/cmds/chformal.cc | 4 | ||||
| -rw-r--r-- | tests/various/chformal_coverprecond.ys | 25 |
2 files changed, 27 insertions, 2 deletions
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index 0131063b3..c4666f1f0 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -273,8 +273,8 @@ struct ChformalPass : public Pass { if (mode =='p') { for (auto cell : constr_cells) - module->addCover(NEW_ID, cell->getPort(ID::EN), State::S1, - "$auto$coverprecond$" + cell->get_src_attribute()); + module->addCover(NEW_ID_SUFFIX("coverprecond"), + cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); } else if (mode == 'c') diff --git a/tests/various/chformal_coverprecond.ys b/tests/various/chformal_coverprecond.ys new file mode 100644 index 000000000..59e302a72 --- /dev/null +++ b/tests/various/chformal_coverprecond.ys @@ -0,0 +1,25 @@ +read_verilog -formal <<EOT +module top(input a, b, c, d); + + always @* begin + if (a) assert (b == c); + if (!a) assert (b != c); + if (b) assume (c); + if (c) cover (d); + end + +endmodule +EOT + +prep -top top + +select -assert-count 1 t:$cover + +chformal -cover -coverprecond +select -assert-count 2 t:$cover + +chformal -assert -coverprecond +select -assert-count 4 t:$cover + +chformal -assume -coverprecond +select -assert-count 5 t:$cover |