search

lnis-uofu / LSOracle

IDEA project source files
MIT License
94 stars 42 forks source link

Problem about command "oracle" #74

Closed foggy-slt closed 2 years ago

foggy-slt commented 2 years ago

Hi I'm having a problem with the LSOracle.

This is my step： lsoracle> read_aig 0.aig lsoracle> oracle lsoracle> write_blif -m 0.blif

But I am using the "cec" of the tool "ABC", and the verificationis not equivalent.

abc 01> cec 0.aig 0.blif Networks are NOT EQUIVALENT. Time = 0.00 sec Verification failed for at least 8 outputs: output_47 output_50 output_53 ... Output output_47: Value in Network1 = 0. Value in Network2 = 1. Input pattern: input_45=0 input_46=0 input_44=0

I have tried other cases, and this situation will also occur. Upload a case below. Thanks! 0.zip

yashton commented 2 years ago

could you post your circuit?

foggy-slt commented 2 years ago

I uploaded a zip package named 0.zip in the first comment, you can unzip it and use it, thanks.

NormandAlexandre commented 2 years ago

Hi, We have updated the oracle command and it’s working now. My steps : lsoracle> read_aig 0.aig lsoracle> oracle lsoracle> write_blif -g 0.blif

Note that the oracle command writes a xmg by default. The two networks are equivalent.