Workspaces ---- apbd asves asvpapers bear blast caltrop cases concurrency cosi dif diva dopcenter dopresence dopsysadmin eecsx44 elab embedded embeddedadmin giotto hyinfo m2t2 mescal metropolis mica mobies msgadmin murieh mvsis nephest ransom recons robosysadmin savg sec seminar smartnets video webmaster

Next: Commands in VIS Up: No Title Previous: Formal Verification in Synthesis in VIS   VIS can interact with SIS in order to optimize the existing logic. There are two possible goals/scenarios: Synthesis for verification. Synthesis can be used to optimize the logic that represents the system, for simpler verification. Front-end to synthesis. Files described in Verilog and compiled into blif_mv (using VL2MV or another tool) can be synthesized by using VIS and SIS together. A key fact is that only the current level of the hierarchy is sent to SIS, and not the subtree rooted at the current node. Modules at a lower level are treated as external and the boundary variables are carefully preserved, by reintegrating their multi-valued status after the optimization step in SIS (SIS requires that boundary variables are completely encoded, i.e., are binary variables). Caveat To prevent that a signal (possibly referred to in a CTL property) is optimized away during synthesis, declare it as an output of a module. In the current version, only combinational logic is sent to SIS: latches are cut away from the module sent to SIS and they are reincorporated when the design is read back into VIS. Therefore we cannot take advantage of sequential optimizations in SIS, either at the level of a completely encoded sequential network or of a symbolic state table. The boundaries between modules are established when the initial hierarchy is described, and they are rigid in the sense that optimizations can never bridge them, but only operate within them. Notice that there is a way to replace a subtree of the hierarchy with another one by using read_blif_mv -r; this feature could be used to change boundaries in the original specification. Writing and Reading from SIS   VIS communicates with SIS via the write_blif and read_blif commands. Operations performed by write_blif are: All variables are encoded, i.e., values of multi-valued variables are replaced by binary vectors. For variables at the boundary with modules at different levels of the hierarchy the encoding assignments are stored into a file with extension .enc, so that it is possible to reintegrate the multi-valued boundaries between modules when coming back to VIS. All unspecified input combinations in the tables are specified by assigning zero code vectors as outputs. Default constructs in the specification of tables are handled appropriately. Nondeterministic tables are determinized by adding pseudo-inputs. As a result a file with extension .blif is created that can be read and optimized by SIS. SIS must be invoked outside of VIS by means of a different shell. All SIS operations to optimize combinational logic can be applied. In summary, write_blif scans all the tables of a given node in the hierarchy and encodes all symbolic variables, determinizes the tables by adding pseudo-inputs, and resolves incomplete specification by associating unspecified input combinations to outputs encoded by zero binary vectors. Operations performed by read_blif are: Restore the symbolic values of multi-valued I/O variables of the node being read in. This is done using the information in the file with extension .enc (e.g., read_blif -e model.enc s-sim.blif), which was written out during the write_blif process. Replace in the hierarchy the old node with the new node. Flow of Operations for Synthesis   The typical flow of operations of synthesis for verification is: read_blif_mv write_blif optimization by SIS read_blif init_verify suite of verification operations The typical flow of operations for direct synthesis is: read_blif_mv write_blif optimization by SIS read_blif It is possible to verify that after optimization with SIS the new global network (where the node returned from SIS is plugged back in the original network) is equivalent to the old global network, by using the command comb_verify that checks combinational equivalence of networks. Combinational equivalence can be checked at each level of the network hierarchy, from root to leaves. Before applying comb_verify, the command init_verify must be invoked. Example of Synthesis of Traffic Light Controller   The following script demonstrates the path from VIS to SIS and back. We have chosen to optimize the network of the leaf farm_control. We verify that the initial global network and the new network, after replacement of the network in the leaf farm_control by the one optimized by SIS, are combinationally equivalent. The script used to run SIS (in a different shell) is shown too. Experiments report big savings in literals for the optimized modules, since the BLIF-MV files generated by VL2MV have a lot of redundancy. UC Berkeley, VIS Release 1.0 (compiled 11-Dec-95 at 10:36 AM) vis> read_blif_mv tlc.mv Warning: Some variables are unused in model main. vis> init_verify vis> ls hwy_control sensor timer farm_control vis> print_network_stats main combinational=142 pi=0 po=0 latches=4 pseudo=2 const=40 edges=206 vis> cd farm_control vis> write_blif farm_control.blif Writing encoding information to farm_control.enc vis> read_blif -e farm_control.enc farm_control.opt.blif Warning: Some variables are unused in model farm_control[0]. vis> cd .. vis> init_verify vis> comb_verify tlc.mv Networks are combinationally equivalent. vis> print_network_stats main combinational=132 pi=0 po=0 latches=4 pseudo=2 const=34 edges=186 sis> read_blif farm_control.blif Warning: network `farm_control', node "[1]0" does not fanout Warning: network `farm_control', node "[5]0" does not fanout Warning: network `farm_control', node "[11]0" does not fanout sis> print_stats farm_control pi=18 po= 6 nodes= 62 latches= 0 lits(sop)= 709 lits(fac)= 419 sis> source script.rugged sis> print_stats farm_control pi=18 po= 6 nodes= 24 latches= 0 lits(sop)= 34 lits(fac)= 34 sis> write_blif farm_control.opt.blif In the previous example, the command init_verify has been given only in order to do print_network_stats before logic synthesis, to compare the networks before and after optimization by SIS. Next: Commands in VIS Up: No Title Previous: Formal Verification in Yuji Kukimoto Tue Feb 6 11:58:14 PST 1996

Contact

©2002-2018 U.C. Regents