Hardware Reference
In-Depth Information
the inputs and outputs of the file produced by this script,
planetxs.aut
,are:
Primary inputs: v0,v1,v2,v3,v4,v5,v6,v11,v12,v7,v8,v9,v10
Primary outputs: Acc
The first 7 inputs are the inputs
of the original
planet.blif
. The inputs
v11
and
v12
are the
u
variables coming from
i
F
, and the last 4 are the
v
variables
which are the outputs of
.
Acc
is the unique primary output of an automaton in
the
BLIF-MV
description to specify accepting states (see the format of automata in
Sect. 8.2).
Finally, we mentioned that the command
latch split
creates also three
more scripts; we will introduce them briefly and leave as an exercise their careful
examination.
The following script
planetSC.script
verifies that the product of the
solution
planetxs.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
The following script
planetL.script
solves the general language equation
F X S
X
. The result is in the file
planetxl.aut
.
# Language solving script (monolithic) generated by MVSIS
# for latch splitting of sequential network "planet.blif"
on Tue Jun 22 13:45:35 2010
# Command line was: "latch_split 0-3".
read_blif planetf.blif
latch_expose
extract_aut planetf.aut
read_blif planet.blif
Search WWH ::
Custom Search