Skip to content

equiv_* doesn't respect $assume #5196

@widlarizer

Description

@widlarizer

Version

main

On which OS did this happen?

Linux

Reproduction Steps

Originally analyzed by @KrystalDelusion

read_verilog -sv <<EOT
module gold (input D, output Q);
assign Q = '0;
endmodule

module gate (input D, output Q);
assume property (D == '0);
assign Q = D;
endmodule
EOT

stat gate
chformal -lower
stat gate
async2sync

equiv_make gold gate equiv
#opt_clean -purge equiv
#show equiv
equiv_simple equiv
#equiv_induct equiv
equiv_status -assert equiv

Image

Expected Behavior

Equivalence proven

Actual Behavior

Equivalence unproven. This is surprising since equiv_* passes use SatGen infrastructure which should construct the corresponding operations for ezsat

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugpending-verificationThis issue is pending verification and/or reproduction

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions