Open ZipCPU opened 4 years ago
cliffordwolf
commented
4 years ago 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. https://github.com/YosysHQ/yosys/commit/779ce3537fa921daf6ffd780264f0867a8ebc4be is a first towards a set of Yosys features that allows us to create "avy compatible" AIGER files.
cliffordwolf
commented
4 years ago 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
commented
2 years ago 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)
Consider the following MCVE:
A simple inspection should assure us that this design will pass.
However, when using the SBY file:
When using the 20190416A build of the SymbioticEDA Suite (and I think more recent as well, this is only the one I've got installed), I'm getting the following error when using AVY:
Expected behavior
This design should simply PASS.
Dan