riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #2995 from georgerennie/cover_precond 

chformal: Add -coverenable option
This commit is contained in:
Jannis Harder 2023-02-14 17:46:31 +01:00 committed by GitHub
parent 85f611fb23 b636af9751
commit ec94703619
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 44 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
passes/cmds/chformal.cc
View File

@ -55,6 +55,14 @@ struct ChformalPass : public Pass {
log(" -skip <N>\n");
log(" ignore activation of the constraint in the first <N> clock cycles\n");
log("\n");
log(" -coverenable\n");
log(" add cover statements for the enable signals of the constraints\n");
log("\n");
#ifdef YOSYS_ENABLE_VERIFIC
log(" Note: For the Verific frontend it is currently not guaranteed that a\n");
log(" reachable SVA statement corresponds to an active enable signal.\n");
log("\n");
#endif
log(" -assert2assume\n");
log(" -assume2assert\n");
log(" -live2fair\n");
@ -114,6 +122,10 @@ struct ChformalPass : public Pass {
mode_arg = atoi(args[++argidx].c_str());
continue;
}
if (mode == 0 && args[argidx] == "-coverenable") {
mode = 'p';
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
assert2assume = true;
mode = 'c';
@ -263,6 +275,13 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN)));
}
else
if (mode =='p')
{
for (auto cell : constr_cells)
module->addCover(NEW_ID_SUFFIX("coverenable"),
cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
}
else
if (mode == 'c')
{
for (auto cell : constr_cells)

25
tests/various/chformal_coverenable.ys Normal file
View File

@ -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 -coverenable
select -assert-count 2 t:$cover
chformal -assert -coverenable
select -assert-count 4 t:$cover
chformal -assume -coverenable
select -assert-count 5 t:$cover