diff options
| -rw-r--r-- | README.md | 9 | ||||
| -rw-r--r-- | examples/smtbmc/demo2.v | 2 | ||||
| -rw-r--r-- | frontends/ast/genrtlil.cc | 4 | ||||
| -rw-r--r-- | frontends/ast/simplify.cc | 2 | ||||
| -rw-r--r-- | frontends/verilog/verilog_parser.y | 4 | ||||
| -rw-r--r-- | kernel/celltypes.h | 2 | ||||
| -rw-r--r-- | kernel/rtlil.cc | 22 | ||||
| -rw-r--r-- | kernel/rtlil.h | 2 | ||||
| -rw-r--r-- | manual/CHAPTER_CellLib.tex | 3 | ||||
| -rw-r--r-- | passes/opt/opt_merge.cc | 2 | ||||
| -rw-r--r-- | techlibs/common/simlib.v | 24 |
11 files changed, 67 insertions, 9 deletions
@@ -387,15 +387,20 @@ Non-standard or SystemVerilog features for formal verification - The system task ``$initstate`` evaluates to 1 in the initial state and to 0 otherwise. -- The system task ``$anyconst`` evaluates to any constant value. This is +- The system function ``$anyconst`` evaluates to any constant value. This is equivalent to declaring a reg as ``rand const``, but also works outside of checkers. (Yosys also supports ``rand const`` outside checkers.) -- The system task ``$anyseq`` evaluates to any value, possibly a different +- The system function ``$anyseq`` evaluates to any value, possibly a different value in each cycle. This is equivalent to declaring a reg as ``rand``, but also works outside of checkers. (Yosys also supports ``rand`` variables outside checkers.) +- The system functions ``$allconst`` and ``$allseq`` are used to construct formal + exist-forall problems. Assertions are only violated if the trace vialoates + the assertion for all ``$allconst/$allseq`` values and assumptions only hold + if the trace satisfies the assumtion for all ``$allconst/$allseq`` values. + - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are supported in any clocked block. diff --git a/examples/smtbmc/demo2.v b/examples/smtbmc/demo2.v index 34745e898..0cf529a42 100644 --- a/examples/smtbmc/demo2.v +++ b/examples/smtbmc/demo2.v @@ -9,7 +9,7 @@ module demo2(input clk, input [4:0] addr, output reg [31:0] data); reg [31:0] mem [0:31]; - always @(posedge clk) + always @(negedge clk) data <= mem[addr]; reg [31:0] used_addr = 0; diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 3b08fc28d..57ba9668d 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -764,7 +764,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun break; case AST_FCALL: - if (str == "\\$anyconst" || str == "\\$anyseq") { + if (str == "\\$anyconst" || str == "\\$anyseq" || str == "\\$allconst" || str == "\\$allseq") { if (GetSize(children) == 1) { while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { } if (children[0]->type != AST_CONSTANT) @@ -1475,7 +1475,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) } break; case AST_FCALL: { - if (str == "\\$anyconst" || str == "\\$anyseq") + if (str == "\\$anyconst" || str == "\\$anyseq" || str == "\\$allconst" || str == "\\$allseq") { string myid = stringf("%s$%d", str.c_str() + 1, autoidx++); int width = width_hint; diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index c454fb907..a16fdfeeb 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1832,7 +1832,7 @@ skip_dynamic_range_lvalue_expansion:; } // $anyconst and $anyseq are mapped in AstNode::genRTLIL() - if (str == "\\$anyconst" || str == "\\$anyseq") { + if (str == "\\$anyconst" || str == "\\$anyseq" || str == "\\$allconst" || str == "\\$allseq") { recursion_counter--; return false; } diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 9aa01c9f0..ba2fc036e 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -1335,7 +1335,9 @@ rvalue: $$ = new AstNode(AST_IDENTIFIER, $2); $$->str = *$1; delete $1; - if ($2 == nullptr && ($$->str == "\\$initstate" || $$->str == "\\$anyconst" || $$->str == "\\$anyseq")) + if ($2 == nullptr && ($$->str == "\\$initstate" || + $$->str == "\\$anyconst" || $$->str == "\\$anyseq" || + $$->str == "\\$allconst" || $$->str == "\\$allseq")) $$->type = AST_FCALL; } | hierarchical_id non_opt_multirange { diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 5218b5363..fcc4fcc4b 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -122,6 +122,8 @@ struct CellTypes setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true); setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true); setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true); + setup_type("$allconst", pool<RTLIL::IdString>(), {Y}, true); + setup_type("$allseq", pool<RTLIL::IdString>(), {Y}, true); setup_type("$equiv", {A, B}, {Y}, true); } diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index fb3d9dbe9..a4fa2cf04 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1101,7 +1101,7 @@ namespace { return; } - if (cell->type.in("$anyconst", "$anyseq")) { + if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq")) { port("\\Y", param("\\WIDTH")); check_expected(); return; @@ -2145,6 +2145,26 @@ RTLIL::SigSpec RTLIL::Module::Anyseq(RTLIL::IdString name, int width, const std: return sig; } +RTLIL::SigSpec RTLIL::Module::Allconst(RTLIL::IdString name, int width, const std::string &src) +{ + RTLIL::SigSpec sig = addWire(NEW_ID, width); + Cell *cell = addCell(name, "$allconst"); + cell->setParam("\\WIDTH", width); + cell->setPort("\\Y", sig); + cell->set_src_attribute(src); + return sig; +} + +RTLIL::SigSpec RTLIL::Module::Allseq(RTLIL::IdString name, int width, const std::string &src) +{ + RTLIL::SigSpec sig = addWire(NEW_ID, width); + Cell *cell = addCell(name, "$allseq"); + cell->setParam("\\WIDTH", width); + cell->setPort("\\Y", sig); + cell->set_src_attribute(src); + return sig; +} + RTLIL::SigSpec RTLIL::Module::Initstate(RTLIL::IdString name, const std::string &src) { RTLIL::SigSpec sig = addWire(NEW_ID); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index a251b4252..54d0b8c22 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1127,6 +1127,8 @@ public: RTLIL::SigSpec Anyconst (RTLIL::IdString name, int width = 1, const std::string &src = ""); RTLIL::SigSpec Anyseq (RTLIL::IdString name, int width = 1, const std::string &src = ""); + RTLIL::SigSpec Allconst (RTLIL::IdString name, int width = 1, const std::string &src = ""); + RTLIL::SigSpec Allseq (RTLIL::IdString name, int width = 1, const std::string &src = ""); RTLIL::SigSpec Initstate (RTLIL::IdString name, const std::string &src = ""); }; diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index c36e61b05..277e89328 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -421,7 +421,8 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber 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}, and {\tt \$anyseq} cells. +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} diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc index 93d9f012f..2aeb514e4 100644 --- a/passes/opt/opt_merge.cc +++ b/passes/opt/opt_merge.cc @@ -279,6 +279,8 @@ struct OptMergeWorker ct.cell_types.erase("$_TBUF_"); ct.cell_types.erase("$anyseq"); ct.cell_types.erase("$anyconst"); + ct.cell_types.erase("$allseq"); + ct.cell_types.erase("$allconst"); log("Finding identical cells in module `%s'.\n", module->name.c_str()); assign_map.set(module); diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index 276503fe8..8e43fe058 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1370,6 +1370,30 @@ endmodule // -------------------------------------------------------- +module \$allconst (Y); + +parameter WIDTH = 0; + +output [WIDTH-1:0] Y; + +assign Y = 'bx; + +endmodule + +// -------------------------------------------------------- + +module \$allseq (Y); + +parameter WIDTH = 0; + +output [WIDTH-1:0] Y; + +assign Y = 'bx; + +endmodule + +// -------------------------------------------------------- + module \$equiv (A, B, Y); input A, B; |