summaryrefslogtreecommitdiffstats
path: root/src/aig/ioa/ioaUtil.c
blob: a2748382931eb8cf758349c99a2269a98640f1a4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
/**CFile****************************************************************

  FileName    [ioaUtil.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Command processing package.]

  Synopsis    [Procedures to read binary AIGER format developed by
  Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - December 16, 2006.]

  Revision    [$Id: ioaUtil.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]

***********************************************************************/

#include "ioa.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Returns the file size.]

  Description [The file should be closed.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ioa_FileSize( char * pFileName )
{
    FILE * pFile;
    int nFileSize;
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Ioa_FileSize(): The file is unavailable (absent or open).\n" );
        return 0;
    }
    fseek( pFile, 0, SEEK_END );  
    nFileSize = ftell( pFile ); 
    fclose( pFile );
    return nFileSize;
}

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Ioa_FileNameGeneric( char * FileName )
{
    char * pDot, * pRes;
    pRes = Abc_UtilStrsav( FileName );
    if ( (pDot = strrchr( pRes, '.' )) )
        *pDot = 0;
    return pRes;
}

/**Function*************************************************************

  Synopsis    [Returns the composite name of the file.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix )
{
    static char Buffer[1000];
    char * pDot;
    if ( pBase == NULL )
    {
        strcpy( Buffer, pSuffix );
        return Buffer;
    }
    strcpy( Buffer, pBase );
    if ( (pDot = strrchr( Buffer, '.' )) )
        *pDot = 0;
    strcat( Buffer, pSuffix );
    // find the last occurrance of slash
    for ( pDot = Buffer + strlen(Buffer) - 1; pDot >= Buffer; pDot-- )    
        if (!((*pDot >= '0' && *pDot <= '9') ||
              (*pDot >= 'a' && *pDot <= 'z') ||
              (*pDot >= 'A' && *pDot <= 'Z') || 
               *pDot == '_' || *pDot == '.') )
               break;
    return pDot + 1;
}

/**Function*************************************************************

  Synopsis    [Returns the time stamp.]

  Description [The file should be closed.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Ioa_TimeStamp()
{
    static char Buffer[100];
    char * TimeStamp;
    time_t ltime;
    // get the current time
    time( &ltime );
    TimeStamp = asctime( localtime( &ltime ) );
    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
    strcpy( Buffer, TimeStamp );
    return Buffer;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END
~\ref{navigate} introduces additional commands used to navigate in the design and select portions of the design and print additional information on the elements in the design that are not contained in the circuit diagrams. Sec.~\ref{poke} introduces commands to evaluate the design and solve SAT problems within the design. Sec.~\ref{conclusion} concludes the document and summarizes the key points. \section{Introduction to the {\tt show} command} \label{intro_show} \begin{figure}[b] \begin{lstlisting} $ cat example.ys read_verilog example.v show -pause proc show -pause opt show -pause $ cat example.v module example(input clk, a, b, c, output reg [1:0] y); always @(posedge clk) if (c) y <= c ? a + b : 2'd0; endmodule \end{lstlisting} \caption{Yosys script with {\tt show} commands and example design} \label{example_src} \end{figure} \begin{figure}[b!] \includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_00.pdf} \includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_01.pdf} \includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_02.pdf} \caption{Output of the three {\tt show} commands from Fig.~\ref{example_src}} \label{example_out} \end{figure} The {\tt show} command generates a circuit diagram for the design in its current state. Various options can be used to change the appearance of the circuit diagram, set the name and format for the output file, and so forth. When called without any special options, it saves the circuit diagram in a temporary file and launches {\tt yosys-svgviewer} to display the diagram. Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance (if still running). Fig.~\ref{example_src} shows a simple synthesis script and Verilog file that demonstrates the usage of {\tt show} in a simple setting. Note that {\tt show} is called with the {\tt -pause} option, that halts execution of the Yosys script until the user presses the Enter key. The {\tt show -pause} command also allows the user to enter an interactive shell to further investigate the circuit before continuing synthesis. So this script, when executed, will show the design after each of the three synthesis commands. The generated circuit diagrams are shown in Fig.~\ref{example_out}. The first diagram (from top to bottom) shows the design directly after being read by the Verilog front-end. Input and output ports are visualized using octagonal shapes. Cells are visualized as rectangles with inputs on the left and outputs on the right side. The cell labels are two lines long: The first line contains a unique identifier for the cell and the second line contains the cell type. Internal cell types are prefixed with a dollar sign. The Yosys manual contains a chapter on the internal cell library used in Yosys. Constants are shown as ellipses with the constant value as label. The syntax {\tt <bit\_width>'<bits>} is used for for constants that are not 32-bit wide and/or contain bits that are not 0 or 1 (but {\tt x} or {\tt z}). Ordinary 32-bit constants are written using decimal numbers. Single-bit signals are shown as thin arrows pointing from the driver to the load. Signals that are multiple bits wide are shown as think arrows. Finally {\it processes\/} are shown in boxes with round corners. Processes are Yosys' internal representation of the decision-trees and synchronization events modelled in a Verilog {\tt always}-block. The label reads {\tt PROC} followed by a unique identifier in the first line and contains the source code location of the original {\tt always}-block in the 2nd line. Note how the multiplexer from the {\tt ?:}-expression is represented as a {\tt \$mux} cell but the multiplexer from the {\tt if}-statement is yet still hidden within the process. \medskip The {\tt proc} command transforms the process from the first diagram into a multiplexer and a d-type flip-flip, which brings us to the 2nd diagram. The Rhombus shape to the right is a dangling wire. (Wire nodes are only shown if they are dangling or have "`public"' names, for example names assigned from the Verilog input.) Also note that the design now contains two instances of a {\tt BUF}-node. This are artefacts left behind by the {\tt proc}-command. It is quite usual to see such artefacts after calling commands that perform changes in the design, as most commands only care about doing the transformation in the least complicated way, not about cleaning up after them. The next call to {\tt clean} (or {\tt opt}, which includes {\tt clean} as one of its operations) will clean up this artefacts. This operation is so common in Yosys scripts that it can simply be abbreviated by using the {\tt ;;} token, which doubles as separator for commands. Unless one wants to specifically analyze this artefacts left behind some operations, it is therefore recommended to call {\tt clean} before calling {\tt show}. \medskip In this script we directly call {\tt opt} as next step, which finally leads us to the 3rd diagram in Fig.~\ref{example_out}. Here we see that the {\tt opt} command not only has removed the artifacts left behind by {\tt proc}, but also determined correctly that it can remove the first {\tt \$mux} cell without changing the behavior of the circuit. \medskip \begin{figure}[b!] \includegraphics[width=\linewidth,trim=0 2cm 0 0]{APPNOTE_011_Design_Investigation/splice.pdf} \caption{Output of {\tt yosys -p 'proc; opt; show' splice.v}} \label{splice_dia} \end{figure} \begin{figure}[b!] \begin{lstlisting} module splice_demo(a, b, c, d, e, f, x, y); input [1:0] a, b, c, d, e, f; output [1:0] x = {a[0], a[1]}; output [11:0] y; assign {y[11:4], y[1:0], y[3:2]} = {a, b, -{c, d}, ~{e, f}}; endmodule \end{lstlisting} \caption{\tt splice.v} \label{splice_src} \end{figure} \begin{figure}[t!] \includegraphics[height=\linewidth]{APPNOTE_011_Design_Investigation/cmos_00.pdf} \includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/cmos_01.pdf} \caption{Effects of {\tt splitnets} command and of providing a cell library. (The circuit is a half-adder built from simple CMOS gates.)} \label{splitnets_libfile} \end{figure} As has been indicated in this example, Yosys is can manage signal vectors (aka. multi-bit wires or buses) as native objects. This provides great advantages when analyzing circuits that operate on wide integers. But it also introduces some additional complexity when the individual bits of of a signal vector need to be accessed. The example show in Fig.~\ref{splice_dia} and \ref{splice_src} demonstrates how such circuits are visualized by the {\tt show} command. The key elements in understanding this circuit diagram are of course the boxes with round corners and rows labeled {\tt <MSB\_LEFT>:<LSB\_LEFT> -- <MSB\_RIGHT>:<LSB\_RIGHT>}. Each of this boxes has one signal per row on one side and a common signal for all rows on the other side. The {\tt <MSB>:<LSB>} tuples specify which bits are broken out from the signals and are connected. So The top row of the box connecting the signals {\tt a} and {\tt b} indicates that the bit 0 (i.e. the range 0:0) from signal {\tt a} is connected to bit 1 (i.e. the range 1:1) of signal {\tt x}. Lines connecting such boxes together and lines connecting such boxes to cell ports have slightly different look to emphasise that they are not actual signal wires but a necessity of the graphical representation. This distinction seems like a technicality, until one wants to debug a problem related to the way Yosys internally represents signal vectors, for example when writing custom Yosys commands. \medskip Finally Fig.~\ref{splitnets_libfile} shows two common pitfalls when working with designs mapped to a cell library. The top figure has two problems: First Yosys did not have access to the cell library when this diagram was generated, resulting in all cell ports defaulting to being inputs. This is why all ports are drawn on the left side the cells are awkwardly arranged in a large column. Secondly the two-bit vector {\tt y} requires breakout-boxes for its individual bits, resulting in an unnecessary complex diagram. For the 2nd diagram Yosys has been given a description of the cell library as Verilog file containing blackbox modules. There are two ways to load cell descriptions into Yosys: First the Verilog file for the cell library can be passed directly to the {\tt show} command using the {\tt -lib <filename>} option. Secondly it is possible to load cell libraries into the design with the {\tt read\_verilog -lib <filename>} command. The later option has the great advantage that the library only needs to be loaded once and can then be used in all subsequent calls to the {\tt show} command. In addition to that the 2nd diagram was generated after {\tt splitnet -ports} was run on the design. This command splits all signal vectors into individual signals, which is often desirable when looking at gate-level circuits. The {\tt -ports} option is required to also split module ports. Per default the command only operates on interior signals. \section{Navigating the design} \label{navigate} \FIXME{} --- cd and ls, dump, multi-page diagrams, select, cones and boolean operations \section{Advanced investigation techniques} \label{poke} \FIXME{} --- eval, sat \section{Conclusion} \label{conclusion} \FIXME \begin{thebibliography}{9} \bibitem{yosys} Clifford Wolf. The Yosys Open SYnthesis Suite. \url{http://www.clifford.at/yosys/} \bibitem{glaserwolf} Johann Glaser. Clifford Wolf. Methodology and Example-Driven Interconnect Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable Architectures. In: Jan Haase (Editor). {\it Models, Methods, and Tools for Complex Chip Design. Lecture Notes in Electrical Engineering. Volume 265, 2014, pp 201-221.\/} \href{http://dx.doi.org/10.1007/978-3-319-01418-0_12}{DOI 10.1007/978-3-319-01418-0\_12} \bibitem{graphviz} Graphviz - Graph Visualization Software. \url{http://www.graphviz.org/} \end{thebibliography} \end{document}