diff options
| -rw-r--r-- | manual/CHAPTER_CellLib.tex | 101 | ||||
| -rw-r--r-- | passes/cmds/show.cc | 2 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 3 | ||||
| -rw-r--r-- | passes/techmap/tribuf.cc | 6 | ||||
| -rw-r--r-- | techlibs/xilinx/synth_xilinx.cc | 3 | ||||
| -rw-r--r-- | tests/arch/xilinx/tribuf.sh | 5 | ||||
| -rw-r--r-- | tests/sat/initval.ys | 11 |
7 files changed, 117 insertions, 14 deletions
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 00a88cc82..55abd9b96 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -198,8 +198,8 @@ calculated signal and a constant zero with an {\tt \$and} gate). \subsection{Registers} -D-Type Flip-Flops are represented by {\tt \$dff} cells. These cells have a clock port \B{CLK}, -an input port \B{D} and an output port \B{Q}. The following parameters are available for \$dff +D-type flip-flops are represented by {\tt \$dff} cells. These cells have a clock port \B{CLK}, +an input port \B{D} and an output port \B{Q}. The following parameters are available for {\tt \$dff} cells: \begin{itemize} @@ -211,13 +211,23 @@ Clock is active on the positive edge if this parameter has the value {\tt 1'b1} edge if this parameter is {\tt 1'b0}. \end{itemize} -D-Type Flip-Flops with asynchronous resets are represented by {\tt \$adff} cells. As the {\tt \$dff} +D-type flip-flops with enable are represented by {\tt \$dffe} cells. As the {\tt \$dff} +cells they have \B{CLK}, \B{D} and \B{Q} ports. In addition they also have a single-bit \B{EN} +input port for the enable pin and the following parameter: + +\begin{itemize} +\item \B{EN\_POLARITY} \\ +The enable input is active-high if this parameter has the value {\tt 1'b1} and active-low +if this parameter is {\tt 1'b0}. +\end{itemize} + +D-type flip-flops with asynchronous reset are represented by {\tt \$adff} cells. As the {\tt \$dff} cells they have \B{CLK}, \B{D} and \B{Q} ports. In addition they also have a single-bit \B{ARST} input port for the reset pin and the following additional two parameters: \begin{itemize} \item \B{ARST\_POLARITY} \\ -The asynchronous reset is high-active if this parameter has the value {\tt 1'b1} and low-active +The asynchronous reset is active-high if this parameter has the value {\tt 1'b1} and active-low if this parameter is {\tt 1'b0}. \item \B{ARST\_VALUE} \\ @@ -231,8 +241,27 @@ Usually these cells are generated by the {\tt proc} pass using the information in the designs RTLIL::Process objects. \end{sloppypar} +D-type flip-flops with asynchronous set and reset are represented by {\tt \$dffsr} cells. +As the {\tt \$dff} cells they have \B{CLK}, \B{D} and \B{Q} ports. In addition they also have +a single-bit \B{SET} input port for the set pin, a single-bit \B{CLR} input port for the reset pin, +and the following two parameters: + +\begin{itemize} +\item \B{SET\_POLARITY} \\ +The set input is active-high if this parameter has the value {\tt 1'b1} and active-low +if this parameter is {\tt 1'b0}. + +\item \B{CLR\_POLARITY} \\ +The reset input is active-high if this parameter has the value {\tt 1'b1} and active-low +if this parameter is {\tt 1'b0}. +\end{itemize} + +When both the set and reset inputs of a {\tt \$dffsr} cell are active, the reset input takes +precedence. + \begin{fixme} -Add information about {\tt \$sr} cells (set-reset flip-flops) and d-type latches. +Add information about {\tt \$sr} cells (set-reset flip-flops), {\tt \$dlatch} cells (d-type latches), +and {\tt \$dlatchsr} cells (d-type latches with set/reset). \end{fixme} \subsection{Memories} @@ -451,6 +480,30 @@ $ClkEdge$ & $RstLvl$ & $RstVal$ & Cell Type \\ \lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DFF\_PP0\_} \\ \lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DFF\_PP1\_} \\ \end{tabular} +% FIXME: the layout of this is broken and I have no idea how to fix it +\hfil +\begin{tabular}[t]{lll} +$ClkEdge$ & $EnLvl$ & Cell Type \\ +\hline +\lstinline[language=Verilog];negedge; & \lstinline[language=Verilog];0; & {\tt \$\_DFFE\_NN\_} \\ +\lstinline[language=Verilog];negedge; & \lstinline[language=Verilog];1; & {\tt \$\_DFFE\_NP\_} \\ +\lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];0; & {\tt \$\_DFFE\_PN\_} \\ +\lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];1; & {\tt \$\_DFFE\_PP\_} \\ +\end{tabular} +% FIXME: the layout of this is broken too +\hfil +\begin{tabular}[t]{llll} +$ClkEdge$ & $SetLvl$ & $RstLvl$ & Cell Type \\ +\hline +\lstinline[language=Verilog];negedge; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_DFFSR\_NNN\_} \\ +\lstinline[language=Verilog];negedge; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_DFFSR\_NNP\_} \\ +\lstinline[language=Verilog];negedge; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DFFSR\_NPN\_} \\ +\lstinline[language=Verilog];negedge; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DFFSR\_NPP\_} \\ +\lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_DFFSR\_PNN\_} \\ +\lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_DFFSR\_PNP\_} \\ +\lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DFFSR\_PPN\_} \\ +\lstinline[language=Verilog];posedge; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DFFSR\_PPP\_} \\ +\end{tabular} \caption{Cell types for gate level logic networks} \label{tab:CellLib_gates} \end{table} @@ -459,11 +512,22 @@ Table~\ref{tab:CellLib_gates} lists all cell types used for gate level logic. Th {\tt \$\_NOT\_}, {\tt \$\_AND\_}, {\tt \$\_NAND\_}, {\tt \$\_ANDNOT\_}, {\tt \$\_OR\_}, {\tt \$\_NOR\_}, {\tt \$\_ORNOT\_}, {\tt \$\_XOR\_}, {\tt \$\_XNOR\_} and {\tt \$\_MUX\_} are used to model combinatorial logic. The cell type {\tt \$\_TBUF\_} is used to model tristate logic. + The cell types {\tt \$\_DFF\_N\_} and {\tt \$\_DFF\_P\_} represent d-type flip-flops. +The cell types {\tt \$\_DFFE\_NN\_}, {\tt \$\_DFFE\_NP\_}, {\tt \$\_DFFE\_PN\_} and {\tt \$\_DFFE\_PP\_} +implement d-type flip-flops with enable. The values in the table for these cell types relate to the +following Verilog code template. + +\begin{lstlisting}[mathescape,language=Verilog] + always @($ClkEdge$ C) + if (EN == $EnLvl$) + Q <= D; +\end{lstlisting} + The cell types {\tt \$\_DFF\_NN0\_}, {\tt \$\_DFF\_NN1\_}, {\tt \$\_DFF\_NP0\_}, {\tt \$\_DFF\_NP1\_}, {\tt \$\_DFF\_PN0\_}, {\tt \$\_DFF\_PN1\_}, {\tt \$\_DFF\_PP0\_} and {\tt \$\_DFF\_PP1\_} implement -d-type flip-flops with asynchronous resets. The values in the table for these cell types relate to the +d-type flip-flops with asynchronous reset. The values in the table for these cell types relate to the following Verilog code template, where \lstinline[mathescape,language=Verilog];$RstEdge$; is \lstinline[language=Verilog];posedge; if \lstinline[mathescape,language=Verilog];$RstLvl$; if \lstinline[language=Verilog];1;, and \lstinline[language=Verilog];negedge; otherwise. @@ -476,6 +540,25 @@ otherwise. Q <= D; \end{lstlisting} +The cell types {\tt \$\_DFFSR\_NNN\_}, {\tt \$\_DFFSR\_NNP\_}, {\tt \$\_DFFSR\_NPN\_}, {\tt \$\_DFFSR\_NPP\_}, +{\tt \$\_DFFSR\_PNN\_}, {\tt \$\_DFFSR\_PNP\_}, {\tt \$\_DFFSR\_PPN\_} and {\tt \$\_DFFSR\_PPP\_} implement +d-type flip-flops with asynchronous set and reset. The values in the table for these cell types relate to the +following Verilog code template, where \lstinline[mathescape,language=Verilog];$RstEdge$; is \lstinline[language=Verilog];posedge; +if \lstinline[mathescape,language=Verilog];$RstLvl$; if \lstinline[language=Verilog];1;, \lstinline[language=Verilog];negedge; +otherwise, and \lstinline[mathescape,language=Verilog];$SetEdge$; is \lstinline[language=Verilog];posedge; +if \lstinline[mathescape,language=Verilog];$SetLvl$; if \lstinline[language=Verilog];1;, \lstinline[language=Verilog];negedge; +otherwise. + +\begin{lstlisting}[mathescape,language=Verilog] + always @($ClkEdge$ C, $RstEdge$ R, $SetEdge$ S) + if (R == $RstLvl$) + Q <= 0; + else if (S == $SetLvl$) + Q <= 1; + else + Q <= D; +\end{lstlisting} + In most cases gate level logic networks are created from RTL networks using the {\tt techmap} pass. The flip-flop cells from the gate level logic network can be mapped to physical flip-flop cells from a Liberty file using the {\tt dfflibmap} pass. The combinatorial logic cells can be mapped to physical cells from a Liberty file via ABC \citeweblink{ABC} @@ -507,11 +590,7 @@ Add information about {\tt \$ff} and {\tt \$\_FF\_} cells. \end{fixme} \begin{fixme} -Add information about {\tt \$dffe}, {\tt \$dffsr}, {\tt \$dlatch}, and {\tt \$dlatchsr} cells. -\end{fixme} - -\begin{fixme} -Add information about {\tt \$\_DFFE\_??\_}, {\tt \$\_DFFSR\_???\_}, {\tt \$\_DLATCH\_?\_}, and {\tt \$\_DLATCHSR\_???\_} cells. +Add information about {\tt \$\_DLATCH\_?\_}, and {\tt \$\_DLATCHSR\_???\_} cells. \end{fixme} \begin{fixme} diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index a3e969ef1..eeef24bde 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -873,7 +873,7 @@ struct ShowPass : public Pass { #ifdef __APPLE__ std::string cmd = stringf("ps -fu %d | grep -q '[ ]%s' || xdot '%s' &", getuid(), dot_file.c_str(), dot_file.c_str()); #else - std::string cmd = stringf("{ test -f '%s.pid' && fuser -s '%s.pid'; } || ( echo $$ >&3; exec xdot '%s'; ) 3> '%s.pid' &", dot_file.c_str(), dot_file.c_str(), dot_file.c_str(), dot_file.c_str()); + std::string cmd = stringf("{ test -f '%s.pid' && fuser -s '%s.pid' 2> /dev/null; } || ( echo $$ >&3; exec xdot '%s'; ) 3> '%s.pid' &", dot_file.c_str(), dot_file.c_str(), dot_file.c_str(), dot_file.c_str()); #endif log("Exec: %s\n", cmd.c_str()); if (run_command(cmd) != 0) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 430bba1e8..436ac1b01 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -269,7 +269,8 @@ struct SatHelper for (int i = 0; i < lhs.size(); i++) { RTLIL::SigSpec bit = lhs.extract(i, 1); if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit)) { - removed_bits.append(bit); + if (rhs[i] != State::Sx) + removed_bits.append(bit); lhs.remove(i, 1); rhs.remove(i, 1); i--; diff --git a/passes/techmap/tribuf.cc b/passes/techmap/tribuf.cc index 41fdc8f3d..decf9a202 100644 --- a/passes/techmap/tribuf.cc +++ b/passes/techmap/tribuf.cc @@ -86,6 +86,7 @@ struct TribufWorker { cell->unsetPort(ID(S)); cell->type = tri_type; tribuf_cells[sigmap(cell->getPort(ID::Y))].push_back(cell); + module->design->scratchpad_set_bool("tribuf.added_something", true); continue; } @@ -95,6 +96,7 @@ struct TribufWorker { cell->unsetPort(ID(S)); cell->type = tri_type; tribuf_cells[sigmap(cell->getPort(ID::Y))].push_back(cell); + module->design->scratchpad_set_bool("tribuf.added_something", true); continue; } } @@ -130,8 +132,10 @@ struct TribufWorker { if (no_tribuf) module->connect(it.first, muxout); - else + else { module->addTribuf(NEW_ID, muxout, module->ReduceOr(NEW_ID, pmux_s), it.first); + module->design->scratchpad_set_bool("tribuf.added_something", true); + } } } } diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc index 5c3b5179d..3c5599e4e 100644 --- a/techlibs/xilinx/synth_xilinx.cc +++ b/techlibs/xilinx/synth_xilinx.cc @@ -316,7 +316,10 @@ struct SynthXilinxPass : public ScriptPass run("proc"); if (flatten || help_mode) run("flatten", "(with '-flatten')"); + active_design->scratchpad_unset("tribuf.added_something"); run("tribuf -logic"); + if (noiopad && active_design->scratchpad_get_bool("tribuf.added_something")) + log_error("Tristate buffers are unsupported without the '-iopad' option.\n"); run("deminout"); run("opt_expr"); run("opt_clean"); diff --git a/tests/arch/xilinx/tribuf.sh b/tests/arch/xilinx/tribuf.sh new file mode 100644 index 000000000..636aed12a --- /dev/null +++ b/tests/arch/xilinx/tribuf.sh @@ -0,0 +1,5 @@ +! ../../../yosys ../common/tribuf.v -qp "synth_xilinx" +../../../yosys ../common/tribuf.v -qp "synth_xilinx -iopad; \ +select -assert-count 2 t:IBUF; \ +select -assert-count 1 t:INV; \ +select -assert-count 1 t:OBUFT" diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..1436724b0 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,3 +2,14 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts + +design -reset +read_verilog -icells <<EOT +module top(input clk, i, output [1:0] o); +(* init = 2'bx0 *) +wire [1:0] o; +assign o[1] = o[0]; +$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0])); +endmodule +EOT +sat -seq 1 |