mirror of https://github.com/YosysHQ/yosys.git
chformal: Test -coverprecond and reuse the src attribute
This commit is contained in:
parent
c659bd1878
commit
e39c422734
|
@ -273,8 +273,8 @@ struct ChformalPass : public Pass {
|
||||||
if (mode =='p')
|
if (mode =='p')
|
||||||
{
|
{
|
||||||
for (auto cell : constr_cells)
|
for (auto cell : constr_cells)
|
||||||
module->addCover(NEW_ID, cell->getPort(ID::EN), State::S1,
|
module->addCover(NEW_ID_SUFFIX("coverprecond"),
|
||||||
"$auto$coverprecond$" + cell->get_src_attribute());
|
cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
if (mode == 'c')
|
if (mode == 'c')
|
||||||
|
|
|
@ -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
|
Loading…
Reference in New Issue