Unexpected gate in partition that causes FAIL checking result #76
Comments
|
I give a couple of details for this problem. module Design_000159 (
input in_6 ,
input in_7 ,
output out_11 ,
output out_15
);
wire one_16 ;
wire zero_17 ;
wire xor_18 ;
wire and_19 ;
wire xor_20 ;
wire xor_41 ;
assign one_16 = 1 ;
assign zero_17 = 0 ;
xor ( xor_18 , in_7 , one_16 );
and ( and_19 , in_7 , one_16 );
xor ( xor_20 , in_6 , zero_17 );
xor ( xor_41 , and_19 , xor_20 );
assign out_11 = xor_41 ;
assign out_15 = xor_18 ;
endmodule // Design_000159And here is the "gate" design named module Design_000159 (
input in_6 ,
input in_7 ,
output out_11 ,
output out_15
);
wire one_16 ;
wire zero_17 ;
wire and_18 ;
wire and_28 ;
wire and_29 ;
wire and_33 ;
assign one_16 = 1 ;
assign zero_17 = 0 ;
and ( and_18 , in_7 , one_16 );
and ( and_28 , in_6 , and_18 );
and ( and_29 , ~and_18 , ~in_6 );
and ( and_33 , ~and_28 , ~and_29 );
assign out_11 = and_33 ;
assign out_15 = ~in_7 ;
endmodule // Design_000159The scenario for EQY is as follows: The checking result is as follows: When I dive into the counterexample, I found that for gate design the After that, during equivalence checking, the It is impossible (see last "assign" in gate design). I've removed "prep" pass from *.eqy and equivalence checking returned "OK", but it looks that is some cases "opt_merge" pass may break the circuit in a non-equivalent way. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I have checked the equivalence between two Verilog descriptions
in1.vandin2.v.The checking result is "FAIL", but the generated counterexample contains inner gate
and_32(in gate design) that is not connected with primary outputout_11, while there isand_33gate that is an input forout_11(see partitioning result in *.json file). I wonder why there is such partition here? Are there any opportunities to construct the specific partitions in EQY?I've attached an archive with Verilog descriptions, JSON result of partitioning and EQY config too.
Thanks in advance!
eqy_fail.tar.gz
The text was updated successfully, but these errors were encountered: