Avy solver crashes SES about sby

[cliffordwolf]

Building avy with cmake -DCMAKE_BUILD_TYPE=Debug makes avy fail with assertions that reveal that in fact avy is very picky with regard to what AIGER files it accepts. YosysHQ/yosys@779ce35 is a first towards a set of Yosys features that allows us to create "avy compatible" AIGER files.

[cliffordwolf]

Even with write_aiger -L (and without -O) I was not able to get avy to process a trivial test case:

$ cat test.sv
module test(input a, output o_v);
	assign o_v = a || !a;
	always @(*) assert(o_v);
endmodule

$ yosys -p 'synth; delete -output;; write_aiger -L test.aig' test.sv

$ avy -v9 test.aig
AVY PARAMETERS
	fName = test.aig
	ipt = 0
	avy = 1
	stutter = 0
	reset-cover = 0
	shallow_push = 0
	min-core = 0
	abstraction = 0
	tr0 = 0
	pdr = 100000
	min-suffix = 0
	sat1 = 0
	minisat = 0
	glucose = 1
	minisat_itp = 0
	glucose_itp = 1
	sat_simp = 1
	itp_simp = 0
	proof_reorder = 0
	gen-conf-limit = 0
	kstep = 1
	stick-error = 0
	itp-simplify = 1
	max-frame = 100000
END
Starting ABC
	Reading AIG from 'test.aig'
Found 0 (0) equiv and 1 constans out of 1
Found output driven by intput: 0


************** BRUNCH STATS ***************** 
BRUNCH_STAT run.loop 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
Assumption size: 1 core size: 1
UNSAT from BMC at frame: 0
itp             : pi =     1  po =     1  and =       0  lev =   0
itp             : pi =     1  po =     1  and =       0  lev =   0


************** BRUNCH STATS ***************** 
BRUNCH_STAT Depth 0
BRUNCH_STAT Frame 1
BRUNCH_STAT OrigItp 0
BRUNCH_STAT SimpItp 0
BRUNCH_STAT Aig_ManSimplifyComb 0.00
BRUNCH_STAT Glucose_solve 0.00
BRUNCH_STAT doBmc 0.00
BRUNCH_STAT getCnfTr 0.00
BRUNCH_STAT getInterpolant 0.00
BRUNCH_STAT run.loop 0.00
BRUNCH_STAT solveWithCore 0.00
BRUNCH_STAT Result UNKNOWN
************** BRUNCH STATS END ***************** 
FINDING NEEDED CONSTRAINTS: CoNum: 1 EquivNum: 1
. Done
Validating ITP: CoNum: 1
.. Done
Building PDR trace
avy: /usr/local/src/extavy/abc/src/misc/vec/vecWec.h:144: abc::Vec_Int_t* abc::Vec_WecEntry(abc::Vec_Wec_t*, int): Assertion `i >= 0 && i < p->nSize' failed.
Aborted (core dumped)

I am now considering to simply drop support for AVY in SymbiYosys.

[tmeissner]

Hi. Are there any news with this? I assume avy is still broken?

I tried it (again) with an own test design and stumbled over another assertion than above that above (avy branch new-quic & built with Debug):

Test design: https://raw.githubusercontent.com/tmeissner/formal_hw_verification/master/fifo/fifo.vhd

First synthesize & write AIGER file:

yosys -m ghdl -p 'ghdl --std=08 -gFormal=true -gDepth=4 -gWidth=4 fifo.vhd -e fifo; synth -flatten; delete -output; async2sync; chformal -live -fair -cover -remove; dffunmap; abc -g AND -fast; write_aiger -L -zinit fifo.aig'

Then try avy:

$ avy --cex - -v 2 test.aig 
AVY PARAMETERS
        fName = test.aig
        ipt = 0
        avy = 1
        stutter = 0
        reset-cover = 0
        shallow_push = 0
        min-core = 0
        abstraction = 0
        tr0 = 0
        pdr = 100000
        min-suffix = 0
        sat1 = 0
        minisat = 0
        glucose = 1
        minisat_itp = 0
        glucose_itp = 1
        sat_simp = 1
        itp_simp = 0
        proof_reorder = 0
        gen-conf-limit = 0
        kstep = 1
        stick-error = 0
        itp-simplify = 1
        max-frame = 100000
        min-core-muser = 0
        incr = 0
END
Starting ABC
        Reading AIG from 'test.aig'
Warning: The last 2 outputs are interpreted as constraints.
Error:/root/extavy/avy/src/SafetyVC2.cc:18: Assertion: Saig_ManPoNum(pCircuit) - Saig_ManConstrNum(pCircuit) == 1
Aborted (core dumped)