Hardware Reference
In-Depth Information
extract_aut planets.aut
echo "Solving the equation using the standard script ... "
determinize -ci planets.aut spec_dci.aut
support v0,v1,v2,v3,v4,v5,v6,v11,v12,v7,v8,v9,v10,v13.6,v13.7,
v13.8,v13.9,v13.10,v13.11,v13.12,v13.13,v13.14,v13.15,v13.16,
v13.17,v13.18,v13.19,v13.20,v13.21,v13.22,v13.23,v13.24
spec_dci.aut
suppsi.aut
support v0,v1,v2,v3,v4,v5,v6,v11,v12,v7,v8,v9,v10,v13.6,v13.7,
v13.8,v13.9,v13.10,v13.11,v13.12,v13.13,v13.14,v13.15,v13.16,
v13.17,v13.18,v13.19,v13.20,v13.21,v13.22,v13.23,v13.24
planetf.aut
suppf.aut
product suppf.aut suppsi.aut p.aut
support v0,v1,v2,v3,v4,v5,v6,v11,v12,v7,v8,v9,v10
p.aut p_supp.aut
determinize -ci p_supp.aut p_dci.aut
progressive -i 9 p_dci.aut planetxl.aut
print_stats_aut planetxl.aut
The following script
planetLC.script
verifies that the product of the
solution
planetxl.aut
and of the context
planetf.aut
is contained in the
specification
planets.aut
.
echo "Verifying the (partitioned) composition in the spec ... "
support v0,v1,v2,v3,v4,v5,v6,v11,v12,v7,v8,v9,v10,v13.6,v13.7,
v13.8,v13.9,v13.10,v13.11,v13.12,v13.13,v13.14,v13.15,v13.16,
v13.17,v13.18,v13.19,v13.20,v13.21,v13.22,v13.23,v13.24
planetxs.aut
suppx.aut
read_blif planetf.blif
latch_expose
extract_aut planetf.aut
support v0,v1,v2,v3,v4,v5,v6,v11,v12,v7,v8,v9,v10,v13.6,v13.7,
v13.8,v13.9,v13.10,v13.11,v13.12,v13.13,v13.14,v13.15,v13.16,
v13.17,v13.18,v13.19,v13.20,v13.21,v13.22,v13.23,v13.24
planetf.aut
suppf.aut
product suppx.aut suppf.aut prod.aut
support v0,v1,v2,v3,v4,v5,v6,v13.6,v13.7,v13.8,v13.9,v13.10,
v13.11,
v13.12,v13.13,v13.14,v13.15,v13.16,v13.17,v13.18,v13.19,
v13.20,
v13.21,v13.22,v13.23,v13.24 prod.aut prod.aut
determinize prod.aut prod.aut
read_blif planet.blif
extract_aut planets.aut
support v0,v1,v2,v3,v4,v5,v6,v13.6,v13.7,v13.8,v13.9,v13.10,
v13.11,
v13.12,v13.13,v13.14,v13.15,v13.16,v13.17,v13.18,v13.19,v13.20,
v13.21,v13.22,v13.23,v13.24 planets.aut supps.aut
contain prod.aut supps.aut
Search WWH ::
Custom Search