diff options
-rw-r--r-- | frontends/ast/ast.cc | 1 | ||||
-rw-r--r-- | frontends/ast/ast.h | 1 | ||||
-rw-r--r-- | frontends/ast/genrtlil.cc | 24 | ||||
-rw-r--r-- | frontends/ast/simplify.cc | 14 | ||||
-rw-r--r-- | frontends/verific/verific.cc | 2 | ||||
-rw-r--r-- | frontends/verilog/verilog_lexer.l | 2 | ||||
-rw-r--r-- | frontends/verilog/verilog_parser.y | 33 | ||||
-rw-r--r-- | manual/CHAPTER_CellLib.tex | 251 | ||||
-rw-r--r-- | passes/opt/opt_merge.cc | 4 | ||||
-rw-r--r-- | passes/sat/fmcombine.cc | 3 | ||||
-rw-r--r-- | passes/sat/qbfsat.cc | 89 | ||||
-rw-r--r-- | passes/sat/sim.cc | 5 | ||||
-rw-r--r-- | passes/tests/test_cell.cc | 4 | ||||
-rw-r--r-- | tests/svtypes/static_cast_negative.ys | 4 | ||||
-rw-r--r-- | tests/svtypes/static_cast_nonconst.ys | 4 | ||||
-rw-r--r-- | tests/svtypes/static_cast_simple.sv | 64 | ||||
-rw-r--r-- | tests/svtypes/static_cast_verilog.ys | 4 | ||||
-rw-r--r-- | tests/svtypes/static_cast_zero.ys | 4 | ||||
-rw-r--r-- | tests/various/const_func.v | 75 | ||||
-rw-r--r-- | tests/various/const_func.ys | 1 | ||||
-rw-r--r-- | tests/various/signed.ys | 28 |
21 files changed, 535 insertions, 82 deletions
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 03fd272da..9520ae32c 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -95,6 +95,7 @@ std::string AST::type2str(AstNodeType type) X(AST_TO_SIGNED) X(AST_TO_UNSIGNED) X(AST_SELFSZ) + X(AST_CAST_SIZE) X(AST_CONCAT) X(AST_REPLICATE) X(AST_BIT_NOT) diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h index 46864a4e1..9a5aa15f9 100644 --- a/frontends/ast/ast.h +++ b/frontends/ast/ast.h @@ -76,6 +76,7 @@ namespace AST AST_TO_SIGNED, AST_TO_UNSIGNED, AST_SELFSZ, + AST_CAST_SIZE, AST_CONCAT, AST_REPLICATE, AST_BIT_NOT, diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 9546558aa..e878d0dd2 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -814,6 +814,16 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun children.at(0)->detectSignWidthWorker(sub_width_hint, sign_hint); break; + case AST_CAST_SIZE: + while (children.at(0)->simplify(true, false, false, 1, -1, false, false)) { } + if (children.at(0)->type != AST_CONSTANT) + log_file_error(filename, location.first_line, "Static cast with non constant expression!\n"); + children.at(1)->detectSignWidthWorker(width_hint, sign_hint); + width_hint = children.at(0)->bitsAsConst().as_int(); + if (width_hint <= 0) + log_file_error(filename, location.first_line, "Static cast with zero or negative size!\n"); + break; + case AST_CONCAT: for (auto child : children) { sub_width_hint = 0; @@ -1289,6 +1299,20 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) return sig; } + // changing the size of signal can be done directly using RTLIL::SigSpec + case AST_CAST_SIZE: { + RTLIL::SigSpec size = children[0]->genRTLIL(); + RTLIL::SigSpec sig = children[1]->genRTLIL(); + if (!size.is_fully_const()) + log_file_error(filename, location.first_line, "Static cast with non constant expression!\n"); + int width = size.as_int(); + if (width <= 0) + log_file_error(filename, location.first_line, "Static cast with zero or negative size!\n"); + sig.extend_u0(width, sign_hint); + is_signed = sign_hint; + return sig; + } + // concatenation of signals can be done directly using RTLIL::SigSpec case AST_CONCAT: { RTLIL::SigSpec sig; diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 55e7da0aa..c4df5c0a0 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -950,6 +950,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, case AST_TO_SIGNED: case AST_TO_UNSIGNED: case AST_SELFSZ: + case AST_CAST_SIZE: case AST_CONCAT: case AST_REPLICATE: case AST_REDUCE_AND: @@ -1126,6 +1127,10 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, bool in_param_here = in_param; if (i == 0 && (type == AST_REPLICATE || type == AST_WIRE)) const_fold_here = true, in_param_here = true; + if (i == 0 && (type == AST_GENIF || type == AST_GENCASE)) + in_param_here = true; + if (i == 1 && (type == AST_FOR || type == AST_GENFOR)) + in_param_here = true; if (type == AST_PARAMETER || type == AST_LOCALPARAM) const_fold_here = true; if (i == 0 && (type == AST_ASSIGN || type == AST_ASSIGN_EQ || type == AST_ASSIGN_LE)) @@ -1942,7 +1947,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, continue; buf = child->clone(); - while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { } + while (buf->simplify(true, false, false, stage, width_hint, sign_hint, true)) { } if (buf->type != AST_CONSTANT) { // for (auto f : log_files) // dumpAst(f, "verilog-ast> "); @@ -3483,6 +3488,13 @@ replace_fcall_later:; } } break; + case AST_CAST_SIZE: + if (children.at(0)->type == AST_CONSTANT && children.at(1)->type == AST_CONSTANT) { + int width = children[0]->bitsAsConst().as_int(); + RTLIL::Const val = children[1]->bitsAsConst(width); + newNode = mkconst_bits(val.bits, children[1]->is_signed); + } + break; case AST_CONCAT: string_op = !children.empty(); for (auto it = children.begin(); it != children.end(); it++) { diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index ccd13e92f..9785b8eff 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -53,7 +53,7 @@ USING_YOSYS_NAMESPACE # error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific." #endif -#if SYMBIOTIC_VERIFIC_API_VERSION < 1 +#if SYMBIOTIC_VERIFIC_API_VERSION < 202006 # error "Please update your version of Symbiotic EDA flavored Verific." #endif diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 028106381..f2241066f 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -517,6 +517,8 @@ import[ \t\r\n]+\"(DPI|DPI-C)\"[ \t\r\n]+function[ \t\r\n]+ { "<<<" { return OP_SSHL; } ">>>" { return OP_SSHR; } +"'" { return OP_CAST; } + "::" { return TOK_PACKAGESEP; } "++" { return TOK_INCREMENT; } "--" { return TOK_DECREMENT; } diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 96d9299fe..656910c0c 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -299,6 +299,7 @@ static void rewriteAsMemoryNode(AstNode *node, AstNode *rangeNode) %left '+' '-' %left '*' '/' '%' %left OP_POW +%left OP_CAST %right UNARY_OPS %define parse.error verbose @@ -746,7 +747,7 @@ module_body: module_body_stmt: task_func_decl | specify_block | param_decl | localparam_decl | typedef_decl | defparam_decl | specparam_declaration | wire_decl | assign_stmt | cell_stmt | enum_decl | struct_decl | - always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property | checker_decl | ignored_specify_block; + always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property | checker_decl | ignored_specify_block | /* empty statement */ ';'; checker_decl: TOK_CHECKER TOK_ID ';' { @@ -1330,6 +1331,8 @@ ignspec_id: param_signed: TOK_SIGNED { astbuf1->is_signed = true; + } | TOK_UNSIGNED { + astbuf1->is_signed = false; } | /* empty */; param_integer: @@ -1340,14 +1343,14 @@ param_integer: astbuf1->children.back()->children.push_back(AstNode::mkconst_int(31, true)); astbuf1->children.back()->children.push_back(AstNode::mkconst_int(0, true)); astbuf1->is_signed = true; - } | /* empty */; + } param_real: TOK_REAL { if (astbuf1->children.size() != 1) frontend_verilog_yyerror("Parameter already declared as integer, cannot set to real."); astbuf1->children.push_back(new AstNode(AST_REALVALUE)); - } | /* empty */; + } param_range: range { @@ -1358,8 +1361,12 @@ param_range: } }; +param_integer_type: param_integer param_signed +param_range_type: type_vec param_signed param_range +param_implicit_type: param_signed param_range + param_type: - param_signed param_integer param_real param_range | + param_integer_type | param_real | param_range_type | param_implicit_type | hierarchical_type_id { astbuf1->is_custom_type = true; astbuf1->children.push_back(new AstNode(AST_WIRETYPE)); @@ -3042,6 +3049,24 @@ basic_expr: $$ = new AstNode(AST_LOGIC_NOT, $3); SET_AST_NODE_LOC($$, @1, @3); append_attr($$, $2); + } | + TOK_SIGNED OP_CAST '(' expr ')' { + if (!sv_mode) + frontend_verilog_yyerror("Static cast is only supported in SystemVerilog mode."); + $$ = new AstNode(AST_TO_SIGNED, $4); + SET_AST_NODE_LOC($$, @1, @4); + } | + TOK_UNSIGNED OP_CAST '(' expr ')' { + if (!sv_mode) + frontend_verilog_yyerror("Static cast is only supported in SystemVerilog mode."); + $$ = new AstNode(AST_TO_UNSIGNED, $4); + SET_AST_NODE_LOC($$, @1, @4); + } | + basic_expr OP_CAST '(' expr ')' { + if (!sv_mode) + frontend_verilog_yyerror("Static cast is only supported in SystemVerilog mode."); + $$ = new AstNode(AST_CAST_SIZE, $1, $4); + SET_AST_NODE_LOC($$, @1, @4); }; concat_list: diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 25adcda86..d4572a88a 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -221,6 +221,26 @@ calculated signal and a constant zero with an {\tt \$and} gate). \subsection{Registers} +SR-type latches are represented by {\tt \$sr} cells. These cells have input ports +\B{SET} and \B{CLR} and an output port \B{Q}. They have the following parameters: + +\begin{itemize} +\item \B{WIDTH} \\ +The width of inputs \B{SET} and \B{CLR} and output \B{Q}. + +\item \B{SET\_POLARITY} \\ +The set input bits are 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 bits are active-high if this parameter has the value {\tt 1'b1} and active-low +if this parameter is {\tt 1'b0}. +\end{itemize} + +Both set and reset inputs have separate bits for every output bit. +When both the set and reset inputs of an {\tt \$sr} cell are active for a given bit +index, the reset input takes precedence. + 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: @@ -269,21 +289,8 @@ Note that the {\tt \$adff} and {\tt \$sdff} cells can only be used when the rese 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. +multi-bit \B{SET} and \B{CLR} input ports and the corresponding polarity parameters, like +{\tt \$sr} cells. D-type flip-flops with enable are represented by {\tt \$dffe}, {\tt \$adffe}, {\tt \$dffsre}, {\tt \$sdffe}, and {\tt \$sdffce} cells, which are enhanced variants of {\tt \$dff}, {\tt \$adff}, {\tt \$dffsr}, @@ -297,10 +304,36 @@ The enable input is active-high if this parameter has the value {\tt 1'b1} and a if this parameter is {\tt 1'b0}. \end{itemize} -\begin{fixme} -Add information about {\tt \$sr} cells (set-reset flip-flops), {\tt \$dlatch} cells (d-type latches), -{\tt \$adlatch} and {\tt \$dlatchsr} cells (d-type latches with set/reset). -\end{fixme} +D-type latches are represented by {\tt \$dlatch} cells. These cells have an enable port \B{EN}, +an input port \B{D}, and an output port \B{Q}. The following parameters are available for {\tt \$dlatch} cells: + +\begin{itemize} +\item \B{WIDTH} \\ +The width of input \B{D} and output \B{Q}. + +\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} + +The latch is transparent when the \B{EN} input is active. + +D-type latches with reset are represented by {\tt \$adlatch} cells. In addition to {\tt \$dlatch} +ports and parameters, they also have a single-bit \B{ARST} input port for the reset pin and the following additional parameters: + +\begin{itemize} +\item \B{ARST\_POLARITY} \\ +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} \\ +The state of \B{Q} will be set to this value when the reset is active. +\end{itemize} + +D-type latches with set and reset are represented by {\tt \$dlatchsr} cells. +In addition to {\tt \$dlatch} ports and parameters, they also have multi-bit +\B{SET} and \B{CLR} input ports and the corresponding polarity parameters, like +{\tt \$sr} cells. \subsection{Memories} \label{sec:memcells} @@ -476,6 +509,23 @@ The {\tt memory\_map} pass can be used to implement {\tt \$mem} cells as basic l Add a brief description of the {\tt \$fsm} cell type. \end{fixme} +\subsection{Specify rules} + +\begin{fixme} +Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} cells. +\end{fixme} + +\subsection{Formal verification cells} + +\begin{fixme} +Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv}, +{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells. +\end{fixme} + +\begin{fixme} +Add information about {\tt \$ff} and {\tt \$\_FF\_} cells. +\end{fixme} + \section{Gates} \label{sec:celllib_gates} @@ -490,6 +540,7 @@ source tree. \begin{tabular}[t]{ll} Verilog & Cell Type \\ \hline +\lstinline[language=Verilog]; Y = A; & {\tt \$\_BUF\_} \\ \lstinline[language=Verilog]; Y = ~A; & {\tt \$\_NOT\_} \\ \lstinline[language=Verilog]; Y = A & B; & {\tt \$\_AND\_} \\ \lstinline[language=Verilog]; Y = ~(A & B); & {\tt \$\_NAND\_} \\ @@ -499,11 +550,21 @@ Verilog & Cell Type \\ \lstinline[language=Verilog]; Y = A | ~B; & {\tt \$\_ORNOT\_} \\ \lstinline[language=Verilog]; Y = A ^ B; & {\tt \$\_XOR\_} \\ \lstinline[language=Verilog]; Y = ~(A ^ B); & {\tt \$\_XNOR\_} \\ +\lstinline[language=Verilog]; Y = ~((A & B) | C); & {\tt \$\_AOI3\_} \\ +\lstinline[language=Verilog]; Y = ~((A | B) & C); & {\tt \$\_OAI3\_} \\ +\lstinline[language=Verilog]; Y = ~((A & B) | (C & D)); & {\tt \$\_AOI4\_} \\ +\lstinline[language=Verilog]; Y = ~((A | B) & (C | D)); & {\tt \$\_OAI4\_} \\ \lstinline[language=Verilog]; Y = S ? B : A; & {\tt \$\_MUX\_} \\ -\lstinline[language=Verilog]; Y = EN ? A : 'bz; & {\tt \$\_TBUF\_} \\ +\lstinline[language=Verilog]; Y = ~(S ? B : A); & {\tt \$\_NMUX\_} \\ +(see below) & {\tt \$\_MUX4\_} \\ +(see below) & {\tt \$\_MUX8\_} \\ +(see below) & {\tt \$\_MUX16\_} \\ +\lstinline[language=Verilog]; Y = EN ? A : 1'bz; & {\tt \$\_TBUF\_} \\ \hline \lstinline[language=Verilog]; always @(negedge C) Q <= D; & {\tt \$\_DFF\_N\_} \\ \lstinline[language=Verilog]; always @(posedge C) Q <= D; & {\tt \$\_DFF\_P\_} \\ +\lstinline[language=Verilog]; always @* if (!E) Q <= D; & {\tt \$\_DLATCH\_N\_} \\ +\lstinline[language=Verilog]; always @* if (E) Q <= D; & {\tt \$\_DLATCH\_P\_} \\ \end{tabular} \caption{Cell types for gate level logic networks (main list)} \label{tab:CellLib_gates} @@ -610,14 +671,88 @@ $ClkEdge$ & $SetLvl$ & $RstLvl$ & $EnLvl$ & Cell Type \\ \label{tab:CellLib_gates_dffsre} \end{table} -Tables~\ref{tab:CellLib_gates}, \ref{tab:CellLib_gates_dffe}, \ref{tab:CellLib_gates_adff}, \ref{tab:CellLib_gates_adffe}, \ref{tab:CellLib_gates_dffsr} and \ref{tab:CellLib_gates_dffsre} list all cell types used for gate level logic. The cell types -{\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. +\begin{table}[t] +\hfil +\begin{tabular}[t]{llll} +$EnLvl$ & $RstLvl$ & $RstVal$ & Cell Type \\ +\hline +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCH\_NN0\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCH\_NN1\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCH\_NP0\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCH\_NP1\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCH\_PN0\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCH\_PN1\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCH\_PP0\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCH\_PP1\_} \\ +\end{tabular} +\caption{Cell types for gate level logic networks (latches with reset)} +\label{tab:CellLib_gates_adlatch} +\end{table} + +\begin{table}[t] +\hfil +\begin{tabular}[t]{llll} +$EnLvl$ & $SetLvl$ & $RstLvl$ & Cell Type \\ +\hline +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCHSR\_NNN\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCHSR\_NNP\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCHSR\_NPN\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCHSR\_NPP\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCHSR\_PNN\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCHSR\_PNP\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_DLATCHSR\_PPN\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_DLATCHSR\_PPP\_} \\ +\end{tabular} +\caption{Cell types for gate level logic networks (latches with set and reset)} +\label{tab:CellLib_gates_dlatchsr} +\end{table} + +\begin{table}[t] +\hfil +\begin{tabular}[t]{llll} +$SetLvl$ & $RstLvl$ & Cell Type \\ +\hline +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];0; & {\tt \$\_SR\_NN\_} \\ +\lstinline[language=Verilog];0; & \lstinline[language=Verilog];1; & {\tt \$\_SR\_NP\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];0; & {\tt \$\_SR\_PN\_} \\ +\lstinline[language=Verilog];1; & \lstinline[language=Verilog];1; & {\tt \$\_SR\_PP\_} \\ +\end{tabular} +\caption{Cell types for gate level logic networks (SR latches)} +\label{tab:CellLib_gates_sr} +\end{table} + +Tables~\ref{tab:CellLib_gates}, \ref{tab:CellLib_gates_dffe}, \ref{tab:CellLib_gates_adff}, \ref{tab:CellLib_gates_adffe}, \ref{tab:CellLib_gates_dffsr}, \ref{tab:CellLib_gates_dffsre}, \ref{tab:CellLib_gates_adlatch}, \ref{tab:CellLib_gates_dlatchsr} and \ref{tab:CellLib_gates_sr} list all cell types used for gate level logic. The cell types +{\tt \$\_BUF\_}, {\tt \$\_NOT\_}, {\tt \$\_AND\_}, {\tt \$\_NAND\_}, {\tt \$\_ANDNOT\_}, +{\tt \$\_OR\_}, {\tt \$\_NOR\_}, {\tt \$\_ORNOT\_}, {\tt \$\_XOR\_}, {\tt \$\_XNOR\_}, +{\tt \$\_AOI3\_}, {\tt \$\_OAI3\_}, {\tt \$\_AOI4\_}, {\tt \$\_OAI4\_}, +{\tt \$\_MUX\_}, {\tt \$\_MUX4\_}, {\tt \$\_MUX8\_}, {\tt \$\_MUX16\_} and {\tt \$\_NMUX\_} are used to model combinatorial logic. The cell type {\tt \$\_TBUF\_} is used to model tristate logic. +The {\tt \$\_MUX4\_}, {\tt \$\_MUX8\_} and {\tt \$\_MUX16\_} cells are used to model wide muxes, and correspond to the following Verilog code: + +\begin{lstlisting}[language=Verilog] +// $_MUX4_ +assign Y = T ? (S ? D : C) : + (S ? B : A); +// $_MUX8_ +assign Y = U ? T ? (S ? H : G) : + (S ? F : E) : + T ? (S ? D : C) : + (S ? B : A); +// $_MUX16_ +assign Y = V ? U ? T ? (S ? P : O) : + (S ? N : M) : + T ? (S ? L : K) : + (S ? J : I) : + U ? T ? (S ? H : G) : + (S ? F : E) : + T ? (S ? D : C) : + (S ? B : A); +\end{lstlisting} + 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\_} +The cell types {\tt \$\_DFFE\_[NP][NP]\_} implement d-type flip-flops with enable. The values in the table for these cell types relate to the following Verilog code template. @@ -627,8 +762,7 @@ following Verilog code template. 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 +The cell types {\tt \$\_DFF\_[NP][NP][01]\_} implement 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; @@ -642,8 +776,7 @@ otherwise. Q <= D; \end{lstlisting} -The cell types {\tt \$\_SDFF\_NN0\_}, {\tt \$\_SDFF\_NN1\_}, {\tt \$\_SDFF\_NP0\_}, {\tt \$\_SDFF\_NP1\_}, -{\tt \$\_SDFF\_PN0\_}, {\tt \$\_SDFF\_PN1\_}, {\tt \$\_SDFF\_PP0\_} and {\tt \$\_SDFF\_PP1\_} implement +The cell types {\tt \$\_SDFF\_[NP][NP][01]\_} implement d-type flip-flops with synchronous reset. The values in the table for these cell types relate to the following Verilog code template: @@ -732,21 +865,52 @@ otherwise. Q <= D; \end{lstlisting} +The cell types {\tt \$\_DLATCH\_N\_} and {\tt \$\_DLATCH\_P\_} represent d-type latches. + +The cell types {\tt \$\_DLATCH\_[NP][NP][01]\_} implement +d-type latches with reset. The values in the table for these cell types relate to the +following Verilog code template: + +\begin{lstlisting}[mathescape,language=Verilog] + always @* + if (R == $RstLvl$) + Q <= $RstVal$; + else if (E == $EnLvl$) + Q <= D; +\end{lstlisting} + +The cell types {\tt \$\_DLATCHSR\_[NP][NP][NP]\_} implement +d-type latches with set and reset. The values in the table for these cell types relate to the +following Verilog code template: + +\begin{lstlisting}[mathescape,language=Verilog] + always @* + if (R == $RstLvl$) + Q <= 0; + else if (S == $SetLvl$) + Q <= 1; + else if (E == $EnLvl$) + Q <= D; +\end{lstlisting} + +The cell types {\tt \$\_SR\_[NP][NP]\_} implement +sr-type latches. The values in the table for these cell types relate to the +following Verilog code template: + +\begin{lstlisting}[mathescape,language=Verilog] + always @* + if (R == $RstLvl$) + Q <= 0; + else if (S == $SetLvl$) + Q <= 1; +\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} using the {\tt abc} pass. \begin{fixme} -Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv}, -{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells. -\end{fixme} - -\begin{fixme} -Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} cells. -\end{fixme} - -\begin{fixme} Add information about {\tt \$slice} and {\tt \$concat} cells. \end{fixme} @@ -757,16 +921,3 @@ Add information about {\tt \$lut} and {\tt \$sop} cells. \begin{fixme} Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cells. \end{fixme} - -\begin{fixme} -Add information about {\tt \$ff} and {\tt \$\_FF\_} cells. -\end{fixme} - -\begin{fixme} -Add information about {\tt \$\_DLATCH\_?\_}, and {\tt \$\_DLATCHSR\_???\_} cells. -\end{fixme} - -\begin{fixme} -Add information about {\tt \$\_AOI3\_}, {\tt \$\_OAI3\_}, {\tt \$\_AOI4\_}, {\tt \$\_OAI4\_}, and {\tt \$\_NMUX\_} cells. -\end{fixme} - diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc index a95aa74c1..f03faa9cf 100644 --- a/passes/opt/opt_merge.cc +++ b/passes/opt/opt_merge.cc @@ -298,9 +298,7 @@ struct OptMergeWorker module->connect(RTLIL::SigSig(it.second, other_sig)); assign_map.add(it.second, other_sig); - if (it.first == ID::Q && (cell->type.begins_with("$dff") || cell->type.begins_with("$dlatch") || - cell->type.begins_with("$_DFF") || cell->type.begins_with("$_DLATCH") || cell->type.begins_with("$_SR_") || - cell->type.in(ID($adff), ID($sr), ID($ff), ID($_FF_)))) { + if (it.first == ID::Q && RTLIL::builtin_ff_cell_types().count(cell->type)) { for (auto c : it.second.chunks()) { auto jt = c.wire->attributes.find(ID::init); if (jt == c.wire->attributes.end()) diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc index 5694a7473..cb49edac3 100644 --- a/passes/sat/fmcombine.cc +++ b/passes/sat/fmcombine.cc @@ -114,8 +114,7 @@ struct FmcombineWorker Cell *gold = import_prim_cell(cell, "_gold"); Cell *gate = import_prim_cell(cell, "_gate"); if (opts.initeq) { - if (cell->type.in(ID($ff), ID($dff), ID($dffe), - ID($dffsr), ID($adff), ID($dlatch), ID($dlatchsr))) { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { SigSpec gold_q = gold->getPort(ID::Q); SigSpec gate_q = gate->getPort(ID::Q); SigSpec en = module->Initstate(NEW_ID); diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index f4624ab3b..136259558 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -51,6 +51,7 @@ struct QbfSolveOptions { bool nooptimize, nobisection; bool sat, unsat, show_smtbmc; enum Solver{Z3, Yices, CVC4} solver; + enum OptimizationLevel{O0, O1, O2} oflag; int timeout; std::string specialize_soln_file; std::string write_soln_soln_file; @@ -59,7 +60,7 @@ struct QbfSolveOptions { QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false), nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), - solver(Yices), timeout(0), argidx(0) {}; + solver(Yices), oflag(O0), timeout(0), argidx(0) {}; }; std::string get_solver_name(const QbfSolveOptions &opt) { @@ -147,6 +148,9 @@ void recover_solution(QbfSolutionType &sol) { dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) { dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit; + pool<RTLIL::SigBit> anyconst_sigbits; + dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit; + for (auto cell : module->cells()) { pool<std::string> cell_src = cell->get_strpool_attribute(ID::src); auto pos = sol.hole_to_value.find(cell_src); @@ -154,10 +158,30 @@ dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_m RTLIL::SigSpec port_y = cell->getPort(ID::Y); for (int i = GetSize(port_y) - 1; i >= 0; --i) { hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i]; + anyconst_sigbits.insert(port_y[i]); + } + } + } + + for (auto &conn : module->connections()) { + auto lhs = conn.first; + auto rhs = conn.second; + for (auto i = 0; i < GetSize(rhs); ++i) { + if (anyconst_sigbits[rhs[i]]) { + auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]); + if (pos != anyconst_sigbit_to_wire_sigbit.end()) + log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i])); + anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i]; } } } + for (auto &it : hole_loc_idx_to_sigbit) { + auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second); + if (pos != anyconst_sigbit_to_wire_sigbit.end()) + it.second = pos->second; + } + return hole_loc_idx_to_sigbit; } @@ -274,8 +298,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { pool<std::string> hole_loc_pool(locs.begin(), locs.end()); auto hole_cell_it = anyconst_loc_to_cell.find(hole_loc_pool); if (hole_cell_it == anyconst_loc_to_cell.end()) - YS_DEBUGTRAP; - //log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str()); + log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str()); RTLIL::Cell *hole_cell = hole_cell_it->second; hole_sigbit = hole_cell->getPort(ID::Y)[hole_bit]; @@ -438,8 +461,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { RTLIL::Module *module = mod; RTLIL::Design *design = module->design; std::string module_name = module->name.str(); - RTLIL::Wire *wire_to_optimize = nullptr; - RTLIL::IdString wire_to_optimize_name; + RTLIL::IdString wire_to_optimize_name = ""; bool maximize = false; log_assert(module->design != nullptr); @@ -452,19 +474,30 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { assume_miter_outputs(module, opt); //Find the wire to be optimized, if any: - for (auto wire : module->wires()) - if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) - wire_to_optimize = wire; - if (wire_to_optimize != nullptr) { - wire_to_optimize_name = wire_to_optimize->name; - maximize = wire_to_optimize->get_bool_attribute("\\maximize"); + for (auto wire : module->wires()) { + if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) { + wire_to_optimize_name = wire->name; + maximize = wire->get_bool_attribute("\\maximize"); + if (opt.nooptimize) { + if (maximize) + wire->set_bool_attribute("\\maximize", false); + else + wire->set_bool_attribute("\\minimize", false); + } + } } - if (opt.nobisection || opt.nooptimize || wire_to_optimize == nullptr) { - if (wire_to_optimize != nullptr && opt.nooptimize) { - wire_to_optimize->set_bool_attribute("\\maximize", false); - wire_to_optimize->set_bool_attribute("\\minimize", false); - } + //If -O1 or -O2 was specified, use ABC to simplify the problem: + if (opt.oflag == opt.OptimizationLevel::O1) + Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor,-N,10,-lz;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str()); + else if (opt.oflag == opt.OptimizationLevel::O2) + Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;dch,-S,1000000,-C,100000,-p;print_stats;fraig;print_stats;refactor,-N,15,-lz;print_stats;dc2,-pbl;print_stats;drwsat;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str()); + if (opt.oflag != opt.OptimizationLevel::O0) { + Pass::call(module->design, "techmap"); + Pass::call(module->design, "opt"); + } + + if (opt.nobisection || opt.nooptimize || wire_to_optimize_name == "") { ret = call_qbf_solver(module, opt, tempdir_name, false, 0); } else { //Do the iterated bisection method: @@ -473,8 +506,9 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { unsigned int failure = 0; unsigned int cur_thresh = 0; - log_assert(wire_to_optimize != nullptr); - log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize)); + log_assert(wire_to_optimize_name != ""); + log_assert(module->wire(wire_to_optimize_name) != nullptr); + log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), wire_to_optimize_name.c_str()); //If maximizing, grow until we get a failure. Then bisect success and failure. while (failure == 0 || difference(success, failure) > 1) { @@ -607,6 +641,22 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { } continue; } + else if (args[opt.argidx].substr(0, 2) == "-O" && args[opt.argidx].size() == 3) { + switch (args[opt.argidx][2]) { + case '0': + opt.oflag = opt.OptimizationLevel::O0; + break; + case '1': + opt.oflag = opt.OptimizationLevel::O1; + break; + case '2': + opt.oflag = opt.OptimizationLevel::O2; + break; + default: + log_cmd_error("unknown argument %s\n", args[opt.argidx].c_str()); + } + continue; + } else if (args[opt.argidx] == "-sat") { opt.sat = true; continue; @@ -721,6 +771,9 @@ struct QbfSatPass : public Pass { log(" -timeout <value>\n"); log(" Set the per-iteration timeout in seconds.\n"); log("\n"); + log(" -O0, -O1, -O2\n"); + log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n"); + log("\n"); log(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); log("\n"); diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 1ab082b09..fb496ff87 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -163,7 +163,10 @@ struct SimInstance mem_database[cell] = mem; } - + if (cell->type.in(ID($memwr),ID($memrd))) + { + log_error("$memrd and $memwr cells have to be merged to stand-alone $mem cells (execute memory_collect pass)\n"); + } if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); } diff --git a/passes/tests/test_cell.cc b/passes/tests/test_cell.cc index 125efbaa3..bdb475d3b 100644 --- a/passes/tests/test_cell.cc +++ b/passes/tests/test_cell.cc @@ -909,7 +909,7 @@ struct TestCellPass : public Pass { if (!ilang_file.empty()) { if (!selected_cell_types.empty()) log_cmd_error("Do not specify any cell types when using -f.\n"); - selected_cell_types.push_back("ilang"); + selected_cell_types.push_back(ID(ilang)); } if (selected_cell_types.empty()) @@ -921,7 +921,7 @@ struct TestCellPass : public Pass { for (int i = 0; i < num_iter; i++) { RTLIL::Design *design = new RTLIL::Design; - if (cell_type == "ilang") + if (cell_type == ID(ilang)) Frontend::frontend_call(design, NULL, std::string(), "ilang " + ilang_file); else create_gold_module(design, cell_type, cell_types.at(cell_type), constmode, muxdiv); diff --git a/tests/svtypes/static_cast_negative.ys b/tests/svtypes/static_cast_negative.ys new file mode 100644 index 000000000..4f9e8cf6e --- /dev/null +++ b/tests/svtypes/static_cast_negative.ys @@ -0,0 +1,4 @@ +logger -expect error "Static cast with zero or negative size" 1 +read_verilog -sv <<EOT +module top; wire [7:0] a = (-1)'(a); endmodule +EOT diff --git a/tests/svtypes/static_cast_nonconst.ys b/tests/svtypes/static_cast_nonconst.ys new file mode 100644 index 000000000..72d8f9910 --- /dev/null +++ b/tests/svtypes/static_cast_nonconst.ys @@ -0,0 +1,4 @@ +logger -expect error "Static cast with non constant expression" 1 +read_verilog -sv <<EOT +module top; wire [7:0] a, b = (a)'(0); endmodule +EOT diff --git a/tests/svtypes/static_cast_simple.sv b/tests/svtypes/static_cast_simple.sv new file mode 100644 index 000000000..2e4ad7d2b --- /dev/null +++ b/tests/svtypes/static_cast_simple.sv @@ -0,0 +1,64 @@ +module top; + wire [7:0] a, b, c, d; + assign a = 8'd16; + assign b = 8'd16; + assign c = (a * b) >> 8; + assign d = (16'(a) * b) >> 8; + + parameter P = 16; + + wire signed [7:0] s0, s1, s2; + wire [7:0] u0, u1, u2, u3, u4, u5, u6; + assign s0 = -8'd1; + assign s1 = 4'(s0); + assign s2 = 4'(unsigned'(s0)); + assign u0 = -8'd1; + assign u1 = 4'(u0); + assign u2 = 4'(signed'(u0)); + assign u3 = 8'(4'(s0)); + assign u4 = 8'(4'(u0)); + assign u5 = 8'(4'(signed'(-8'd1))); + assign u6 = 8'(4'(unsigned'(-8'd1))); + + wire [8:0] n0, n1, n2, n3, n4, n5, n6, n7, n8, n9; + assign n0 = s1; + assign n1 = s2; + assign n2 = 9'(s1); + assign n3 = 9'(s2); + assign n4 = 9'(unsigned'(s1)); + assign n5 = 9'(unsigned'(s2)); + assign n6 = 9'(u0); + assign n7 = 9'(u1); + assign n8 = 9'(signed'(u0)); + assign n9 = 9'(signed'(u1)); + + always_comb begin + assert(c == 8'b0000_0000); + assert(d == 8'b0000_0001); + + assert((P + 1)'(a) == 17'b0_0000_0000_0001_0000); + assert((P + 1)'(d - 2) == 17'b1_1111_1111_1111_1111); + + assert(s0 == 8'b1111_1111); + assert(s1 == 8'b1111_1111); + assert(s2 == 8'b0000_1111); + assert(u0 == 8'b1111_1111); + assert(u1 == 8'b0000_1111); + assert(u2 == 8'b1111_1111); + assert(u3 == 8'b1111_1111); + assert(u4 == 8'b0000_1111); + assert(u5 == 8'b1111_1111); + assert(u6 == 8'b0000_1111); + + assert(n0 == 9'b1_1111_1111); + assert(n1 == 9'b0_0000_1111); + assert(n2 == 9'b1_1111_1111); + assert(n3 == 9'b0_0000_1111); + assert(n4 == 9'b0_1111_1111); + assert(n5 == 9'b0_0000_1111); + assert(n6 == 9'b0_1111_1111); + assert(n7 == 9'b0_0000_1111); + assert(n8 == 9'b1_1111_1111); + assert(n9 == 9'b0_0000_1111); + end +endmodule diff --git a/tests/svtypes/static_cast_verilog.ys b/tests/svtypes/static_cast_verilog.ys new file mode 100644 index 000000000..fa3680b68 --- /dev/null +++ b/tests/svtypes/static_cast_verilog.ys @@ -0,0 +1,4 @@ +logger -expect error "Static cast is only supported in SystemVerilog mode" 1 +read_verilog <<EOT +module top; wire [7:0] a = 1'(a); endmodule +EOT diff --git a/tests/svtypes/static_cast_zero.ys b/tests/svtypes/static_cast_zero.ys new file mode 100644 index 000000000..d8335ca1b --- /dev/null +++ b/tests/svtypes/static_cast_zero.ys @@ -0,0 +1,4 @@ +logger -expect error "Static cast with zero or negative size" 1 +read_verilog -sv <<EOT +module top; wire [7:0] a = 0'(a); endmodule +EOT diff --git a/tests/various/const_func.v b/tests/various/const_func.v new file mode 100644 index 000000000..76cdc385d --- /dev/null +++ b/tests/various/const_func.v @@ -0,0 +1,75 @@ +module Example(outA, outB, outC, outD); + parameter OUTPUT = "FOO"; + output wire [23:0] outA; + output wire [23:0] outB; + output reg outC, outD; + function automatic [23:0] flip; + input [23:0] inp; + flip = ~inp; + endfunction + + generate + if (flip(OUTPUT) == flip("BAR")) + assign outA = OUTPUT; + else + assign outA = 0; + + case (flip(OUTPUT)) + flip("FOO"): assign outB = OUTPUT; + flip("BAR"): assign outB = 0; + flip("BAZ"): assign outB = "HI"; + endcase + + genvar i; + initial outC = 0; + for (i = 0; i != flip(flip(OUTPUT[15:8])); i = i + 1) + if (i + 1 == flip(flip("O"))) + initial outC = 1; + endgenerate + + integer j; + initial begin + outD = 1; + for (j = 0; j != flip(flip(OUTPUT[15:8])); j = j + 1) + if (j + 1 == flip(flip("O"))) + outD = 0; + end +endmodule + +module top(out); + wire [23:0] a1, a2, a3, a4; + wire [23:0] b1, b2, b3, b4; + wire c1, c2, c3, c4; + wire d1, d2, d3, d4; + Example e1(a1, b1, c1, d1); + Example #("FOO") e2(a2, b2, c2, d2); + Example #("BAR") e3(a3, b3, c3, d3); + Example #("BAZ") e4(a4, b4, c4, d4); + + output wire [24 * 8 - 1 + 4 :0] out; + assign out = { + a1, a2, a3, a4, + b1, b2, b3, b4, + c1, c2, c3, c4, + d1, d2, d3, d4}; + +// `define VERIFY +`ifdef VERIFY + assert property (a1 == 0); + assert property (a2 == 0); + assert property (a3 == "BAR"); + assert property (a4 == 0); + assert property (b1 == "FOO"); + assert property (b2 == "FOO"); + assert property (b3 == 0); + assert property (b4 == "HI"); + assert property (c1 == 1); + assert property (c2 == 1); + assert property (c3 == 0); + assert property (c4 == 0); + assert property (d1 == 0); + assert property (d2 == 0); + assert property (d3 == 1); + assert property (d4 == 1); +`endif +endmodule diff --git a/tests/various/const_func.ys b/tests/various/const_func.ys new file mode 100644 index 000000000..5e3c04105 --- /dev/null +++ b/tests/various/const_func.ys @@ -0,0 +1 @@ +read_verilog const_func.v diff --git a/tests/various/signed.ys b/tests/various/signed.ys new file mode 100644 index 000000000..2319a5da1 --- /dev/null +++ b/tests/various/signed.ys @@ -0,0 +1,28 @@ +# SV LRM A2.2.1 + +read_verilog -sv <<EOT +module test_signed(); +parameter integer signed a = 0; +parameter integer unsigned b = 0; + +endmodule +EOT + +design -reset +read_verilog -sv <<EOT +module test_signed(); +parameter logic signed [7:0] a = 0; +parameter logic unsigned [7:0] b = 0; + +endmodule +EOT + +design -reset +logger -expect error "syntax error, unexpected TOK_INTEGER" 1 +read_verilog -sv <<EOT +module test_signed(); +parameter signed integer a = 0; +parameter unsigned integer b = 0; + +endmodule +EOT |