riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3434 from jix/witness_flow 

Updated formal flow with new witness format
This commit is contained in:
Jannis Harder 2022-08-16 14:18:35 +02:00 committed by GitHub
parent c26b2bf543 f7023d06a2
commit 556d008ed3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
33 changed files with 2255 additions and 167 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@ -28,6 +28,9 @@ __pycache__
/yosys-smtbmc
/yosys-smtbmc.exe
/yosys-smtbmc-script.py
/yosys-witness
/yosys-witness.exe
/yosys-witness-script.py
/yosys-filterlib
/yosys-filterlib.exe
/kernel/*.pyh

18
CHANGELOG
View File

@ -4,6 +4,24 @@ List of major changes and improvements between releases
Yosys 0.20 .. Yosys 0.20-dev
--------------------------
* New commands and options
- Added "formalff" pass - transforms FFs for formal verification
- Added option "-formal" to "memory_map" pass
- Added option "-witness" to "rename" - give public names to all signals
present in yosys witness traces
- Added option "-hdlname" to "sim" pass - preserves hiearachy when writing
simulation output for a flattened design
* Formal Verification
- Added $anyinit cell to directly represent FFs with an unconstrained
initialization value. These can be generated by the new formalff pass.
- New JSON based yosys witness format for formal verification traces.
- yosys-smtbmc: Reading and writing of yosys witness traces.
- write_smt2: Emit inline metadata to support yosys witness trace.
- yosys-witness is a new tool to inspect and convert yosys witness traces.
- write_aiger: Option to write a map file for yosys witness trace
conversion.
- yosys-witness: Conversion from and to AIGER witness traces.
Yosys 0.19 .. Yosys 0.20
--------------------------

2
Makefile
View File

@ -155,7 +155,7 @@ bumpversion:
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
ABCREV = 7cc11f7
ABCREV = 20f970f
ABCPULL = 1
ABCURL ?= https://github.com/YosysHQ/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q)

180
backends/aiger/aiger.cc
View File

@ -19,6 +19,7 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
#include "libs/json11/json11.hpp"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@ -61,6 +62,8 @@ struct AigerWriter
dict<SigBit, int> init_inputs;
int initstate_ff = 0;
dict<SigBit, int> ywmap_clocks;
int mkgate(int a0, int a1)
{
aig_m++, aig_a++;
@ -159,6 +162,17 @@ struct AigerWriter
output_bits.insert(wirebit);
}
}
if (wire->width == 1) {
auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
if (gclk_attr != wire->attributes.end()) {
SigBit bit = sigmap(wire);
if (gclk_attr->second == State::S1)
ywmap_clocks[bit] |= 1;
else if (gclk_attr->second == State::S0)
ywmap_clocks[bit] |= 2;
}
}
}
for (auto bit : input_bits)
@ -186,6 +200,22 @@ struct AigerWriter
unused_bits.erase(D);
undriven_bits.erase(Q);
ff_map[Q] = D;
if (cell->type != ID($_FF_)) {
auto sig_clk = sigmap(cell->getPort(ID::CLK).as_bit());
ywmap_clocks[sig_clk] |= cell->type == ID($_DFF_N_) ? 2 : 1;
}
continue;
}
if (cell->type == ID($anyinit))
{
auto sig_d = sigmap(cell->getPort(ID::D));
auto sig_q = sigmap(cell->getPort(ID::Q));
for (int i = 0; i < sig_d.size(); i++) {
undriven_bits.erase(sig_q[i]);
ff_map[sig_q[i]] = sig_d[i];
}
continue;
}
@ -678,6 +708,137 @@ struct AigerWriter
for (auto &it : wire_lines)
f << it.second;
}
template<class T> static std::vector<std::string> witness_path(T *obj) {
std::vector<std::string> path;
if (obj->name.isPublic()) {
auto hdlname = obj->get_string_attribute(ID::hdlname);
for (auto token : split_tokens(hdlname))
path.push_back("\\" + token);
}
if (path.empty())
path.push_back(obj->name.str());
return path;
}
void write_ywmap(std::ostream &f)
{
f << "{\n";
f << " \"version\": \"Yosys Witness Aiger Map\",\n";
f << stringf(" \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str());
f << stringf(" \"latch_count\": %d,\n", aig_l);
f << stringf(" \"input_count\": %d,\n", aig_i);
dict<int, string> clock_lines;
dict<int, string> input_lines;
dict<int, string> init_lines;
dict<int, string> seq_lines;
for (auto cell : module->cells())
{
if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_), ID($anyinit), ID($anyconst), ID($anyseq)))
{
// Use sig_q to get the FF output name, but sig to lookup aiger bits
auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q);
SigSpec sig = sigmap(sig_qy);
for (int i = 0; i < GetSize(sig_qy); i++) {
if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr)
continue;
auto wire = sig_qy[i].wire;
if (init_inputs.count(sig[i])) {
int a = init_inputs.at(sig[i]);
log_assert((a & 1) == 0);
init_lines[a] += json11::Json(json11::Json::object {
{ "path", witness_path(wire) },
{ "input", (a >> 1) - 1 },
{ "offset", sig_qy[i].offset },
}).dump();
}
if (input_bits.count(sig[i])) {
int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0);
seq_lines[a] += json11::Json(json11::Json::object {
{ "path", witness_path(wire) },
{ "input", (a >> 1) - 1 },
{ "offset", sig_qy[i].offset },
}).dump();
}
}
}
}
for (auto wire : module->wires())
{
SigSpec sig = sigmap(wire);
if (wire->port_input)
{
auto path = witness_path(wire);
for (int i = 0; i < GetSize(wire); i++) {
if (aig_map.count(sig[i]) == 0 || sig[i].wire == nullptr)
continue;
int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0);
input_lines[a] += json11::Json(json11::Json::object {
{ "path", path },
{ "input", (a >> 1) - 1 },
{ "offset", i },
}).dump();
if (ywmap_clocks.count(sig[i])) {
int clock_mode = ywmap_clocks[sig[i]];
if (clock_mode != 3) {
clock_lines[a] += json11::Json(json11::Json::object {
{ "path", path },
{ "input", (a >> 1) - 1 },
{ "offset", i },
{ "edge", clock_mode == 1 ? "posedge" : "negedge" },
}).dump();
}
}
}
}
}
f << " \"clocks\": [";
clock_lines.sort();
const char *sep = "\n ";
for (auto &it : clock_lines) {
f << sep << it.second;
sep = ",\n ";
}
f << "\n ],\n";
f << " \"inputs\": [";
input_lines.sort();
sep = "\n ";
for (auto &it : input_lines) {
f << sep << it.second;
sep = ",\n ";
}
f << "\n ],\n";
f << " \"seqs\": [";
sep = "\n ";
for (auto &it : seq_lines) {
f << sep << it.second;
sep = ",\n ";
}
f << "\n ],\n";
f << " \"inits\": [";
sep = "\n ";
for (auto &it : init_lines) {
f << sep << it.second;
sep = ",\n ";
}
f << "\n ]\n}\n";
}
};
struct AigerBackend : public Backend {
@ -717,6 +878,9 @@ struct AigerBackend : public Backend {
log(" -no-startoffset\n");
log(" make indexes zero based, enable using map files with smt solvers.\n");
log("\n");
log(" -ywmap <filename>\n");
log(" write a map file for conversion to and from yosys witness traces.\n");
log("\n");
log(" -I, -O, -B, -L\n");
log(" If the design contains no input/output/assert/flip-flop then create one\n");
log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n");
@ -736,6 +900,7 @@ struct AigerBackend : public Backend {
bool lmode = false;
bool no_startoffset = false;
std::string map_filename;
std::string yw_map_filename;
log_header(design, "Executing AIGER backend.\n");
@ -767,6 +932,10 @@ struct AigerBackend : public Backend {
verbose_map = true;
continue;
}
if (yw_map_filename.empty() && args[argidx] == "-ywmap" && argidx+1 < args.size()) {
yw_map_filename = args[++argidx];
continue;
}
if (args[argidx] == "-no-startoffset") {
no_startoffset = true;
continue;
@ -791,6 +960,9 @@ struct AigerBackend : public Backend {
}
extra_args(f, filename, args, argidx, !ascii_mode);
if (!yw_map_filename.empty() && !zinit_mode)
log_error("Currently -ywmap requires -zinit.\n");
Module *top_module = design->top_module();
if (top_module == nullptr)
@ -815,6 +987,14 @@ struct AigerBackend : public Backend {
log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
writer.write_map(mapf, verbose_map, no_startoffset);
}
if (!yw_map_filename.empty()) {
std::ofstream mapf;
mapf.open(yw_map_filename.c_str(), std::ofstream::trunc);
if (mapf.fail())
log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
writer.write_ywmap(mapf);
}
}
} AigerBackend;

12
backends/btor/btor.cc
View File

@ -612,7 +612,7 @@ struct BtorWorker
goto okay;
}
if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
if (cell->type.in(ID($dff), ID($ff), ID($anyinit), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
{
SigSpec sig_d = sigmap(cell->getPort(ID::D));
SigSpec sig_q = sigmap(cell->getPort(ID::Q));
@ -1112,6 +1112,16 @@ struct BtorWorker
btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str());
add_nid_sig(nid, sig);
if (!info_filename.empty()) {
auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
if (gclk_attr != wire->attributes.end()) {
if (gclk_attr->second == State::S1)
info_clocks[nid] |= 1;
else if (gclk_attr->second == State::S0)
info_clocks[nid] |= 2;
}
}
}
btorf_pop("inputs");

16
backends/smt2/Makefile.inc
View File

@ -7,6 +7,7 @@ ifneq ($(CONFIG),emcc)
# MSYS targets support yosys-smtbmc, but require a launcher script
ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc.exe $(PROGRAM_PREFIX)yosys-smtbmc-script.py
TARGETS += $(PROGRAM_PREFIX)yosys-witness.exe $(PROGRAM_PREFIX)yosys-witness-script.py
# Needed to find the Python interpreter for yosys-smtbmc scripts.
# Override if necessary, it is only used for msys2 targets.
PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
@ -15,18 +16,31 @@ $(PROGRAM_PREFIX)yosys-smtbmc-script.py: backends/smt2/smtbmc.py
$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
$(PROGRAM_PREFIX)yosys-witness-script.py: backends/smt2/witness.py
$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
$(PROGRAM_PREFIX)yosys-smtbmc.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-smtbmc-script.py
$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
$(PROGRAM_PREFIX)yosys-witness.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-witness-script.py
$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
# Other targets
else
TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc
TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc $(PROGRAM_PREFIX)yosys-witness
$(PROGRAM_PREFIX)yosys-smtbmc: backends/smt2/smtbmc.py
$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
$(Q) chmod +x $@.new
$(Q) mv $@.new $@
$(PROGRAM_PREFIX)yosys-witness: backends/smt2/witness.py
$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
$(Q) chmod +x $@.new
$(Q) mv $@.new $@
endif
$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
$(eval $(call add_share_file,share/python3,backends/smt2/ywio.py))
endif
endif

152
backends/smt2/smt2.cc
View File

@ -23,6 +23,7 @@
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include "kernel/mem.h"
#include "libs/json11/json11.hpp"
#include <string>
USING_YOSYS_NAMESPACE
@ -239,6 +240,17 @@ struct Smt2Worker
clock_negedge.erase(bit);
}
for (auto wire : module->wires())
{
auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
if (gclk_attr != wire->attributes.end()) {
if (gclk_attr->second == State::S1)
clock_posedge.insert(sigmap(wire));
else if (gclk_attr->second == State::S0)
clock_negedge.insert(sigmap(wire));
}
}
for (auto wire : module->wires())
{
if (!wire->port_input || GetSize(wire) != 1)
@ -577,31 +589,41 @@ struct Smt2Worker
if (cell->type.in(ID($ff), ID($dff)))
{
registers.insert(cell);
for (auto chunk : cell->getPort(ID::Q).chunks())
if (chunk.is_wire())
decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire));
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
register_bv(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
return;
}
if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq)))
if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq)))
{
auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
registers.insert(cell);
string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
if (cell->attributes.count(ID::reg))
infostr += " " + cell->attributes.at(ID::reg).decode_string();
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str()));
if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(QY)), infostr.c_str()));
if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::maximize)){
decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
log("Wire %s is maximized\n", cell->getPort(QY).as_wire()->name.str().c_str());
}
else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){
else if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::minimize)){
decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
log("Wire %s is minimized\n", cell->getPort(QY).as_wire()->name.str().c_str());
}
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y)));
bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
for (auto chunk : cell->getPort(QY).chunks())
if (chunk.is_wire())
decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire));
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY)));
if (cell->type == ID($anyseq))
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
register_bv(cell->getPort(ID::Y), idcounter++);
register_bv(cell->getPort(QY), idcounter++);
recursive_cells.erase(cell);
return;
}
@ -748,6 +770,7 @@ struct Smt2Worker
log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
decls.push_back(witness_memory(get_id(mem->memid), cell, mem));
string memstate;
if (has_async_wr) {
@ -840,6 +863,7 @@ struct Smt2Worker
if (m != nullptr)
{
decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
decls.push_back(witness_cell(get_id(cell->name), cell));
string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
for (auto &conn : cell->connections())
@ -920,7 +944,7 @@ struct Smt2Worker
pool<SigBit> reg_bits;
for (auto cell : module->cells())
if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_), ID($anyinit))) {
// not using sigmap -- we want the net directly at the dff output
for (auto bit : cell->getPort(ID::Q))
reg_bits.insert(bit);
@ -938,14 +962,19 @@ struct Smt2Worker
for (auto wire : module->wires()) {
bool is_register = false;
for (auto bit : SigSpec(wire))
bool contains_clock = false;
for (auto bit : SigSpec(wire)) {
if (reg_bits.count(bit))
is_register = true;
auto sig_bit = sigmap(bit);
if (clock_posedge.count(sig_bit) || clock_negedge.count(sig_bit))
contains_clock = true;
}
bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
if (is_smtlib2_comb_expr && !is_smtlib2_module)
log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
log_id(wire));
if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
if (wire->port_id || is_register || contains_clock || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
RTLIL::SigSpec sig = sigmap(wire);
std::vector<std::string> comments;
if (wire->port_input)
@ -956,9 +985,20 @@ struct Smt2Worker
comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic()))
comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
if (contains_clock) {
for (int i = 0; i < GetSize(sig); i++) {
bool is_posedge = clock_posedge.count(sig[i]);
bool is_negedge = clock_negedge.count(sig[i]);
if (is_posedge != is_negedge)
comments.push_back(witness_signal(
is_posedge ? "posedge" : "negedge", 1, i, get_id(wire), -1, wire));
}
}
if (wire->port_input)
comments.push_back(witness_signal("input", wire->width, 0, get_id(wire), -1, wire));
std::string smtlib2_comb_expr;
if (is_smtlib2_comb_expr) {
smtlib2_comb_expr =
@ -968,6 +1008,8 @@ struct Smt2Worker
if (!bvmode && GetSize(sig) > 1)
log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
log_id(module), log_id(wire));
comments.push_back(witness_signal("blackbox", wire->width, 0, get_id(wire), -1, wire));
}
auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
if (bvmode && GetSize(sig) > 1) {
@ -1136,7 +1178,7 @@ struct Smt2Worker
ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str()));
}
if (cell->type.in(ID($ff), ID($dff)))
if (cell->type.in(ID($ff), ID($dff), ID($anyinit)))
{
std::string expr_d = get_bv(cell->getPort(ID::D));
std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state");
@ -1435,6 +1477,90 @@ struct Smt2Worker
f << "true)";
f << stringf(" ; end of module %s\n", get_id(module));
}
template<class T> static std::vector<std::string> witness_path(T *obj) {
std::vector<std::string> path;
if (obj->name.isPublic()) {
auto hdlname = obj->get_string_attribute(ID::hdlname);
for (auto token : split_tokens(hdlname))
path.push_back("\\" + token);
}
if (path.empty())
path.push_back(obj->name.str());
return path;
}
std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire)
{
std::vector<std::string> hiername;
const char *wire_name = wire->name.c_str();
if (wire_name[0] == '\\') {
auto hdlname = wire->get_string_attribute(ID::hdlname);
for (auto token : split_tokens(hdlname))
hiername.push_back("\\" + token);
}
if (hiername.empty())
hiername.push_back(wire->name.str());
std::string line = "; yosys-smt2-witness ";
(json11::Json { json11::Json::object {
{ "type", type },
{ "offset", offset },
{ "width", width },
{ "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
{ "path", witness_path(wire) },
}}).dump(line);
line += "\n";
return line;
}
std::string witness_cell(const char *smtname, RTLIL::Cell *cell)
{
std::string line = "; yosys-smt2-witness ";
(json11::Json {json11::Json::object {
{ "type", "cell" },
{ "smtname", smtname },
{ "path", witness_path(cell) },
}}).dump(line);
line += "\n";
return line;
}
std::string witness_memory(const char *smtname, RTLIL::Cell *cell, Mem *mem)
{
json11::Json::array uninitialized;
auto init_data = mem->get_init_data();
int cursor = 0;
while (cursor < init_data.size()) {
while (cursor < init_data.size() && init_data[cursor] != State::Sx)
cursor++;
int offset = cursor;
while (cursor < init_data.size() && init_data[cursor] == State::Sx)
cursor++;
int width = cursor - offset;
if (width)
uninitialized.push_back(json11::Json::object {
{"width", width},
{"offset", offset},
});
}
std::string line = "; yosys-smt2-witness ";
(json11::Json { json11::Json::object {
{ "type", "mem" },
{ "width", mem->width },
{ "size", mem->size },
{ "rom", mem->wr_ports.empty() },
{ "statebv", statebv },
{ "smtname", smtname },
{ "uninitialized", uninitialized },
{ "path", witness_path(cell) },
}}).dump(line);
line += "\n";
return line;
}
};
struct Smt2Backend : public Backend {

439
backends/smt2/smtbmc.py
View File

@ -17,9 +17,10 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import os, sys, getopt, re
import os, sys, getopt, re, bisect
##yosys-sys-path##
from smtio import SmtIo, SmtOpts, MkVcd
from ywio import ReadWitness, WriteWitness, WitnessValues
from collections import defaultdict
got_topt = False
@ -28,6 +29,8 @@ step_size = 1
num_steps = 20
append_steps = 0
vcdfile = None
inywfile = None
outywfile = None
cexfile = None
aimfile = None
aiwfile = None
@ -51,6 +54,7 @@ smtctop = None
noinit = False
binarymode = False
keep_going = False
check_witness = False
so = SmtOpts()
@ -94,6 +98,9 @@ def usage():
the AIGER witness file does not include the status and
properties lines.
--yw <yosys_witness_filename>
read a Yosys witness.
--btorwit <btor_witness_filename>
read a BTOR witness.
@ -121,6 +128,9 @@ def usage():
(hint: use 'write_smt2 -wires' for maximum
coverage of signals in generated VCD file)
--dump-yw <yw_filename>
write trace as a Yosys witness trace
--dump-vlogtb <verilog_filename>
write trace as Verilog test bench
@ -161,15 +171,19 @@ def usage():
covering all found failed assertions, the character '%' is
replaced in all dump filenames with an increasing number.
--check-witness
check that the used witness file contains sufficient
constraints to force an assertion failure.
""" + so.helpmsg())
sys.exit(1)
try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
"dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit", "binary", "keep-going"])
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
"dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
"smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"])
except:
usage()
@ -204,10 +218,14 @@ for o, a in opts:
aiwfile = a + ".aiw"
elif o == "--aig-noheader":
aigheader = False
elif o == "--yw":
inywfile = a
elif o == "--btorwit":
btorwitfile = a
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-yw":
outywfile = a
elif o == "--dump-vlogtb":
vlogtbfile = a
elif o == "--vlogtb-top":
@ -244,6 +262,8 @@ for o, a in opts:
binarymode = True
elif o == "--keep-going":
keep_going = True
elif o == "--check-witness":
check_witness = True
elif so.handle(o, a):
pass
else:
@ -462,7 +482,8 @@ if cexfile is not None:
constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
skip_steps = max(skip_steps, step)
if not check_witness:
skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1)
if aimfile is not None:
@ -595,13 +616,119 @@ if aimfile is not None:
constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
skip_steps = max(skip_steps, step)
if not check_witness:
skip_steps = max(skip_steps, step)
# some solvers optimize the properties so that they fail one cycle early,
# thus we check the properties in the cycle the aiger witness ends, and
# if that doesn't work, we check the cycle after that as well.
num_steps = max(num_steps, step+2)
step += 1
if inywfile is not None:
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0
with open(inywfile, "r") as f:
inyw = ReadWitness(f)
inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True)
smt_wires = defaultdict(list)
smt_mems = defaultdict(list)
for wire in inits + seqs:
smt_wires[wire["path"]].append(wire)
for mem in mems:
smt_mems[mem["path"]].append(mem)
addr_re = re.compile(r'\\\[[0-9]+\]$')
bits_re = re.compile(r'[01?]*$')
for t, step in inyw.steps():
present_signals, missing = step.present_signals(inyw.sigmap)
for sig in present_signals:
bits = step[sig]
if not bits_re.match(bits):
raise ValueError("unsupported bit value in Yosys witness file")
sig_end = sig.offset + len(bits)
if sig.path in smt_wires:
for wire in smt_wires[sig.path]:
width, offset = wire["width"], wire["offset"]
smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1
offset = max(offset, 0)
end = width + offset
common_offset = max(sig.offset, offset)
common_end = min(sig_end, end)
if common_end <= common_offset:
continue
smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"])
if not smt_bool:
slice_high = common_end - offset - 1
slice_low = common_offset - offset
smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr)
bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)]
if bit_slice.count("?") == len(bit_slice):
continue
if smt_bool:
assert width == 1
smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false")
else:
if "?" in bit_slice:
mask = bit_slice.replace("0", "1").replace("?", "0")
bit_slice = bit_slice.replace("?", "0")
smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
constr_assumes[t].append((inywfile, smt_constr))
if sig.memory_path:
if sig.memory_path in smt_mems:
for mem in smt_mems[sig.memory_path]:
width, size, bv = mem["width"], mem["size"], mem["statebv"]
smt_expr = smt.net_expr(topmod, f"s{t}", mem["smtpath"])
if bv:
word_low = sig.memory_addr * width
word_high = word_low + width - 1
smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr)
else:
addr_width = (size - 1).bit_length()
addr_bits = f"{sig.memory_addr:0{addr_width}b}"
smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits)
if len(bits) < width:
slice_high = sig.offset + len(bits) - 1
smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
bit_slice = bits
if "?" in bit_slice:
mask = bit_slice.replace("0", "1").replace("?", "0")
bit_slice = bit_slice.replace("?", "0")
smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
constr_assumes[t].append((inywfile, smt_constr))
if not got_topt:
if not check_witness:
skip_steps = max(skip_steps, t)
num_steps = max(num_steps, t+1)
if btorwitfile is not None:
with open(btorwitfile, "r") as f:
step = None
@ -699,6 +826,115 @@ if btorwitfile is not None:
skip_steps = step
num_steps = step+1
def collect_mem_trace_data(steps_start, steps_stop, vcd=None):
mem_trace_data = dict()
for mempath in sorted(smt.hiermems(topmod)):
abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
expr_id = list()
expr_list = list()
for i in range(steps_start, steps_stop):
for j in range(rports):
expr_id.append(('R', i-steps_start, j, 'A'))
expr_id.append(('R', i-steps_start, j, 'D'))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
for j in range(wports):
expr_id.append(('W', i-steps_start, j, 'A'))
expr_id.append(('W', i-steps_start, j, 'D'))
expr_id.append(('W', i-steps_start, j, 'M'))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
rdata = list()
wdata = list()
addrs = set()
for eid, edat in zip(expr_id, smt.get_list(expr_list)):
t, i, j, f = eid
if t == 'R':
c = rdata
elif t == 'W':
c = wdata
else:
assert False
while len(c) <= i:
c.append(list())
c = c[i]
while len(c) <= j:
c.append(dict())
c = c[j]
c[f] = smt.bv2bin(edat)
if f == 'A':
addrs.add(c[f])
for addr in addrs:
tdata = list()
data = ["x"] * width
gotread = False
if len(wdata) == 0 and len(rdata) != 0:
wdata = [[]] * len(rdata)
assert len(rdata) == len(wdata)
for i in range(len(wdata)):
if not gotread:
for j_data in rdata[i]:
if j_data["A"] == addr:
data = list(j_data["D"])
gotread = True
break
if gotread:
buf = data[:]
for ii in reversed(range(len(tdata))):
for k in range(width):
if tdata[ii][k] == "x":
tdata[ii][k] = buf[k]
else:
buf[k] = tdata[ii][k]
if not asyncwr:
tdata.append(data[:])
for j_data in wdata[i]:
if j_data["A"] != addr:
continue
D = j_data["D"]
M = j_data["M"]
for k in range(width):
if M[k] == "1":
data[k] = D[k]
if asyncwr:
tdata.append(data[:])
assert len(tdata) == len(rdata)
int_addr = int(addr, 2)
netpath = mempath[:]
if vcd:
netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int_addr)
vcd.add_net([topmod] + netpath, width)
for i in range(steps_start, steps_stop):
if i not in mem_trace_data:
mem_trace_data[i] = list()
mem_trace_data[i].append((netpath, int_addr, "".join(tdata[i-steps_start])))
return mem_trace_data
def write_vcd_trace(steps_start, steps_stop, index):
filename = vcdfile.replace("%", index)
print_msg("Writing trace to VCD file: %s" % (filename))
@ -720,107 +956,7 @@ def write_vcd_trace(steps_start, steps_stop, index):
vcd.add_clock([topmod] + netpath, edge)
path_list.append(netpath)
mem_trace_data = dict()
for mempath in sorted(smt.hiermems(topmod)):
abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
expr_id = list()
expr_list = list()
for i in range(steps_start, steps_stop):
for j in range(rports):
expr_id.append(('R', i-steps_start, j, 'A'))
expr_id.append(('R', i-steps_start, j, 'D'))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
for j in range(wports):
expr_id.append(('W', i-steps_start, j, 'A'))
expr_id.append(('W', i-steps_start, j, 'D'))
expr_id.append(('W', i-steps_start, j, 'M'))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
rdata = list()
wdata = list()
addrs = set()
for eid, edat in zip(expr_id, smt.get_list(expr_list)):
t, i, j, f = eid
if t == 'R':
c = rdata
elif t == 'W':
c = wdata
else:
assert False
while len(c) <= i:
c.append(list())
c = c[i]
while len(c) <= j:
c.append(dict())
c = c[j]
c[f] = smt.bv2bin(edat)
if f == 'A':
addrs.add(c[f])
for addr in addrs:
tdata = list()
data = ["x"] * width
gotread = False
if len(wdata) == 0 and len(rdata) != 0:
wdata = [[]] * len(rdata)
assert len(rdata) == len(wdata)
for i in range(len(wdata)):
if not gotread:
for j_data in rdata[i]:
if j_data["A"] == addr:
data = list(j_data["D"])
gotread = True
break
if gotread:
buf = data[:]
for ii in reversed(range(len(tdata))):
for k in range(width):
if tdata[ii][k] == "x":
tdata[ii][k] = buf[k]
else:
buf[k] = tdata[ii][k]
if not asyncwr:
tdata.append(data[:])
for j_data in wdata[i]:
if j_data["A"] != addr:
continue
D = j_data["D"]
M = j_data["M"]
for k in range(width):
if M[k] == "1":
data[k] = D[k]
if asyncwr:
tdata.append(data[:])
assert len(tdata) == len(rdata)
netpath = mempath[:]
netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2))
vcd.add_net([topmod] + netpath, width)
for i in range(steps_start, steps_stop):
if i not in mem_trace_data:
mem_trace_data[i] = list()
mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start])))
mem_trace_data = collect_mem_trace_data(steps_start, steps_stop, vcd)
for i in range(steps_start, steps_stop):
vcd.set_time(i)
@ -828,7 +964,7 @@ def write_vcd_trace(steps_start, steps_stop, index):
for path, value in zip(path_list, value_list):
vcd.set_net([topmod] + path, value)
if i in mem_trace_data:
for path, value in mem_trace_data[i]:
for path, addr, value in mem_trace_data[i]:
vcd.set_net([topmod] + path, value)
vcd.set_time(steps_stop)
@ -1072,8 +1208,72 @@ def write_constr_trace(steps_start, steps_stop, index):
for name, val in zip(pi_names, pi_values):
print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
def write_yw_trace(steps_start, steps_stop, index, allregs=False):
filename = outywfile.replace("%", index)
print_msg("Writing trace to Yosys witness file: %s" % (filename))
def write_trace(steps_start, steps_stop, index):
mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
with open(filename, "w") as f:
inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs)
yw = WriteWitness(f, "smtbmc")
for clock in clocks:
yw.add_clock(clock["path"], clock["offset"], clock["type"])
for seq in seqs:
seq["sig"] = yw.add_sig(seq["path"], seq["offset"], seq["width"])
for init in inits:
init["sig"] = yw.add_sig(init["path"], init["offset"], init["width"], True)
inits = seqs + inits
mem_dict = {tuple(mem["smtpath"]): mem for mem in mems}
mem_init_values = []
for path, addr, value in mem_trace_data.get(0, ()):
json_mem = mem_dict.get(tuple(path))
if not json_mem:
continue
bit_addr = addr * json_mem["width"]
uninit_chunks = [(chunk["width"] + chunk["offset"], chunk["offset"]) for chunk in json_mem["uninitialized"]]
first_chunk_nr = bisect.bisect_left(uninit_chunks, (bit_addr + 1,))
for uninit_end, uninit_offset in uninit_chunks[first_chunk_nr:]:
assert uninit_end > bit_addr
if uninit_offset > bit_addr + json_mem["width"]:
break
word_path = (*json_mem["path"], f"\\[{addr}]")
overlap_start = max(uninit_offset - bit_addr, 0)
overlap_end = min(uninit_end - bit_addr, json_mem["width"])
overlap_bits = value[len(value)-overlap_end:len(value)-overlap_start]
sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True)
mem_init_values.append((sig, overlap_bits.replace("x", "?")))
for k in range(steps_start, steps_stop):
step_values = WitnessValues()
if k == steps_start:
for sig, value in mem_init_values:
step_values[sig] = value
sigs = inits + seqs
else:
sigs = seqs
for sig in sigs:
step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"])))
yw.step(step_values)
yw.end_trace()
def write_trace(steps_start, steps_stop, index, allregs=False):
if vcdfile is not None:
write_vcd_trace(steps_start, steps_stop, index)
@ -1083,6 +1283,9 @@ def write_trace(steps_start, steps_stop, index):
if outconstr is not None:
write_constr_trace(steps_start, steps_stop, index)
if outywfile is not None:
write_yw_trace(steps_start, steps_stop, index, allregs)
def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()):
assert mod in smt.modinfo
@ -1392,12 +1595,12 @@ if tempind:
print_msg("Temporal induction failed!")
print_anyconsts(num_steps)
print_failed_asserts(num_steps)
write_trace(step, num_steps+1, '%')
write_trace(step, num_steps+1, '%', allregs=True)
elif dumpall:
print_anyconsts(num_steps)
print_failed_asserts(num_steps)
write_trace(step, num_steps+1, "%d" % step)
write_trace(step, num_steps+1, "%d" % step, allregs=True)
else:
print_msg("Temporal induction successful.")
@ -1590,6 +1793,7 @@ else: # not tempind, covermode
smt_assert("(not %s)" % active_assert_expr)
else:
active_assert_expr = "true"
smt_assert("false")
@ -1597,6 +1801,17 @@ else: # not tempind, covermode
if retstatus != "FAILED":
print("%s BMC failed!" % smt.timestamp())
if check_witness:
print_msg("Checking witness constraints...")
smt_pop()
smt_push()
smt_assert(active_assert_expr)
if smt_check_sat() != "sat":
retstatus = "PASSED"
check_witness = False
num_steps = -1
break
if append_steps > 0:
for i in range(last_check_step+1, last_check_step+1+append_steps):
print_msg("Appending additional step %d." % i)
@ -1689,6 +1904,8 @@ else: # not tempind, covermode
print_anyconsts(0)
write_trace(0, num_steps, '%')
if check_witness:
retstatus = "FAILED"
smt.write("(exit)")
smt.wait()

63
backends/smt2/smtio.py
View File

@ -16,7 +16,7 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import sys, re, os, signal
import sys, re, os, signal, json
import subprocess
if os.name == "posix":
import resource
@ -108,6 +108,7 @@ class SmtModInfo:
self.allconsts = dict()
self.allseqs = dict()
self.asize = dict()
self.witness = []
class SmtIo:
@ -587,6 +588,11 @@ class SmtIo:
self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-witness":
data = json.loads(stmt.split(None, 2)[2])
if data.get("type") in ["cell", "mem", "posedge", "negedge", "input", "reg", "init", "seq", "blackbox"]:
self.modinfo[self.curmod].witness.append(data)
def hiernets(self, top, regs_only=False):
def hiernets_worker(nets, mod, cursor):
for netname in sorted(self.modinfo[mod].wsize.keys()):
@ -658,6 +664,57 @@ class SmtIo:
hiermems_worker(mems, top, [])
return mems
def hierwitness(self, top, allregs=False, blackbox=True):
init_witnesses = []
seq_witnesses = []
clk_witnesses = []
mem_witnesses = []
def absolute(path, cursor, witness):
return {
**witness,
"path": path + tuple(witness["path"]),
"smtpath": cursor + [witness["smtname"]],
}
for witness in self.modinfo[top].witness:
if witness["type"] == "input":
seq_witnesses.append(absolute((), [], witness))
if witness["type"] in ("posedge", "negedge"):
clk_witnesses.append(absolute((), [], witness))
init_types = ["init"]
if allregs:
init_types.append("reg")
seq_types = ["seq"]
if blackbox:
seq_types.append("blackbox")
def worker(mod, path, cursor):
cell_paths = {}
for witness in self.modinfo[mod].witness:
if witness["type"] in init_types:
init_witnesses.append(absolute(path, cursor, witness))
if witness["type"] in seq_types:
seq_witnesses.append(absolute(path, cursor, witness))
if witness["type"] == "mem":
if allregs and not witness["rom"]:
width, size = witness["width"], witness["size"]
witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}}
if not witness["uninitialized"]:
continue
mem_witnesses.append(absolute(path, cursor, witness))
if witness["type"] == "cell":
cell_paths[witness["smtname"]] = tuple(witness["path"])
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
worker(celltype, path + cell_paths.get(cellname, ("?" + cellname,)), cursor + [cellname])
worker(top, (), [])
return init_witnesses, seq_witnesses, clk_witnesses, mem_witnesses
def read(self):
stmt = []
count_brackets = 0
@ -887,6 +944,8 @@ class SmtIo:
assert mod in self.modinfo
if path[0] == "":
return base
if isinstance(path[0], int):
return "(|%s#%d| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].cells:
return "(|%s_h %s| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].wsize:
@ -909,6 +968,8 @@ class SmtIo:
mod = self.modinfo[mod].cells[net_path[i]]
assert mod in self.modinfo
if isinstance(net_path[-1], int):
return None
assert net_path[-1] in self.modinfo[mod].wsize
return self.modinfo[mod].wsize[net_path[-1]]

254
backends/smt2/witness.py Normal file
View File

@ -0,0 +1,254 @@
#!/usr/bin/env python3
#
# yosys -- Yosys Open SYnthesis Suite
#
# Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
#
# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted, provided that the above
# copyright notice and this permission notice appear in all copies.
#
# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import os, sys, itertools, re
##yosys-sys-path##
import json
import click
from ywio import ReadWitness, WriteWitness, WitnessSig, WitnessSigMap, WitnessValues, coalesce_signals
@click.group()
def cli():
pass
@cli.command(help="""
Display a Yosys witness trace in a human readable format.
""")
@click.argument("input", type=click.File("r"))
def display(input):
click.echo(f"Reading Yosys witness trace {input.name!r}...")
inyw = ReadWitness(input)
def output():
yield click.style("*** RTLIL bit-order below may differ from source level declarations ***", fg="red")
if inyw.clocks:
yield click.style("=== Clock Signals ===", fg="blue")
for clock in inyw.clocks:
yield f" {clock['edge']} {WitnessSig(clock['path'], clock['offset']).pretty()}"
for t, values in inyw.steps():
if t:
yield click.style(f"=== Step {t} ===", fg="blue")
else:
yield click.style("=== Initial State ===", fg="blue")
step_prefix = click.style(f"#{t}", fg="bright_black")
signals, missing = values.present_signals(inyw.sigmap)
assert not missing
for sig in signals:
display_bits = values[sig].replace("?", click.style("?", fg="bright_black"))
yield f" {step_prefix} {sig.pretty()} = {display_bits}"
click.echo_via_pager([line + "\n" for line in output()])
@cli.command(help="""
Display statistics of a Yosys witness trace.
""")
@click.argument("input", type=click.File("r"))
def stats(input):
click.echo(f"Reading Yosys witness trace {input.name!r}...")
inyw = ReadWitness(input)
total = 0
for t, values in inyw.steps():
click.echo(f"{t:5}: {len(values.values):8} bits")
total += len(values.values)
click.echo(f"total: {total:8} bits")
@cli.command(help="""
Transform a Yosys witness trace.
Currently no transformations are implemented, so it is only useful for testing.
""")
@click.argument("input", type=click.File("r"))
@click.argument("output", type=click.File("w"))
def yw2yw(input, output):
click.echo(f"Copying yosys witness trace from {input.name!r} to {output.name!r}...")
inyw = ReadWitness(input)
outyw = WriteWitness(output, "yosys-witness yw2yw")
for clock in inyw.clocks:
outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
for sig in inyw.signals:
outyw.add_sig(sig.path, sig.offset, sig.width, sig.init_only)
for t, values in inyw.steps():
outyw.step(values)
outyw.end_trace()
click.echo(f"Copied {outyw.t + 1} time steps.")
class AigerMap:
def __init__(self, mapfile):
data = json.load(mapfile)
self.latch_count = data["latch_count"]
self.input_count = data["input_count"]
self.clocks = data["clocks"]
self.sigmap = WitnessSigMap()
self.init_inputs = set(init["input"] for init in data["inits"])
for bit in data["inputs"] + data["seqs"] + data["inits"]:
self.sigmap.add_bit((tuple(bit["path"]), bit["offset"]), bit["input"])
@cli.command(help="""
Convert an AIGER witness trace into a Yosys witness trace.
This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'.
""")
@click.argument("input", type=click.File("r"))
@click.argument("mapfile", type=click.File("r"))
@click.argument("output", type=click.File("w"))
def aiw2yw(input, mapfile, output):
input_name = input.name
click.echo(f"Converting AIGER witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
aiger_map = AigerMap(mapfile)
header_lines = list(itertools.islice(input, 0, 2))
if len(header_lines) == 2 and header_lines[1][0] in ".bcjf":
status = header_lines[0].strip()
if status == "0":
raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is unsat")
elif status == "2":
raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is sat")
elif status != "1":
raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
else:
input = itertools.chain(header_lines, input)
ffline = next(input, None)
if ffline is None:
raise click.ClickException(f"{input_name}: unexpected end of file")
ffline = ffline.strip()
if not re.match(r'[01x]*$', ffline):
raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
if not re.match(r'[0]*$', ffline):
raise click.ClickException(f"{input_name}: non-default initial state not supported")
outyw = WriteWitness(output, 'yosys-witness aiw2yw')
for clock in aiger_map.clocks:
outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
for (path, offset), id in aiger_map.sigmap.bit_to_id.items():
outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs)
missing = set()
while True:
inline = next(input, None)
if inline is None:
click.echo(f"Warning: {input_name}: file may be incomplete")
break
inline = inline.strip()
if inline in [".", "# DONE"]:
break
if inline.startswith("#"):
continue
if not re.match(r'[01x]*$', ffline):
raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
if len(inline) != aiger_map.input_count:
raise click.ClickException(
f"{input_name}: {mapfile.name}: number of inputs does not match, "
f"{len(inline)} in witness, {aiger_map.input_count} in map file")
values = WitnessValues()
for i, v in enumerate(inline):
if v == "x" or outyw.t > 0 and i in aiger_map.init_inputs:
continue
try:
bit = aiger_map.sigmap.id_to_bit[i]
except IndexError:
bit = None
if bit is None:
missing.insert(i)
values[bit] = v
outyw.step(values)
outyw.end_trace()
if missing:
click.echo("The following AIGER inputs belong to unknown signals:")
click.echo(" " + " ".join(str(id) for id in sorted(missing)))
click.echo(f"Converted {outyw.t} time steps.")
@cli.command(help="""
Convert a Yosys witness trace into an AIGER witness trace.
This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'.
""")
@click.argument("input", type=click.File("r"))
@click.argument("mapfile", type=click.File("r"))
@click.argument("output", type=click.File("w"))
def yw2aiw(input, mapfile, output):
click.echo(f"Converting Yosys witness trace {input.name!r} to AIGER witness trace {output.name!r}...")
click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
aiger_map = AigerMap(mapfile)
inyw = ReadWitness(input)
print("1", file=output)
print("b0", file=output)
# TODO the b0 status isn't really accurate, but we don't have any better info here
print("0" * aiger_map.latch_count, file=output)
all_missing = set()
for t, step in inyw.steps():
bits, missing = step.pack_present(aiger_map.sigmap)
bits = bits[::-1].replace('?', 'x')
all_missing.update(missing)
bits += 'x' * (aiger_map.input_count - len(bits))
print(bits, file=output)
print(".", file=output)
if all_missing:
click.echo("The following signals are missing in the AIGER map file and will be dropped:")
for sig in coalesce_signals(WitnessSig(*bit) for bit in all_missing):
click.echo(" " + sig.pretty())
click.echo(f"Converted {len(inyw)} time steps.")
if __name__ == "__main__":
cli()

392
backends/smt2/ywio.py Normal file
View File

@ -0,0 +1,392 @@
#
# yosys -- Yosys Open SYnthesis Suite
#
# Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
#
# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted, provided that the above
# copyright notice and this permission notice appear in all copies.
#
# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import json, re
from functools import total_ordering
class PrettyJson:
def __init__(self, f):
self.f = f
self.indent = 0
self.state = ["value"]
def line(self):
indent = len(self.state) - bool(self.state and self.state[-1] == "value")
print("\n", end=" " * (2 * indent), file=self.f)
def raw(self, str):
print(end=str, file=self.f)
def begin_object(self):
self.begin_value()
self.raw("{")
self.state.append("object_first")
def begin_array(self):
self.begin_value()
self.raw("[")
self.state.append("array_first")
def end_object(self):
state = self.state.pop()
if state == "object":
self.line()
else:
assert state == "object_first"
self.raw("}")
self.end_value()
def end_array(self):
state = self.state.pop()
if state == "array":
self.line()
else:
assert state == "array_first"
self.raw("]")
self.end_value()
def name(self, name):
if self.state[-1] == "object_first":
self.state[-1] = "object"
else:
self.raw(",")
self.line()
json.dump(str(name), self.f)
self.raw(": ")
self.state.append("value")
def begin_value(self):
if self.state[-1] == "array_first":
self.line()
self.state[-1] = "array"
elif self.state[-1] == "array":
self.raw(",")
self.line()
else:
assert self.state.pop() == "value"
def end_value(self):
if not self.state:
print(file=self.f, flush=True)
def value(self, value):
self.begin_value()
json.dump(value, self.f)
self.end_value()
def entry(self, name, value):
self.name(name)
self.value(value)
def object(self, entries=None):
if isinstance(entries, dict):
entries = dict.items()
self.begin_object()
for name, value in entries:
self.entry(name, value)
self.end_object()
def array(self, values=None):
self.begin_array()
for value in values:
self.value(value)
self.end_array()
addr_re = re.compile(r'\\\[[0-9]+\]$')
public_name_re = re.compile(r"\\([a-zA-Z_][a-zA-Z0-9_]*(\[[0-9]+\])?|\[[0-9]+\])$")
def pretty_name(id):
if public_name_re.match(id):
return id.lstrip("\\")
else:
return id
def pretty_path(path):
out = ""
for name in path:
name = pretty_name(name)
if name.startswith("["):
out += name
continue
if out:
out += "."
if name.startswith("\\") or name.startswith("$"):
out += name + " "
else:
out += name
return out
@total_ordering
class WitnessSig:
def __init__(self, path, offset, width=1, init_only=False):
path = tuple(path)
self.path, self.width, self.offset, self.init_only = path, width, offset, init_only
self.memory_path = None
self.memory_addr = None
sort_path = path
sort_id = -1
if path and addr_re.match(path[-1]):
self.memory_path = sort_path = path[:-1]
self.memory_addr = sort_id = int(path[-1][2:-1])
self.sort_key = (init_only, sort_path, sort_id, offset, width)
def bits(self):
return ((self.path, i) for i in range(self.offset, self.offset + self.width))
def rev_bits(self):
return ((self.path, i) for i in reversed(range(self.offset, self.offset + self.width)))
def pretty(self):
if self.width > 1:
last_offset = self.offset + self.width - 1
return f"{pretty_path(self.path)}[{last_offset}:{self.offset}]"
else:
return f"{pretty_path(self.path)}[{self.offset}]"
def __eq__(self):
return self.sort_key
def __hash__(self):
return hash(self.sort_key)
def __lt__(self, other):
return self.sort_key < other.sort_key
def coalesce_signals(signals):
bits = {}
for sig in signals:
for bit in sig.bits():
if sig.init_only:
bits.setdefault(bit, False)
else:
bits[bit] = True
active = None
out = []
for bit, not_init in sorted(bits.items()):
if active:
if active[0] == bit[0] and active[2] == bit[1] and active[3] == not_init:
active[2] += 1
else:
out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3]))
active = None
if active is None:
active = [bit[0], bit[1], bit[1] + 1, not_init]
if active:
out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3]))
return sorted(out)
class WitnessSigMap:
def __init__(self, signals=[]):
self.signals = []
self.id_to_bit = []
self.bit_to_id = {}
self.bit_to_sig = {}
for sig in signals:
self.add_signal(sig)
def add_signal(self, sig):
self.signals.append(sig)
for bit in sig.bits():
self.add_bit(bit)
self.bit_to_sig[bit] = sig
def add_bit(self, bit, id=None):
if id is None:
id = len(self.id_to_bit)
self.id_to_bit.append(bit)
else:
if len(self.id_to_bit) <= id:
self.id_to_bit += [None] * (id - len(self.id_to_bit) + 1)
self.id_to_bit[id] = bit
self.bit_to_id[bit] = id
class WitnessValues:
def __init__(self):
self.values = {}
def __setitem__(self, key, value):
if isinstance(key, tuple) and len(key) == 2:
if value != "?":
assert isinstance(value, str)
assert len(value) == 1
self.values[key] = value
else:
assert isinstance(key, WitnessSig)
assert key.width == len(value)
if isinstance(value, str):
value = reversed(value)
for bit, bit_value in zip(key.bits(), value):
if bit_value != "?":
self.values[bit] = bit_value
def __getitem__(self, key):
if isinstance(key, tuple) and len(key) == 2:
return self.values.get(key, "?")
else:
assert isinstance(key, WitnessSig)
return "".join([self.values.get(bit, "?") for bit in key.rev_bits()])
def pack_present(self, sigmap):
missing = []
max_id = max((sigmap.bit_to_id.get(bit, -1) for bit in self.values), default=-1)
vector = ["?"] * (max_id + 1)
for bit, bit_value in self.values.items():
id = sigmap.bit_to_id.get(bit, - 1)
if id < 0:
missing.append(bit)
else:
vector[max_id - sigmap.bit_to_id[bit]] = bit_value
return "".join(vector), missing
def pack(self, sigmap):
packed, missing = self.pack_present(sigmap)
if missing:
raise RuntimeError(f"Cannot pack bits {missing!r}")
return packed
def unpack(self, sigmap, bits):
for i, bit_value in enumerate(reversed(bits)):
if bit_value != "?":
self.values[sigmap.id_to_bit[i]] = bit_value
def present_signals(self, sigmap):
signals = set(sigmap.bit_to_sig.get(bit) for bit in self.values)
missing_signals = None in signals
if missing_signals:
signals.discard(None)
return sorted(signals), missing_signals
class WriteWitness:
def __init__(self, f, generator):
self.out = PrettyJson(f)
self.t = 0
self.header_written = False
self.clocks = []
self.signals = []
self.out.begin_object()
self.out.entry("format", "Yosys Witness Trace")
self.out.entry("generator", generator)
def add_clock(self, path, offset, edge):
assert not self.header_written
self.clocks.append({
"path": path,
"edge": edge,
"offset": offset,
})
def add_sig(self, path, offset, width=1, init_only=False):
assert not self.header_written
sig = WitnessSig(path, offset, width, init_only)
self.signals.append(sig)
return sig
def write_header(self):
assert not self.header_written
self.header_written = True
self.out.name("clocks")
self.out.array(self.clocks)
self.signals = coalesce_signals(self.signals)
self.sigmap = WitnessSigMap(self.signals)
self.out.name("signals")
self.out.array({
"path": sig.path,
"width": sig.width,
"offset": sig.offset,
"init_only": sig.init_only,
} for sig in self.signals)
self.out.name("steps")
self.out.begin_array()
def step(self, values):
if not self.header_written:
self.write_header()
self.out.value({"bits": values.pack(self.sigmap)})
self.t += 1
def end_trace(self):
if not self.header_written:
self.write_header()
self.out.end_array()
self.out.end_object()
class ReadWitness:
def __init__(self, f):
data = json.load(f)
if not isinstance(data, dict):
data = {}
data_format = data.get("format", "Unknown Format")
if data_format != "Yosys Witness Trace":
raise ValueError(f"unsupported format {data_format!r}")
self.clocks = data["clocks"]
for clock in self.clocks:
clock["path"] = tuple(clock["path"])
self.signals = [
WitnessSig(sig["path"], sig["offset"], sig["width"], sig["init_only"])
for sig in data["signals"]
]
self.sigmap = WitnessSigMap(self.signals)
self.bits = [step["bits"] for step in data["steps"]]
def step(self, t):
values = WitnessValues()
values.unpack(self.sigmap, self.bits[t])
return values
def steps(self):
for i in range(len(self.bits)):
yield i, self.step(i)
def __len__(self):
return len(self.bits)

6
kernel/celltypes.h
View File

@ -51,6 +51,7 @@ struct CellTypes
setup_internals();
setup_internals_mem();
setup_internals_anyinit();
setup_stdcells();
setup_stdcells_mem();
}
@ -155,6 +156,11 @@ struct CellTypes
setup_type(ID($dlatchsr), {ID::EN, ID::SET, ID::CLR, ID::D}, {ID::Q});
}
void setup_internals_anyinit()
{
setup_type(ID($anyinit), {ID::D}, {ID::Q});
}
void setup_internals_mem()
{
setup_internals_ff();

1
kernel/constids.inc
View File

@ -171,6 +171,7 @@ X(RD_TRANSPARENCY_MASK)
X(RD_TRANSPARENT)
X(RD_WIDE_CONTINUATION)
X(reg)
X(replaced_by_gclk)
X(reprocess_after)
X(rom_block)
X(rom_style)

19
kernel/ff.cc
View File

@ -33,10 +33,14 @@ FfData::FfData(FfInitVals *initvals, Cell *cell_) : FfData(cell_->module, initva
std::string type_str = cell->type.str();
if (cell->type.in(ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) {
if (cell->type == ID($ff)) {
if (cell->type.in(ID($anyinit), ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) {
if (cell->type.in(ID($anyinit), ID($ff))) {
has_gclk = true;
sig_d = cell->getPort(ID::D);
if (cell->type == ID($anyinit)) {
is_anyinit = true;
log_assert(val_init.is_fully_undef());
}
} else if (cell->type == ID($sr)) {
// No data input at all.
} else if (cell->type.in(ID($dlatch), ID($adlatch), ID($dlatchsr))) {
@ -274,6 +278,7 @@ FfData FfData::slice(const std::vector<int> &bits) {
res.has_sr = has_sr;
res.ce_over_srst = ce_over_srst;
res.is_fine = is_fine;
res.is_anyinit = is_anyinit;
res.pol_clk = pol_clk;
res.pol_ce = pol_ce;
res.pol_aload = pol_aload;
@ -542,7 +547,7 @@ Cell *FfData::emit() {
return nullptr;
}
}
if (initvals)
if (initvals && !is_anyinit)
initvals->set_init(sig_q, val_init);
if (!is_fine) {
if (has_gclk) {
@ -552,7 +557,12 @@ Cell *FfData::emit() {
log_assert(!has_arst);
log_assert(!has_srst);
log_assert(!has_sr);
cell = module->addFf(name, sig_d, sig_q);
if (is_anyinit) {
cell = module->addAnyinit(name, sig_d, sig_q);
log_assert(val_init.is_fully_undef());
} else {
cell = module->addFf(name, sig_d, sig_q);
}
} else if (!has_aload && !has_clk) {
log_assert(has_sr);
cell = module->addSr(name, sig_set, sig_clr, sig_q, pol_set, pol_clr);
@ -603,6 +613,7 @@ Cell *FfData::emit() {
log_assert(!has_arst);
log_assert(!has_srst);
log_assert(!has_sr);
log_assert(!is_anyinit);
cell = module->addFfGate(name, sig_d, sig_q);
} else if (!has_aload && !has_clk) {
log_assert(has_sr);

8
kernel/ff.h
View File

@ -28,7 +28,10 @@ YOSYS_NAMESPACE_BEGIN
// Describes a flip-flop or a latch.
//
// If has_gclk, this is a formal verification FF with implicit global clock:
// Q is simply previous cycle's D.
// Q is simply previous cycle's D. Additionally if is_anyinit is true, this is
// an $anyinit cell which always has an undefined initialization value. Note
// that $anyinit is not considered to be among the FF celltypes, so a pass has
// to explicitly opt-in to process $anyinit cells with FfData.
//
// Otherwise, the FF/latch can have any number of features selected by has_*
// attributes that determine Q's value (in order of decreasing priority):
@ -126,6 +129,8 @@ struct FfData {
// True if this FF is a fine cell, false if it is a coarse cell.
// If true, width must be 1.
bool is_fine;
// True if this FF is an $anyinit cell. Depends on has_gclk.
bool is_anyinit;
// Polarities, corresponding to sig_*. True means active-high, false
// means active-low.
bool pol_clk;
@ -156,6 +161,7 @@ struct FfData {
has_sr = false;
ce_over_srst = false;
is_fine = false;
is_anyinit = false;
pol_clk = false;
pol_aload = false;
pol_ce = false;

17
kernel/rtlil.cc
View File

@ -1632,6 +1632,13 @@ namespace {
return;
}
if (cell->type.in(ID($anyinit))) {
port(ID::D, param(ID::WIDTH));
port(ID::Q, param(ID::WIDTH));
check_expected();
return;
}
if (cell->type == ID($equiv)) {
port(ID::A, 1);
port(ID::B, 1);
@ -3120,6 +3127,16 @@ RTLIL::Cell* RTLIL::Module::addDlatchsrGate(RTLIL::IdString name, const RTLIL::S
return cell;
}
RTLIL::Cell* RTLIL::Module::addAnyinit(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, ID($anyinit));
cell->parameters[ID::WIDTH] = sig_q.size();
cell->setPort(ID::D, sig_d);
cell->setPort(ID::Q, sig_q);
cell->set_src_attribute(src);
return cell;
}
RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width, const std::string &src)
{
RTLIL::SigSpec sig = addWire(NEW_ID, width);

2
kernel/rtlil.h
View File

@ -1375,6 +1375,8 @@ public:
RTLIL::Cell* addDlatchsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addAnyinit(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src = "");
// The methods without the add* prefix create a cell and an output signal. They return the newly created output signal.
RTLIL::SigSpec Not (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, bool is_signed = false, const std::string &src = "");

2
kernel/satgen.cc
View File

@ -1176,7 +1176,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
return true;
}
if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type))
if (timestep > 0 && (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)))
{
FfData ff(nullptr, cell);

2
manual/CHAPTER_CellLib.tex
View File

@ -603,7 +603,7 @@ Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} c
\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.
{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$anyinit}, {\tt \$allconst}, {\tt \$allseq} cells.
\end{fixme}
\begin{fixme}

81
passes/cmds/rename.cc
View File

@ -106,6 +106,60 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, strin
return name + suffix;
}
static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &cache, RTLIL::Module *module)
{
auto cached = cache.find(module);
if (cached != cache.end()) {
if (cached->second == -1)
log_error("Cannot rename witness signals in a design containing recursive instantiations.\n");
return cached->second;
}
cache.emplace(module, -1);
bool has_witness_signals = false;
for (auto cell : module->cells())
{
RTLIL::Module *impl = design->module(cell->type);
if (impl != nullptr) {
bool witness_in_cell = rename_witness(design, cache, impl);
has_witness_signals |= witness_in_cell;
if (witness_in_cell && !cell->name.isPublic()) {
std::string name = cell->name.c_str() + 1;
for (auto &c : name)
if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
c = '_';
auto new_id = module->uniquify("\\_witness_." + name);
cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
module->rename(cell, new_id);
}
}
if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
has_witness_signals = true;
auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
auto sig_out = cell->getPort(QY);
for (auto chunk : sig_out.chunks()) {
if (chunk.is_wire() && !chunk.wire->name.isPublic()) {
std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1);
for (auto &c : name)
if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
c = '_';
auto new_id = module->uniquify("\\_witness_." + name);
auto new_wire = module->addWire(new_id, GetSize(sig_out));
new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
module->connect({sig_out, new_wire});
cell->setPort(QY, new_wire);
break;
}
}
}
}
cache[module] = has_witness_signals;
return has_witness_signals;
}
struct RenamePass : public Pass {
RenamePass() : Pass("rename", "rename object in the design") { }
void help() override
@ -147,6 +201,14 @@ struct RenamePass : public Pass {
log("pattern is '_%%_'.\n");
log("\n");
log("\n");
log(" rename -witness\n");
log("\n");
log("Assigns auto-generated names to all $any*/$all* output wires and containing\n");
log("cells that do not have a public name. This ensures that, during formal\n");
log("verification, a solver-found trace can be fully specified using a public\n");
log("hierarchical names.\n");
log("\n");
log("\n");
log(" rename -hide [selection]\n");
log("\n");
log("Assign private names (the ones with $-prefix) to all selected wires and cells\n");
@ -172,6 +234,7 @@ struct RenamePass : public Pass {
bool flag_src = false;
bool flag_wire = false;
bool flag_enumerate = false;
bool flag_witness = false;
bool flag_hide = false;
bool flag_top = false;
bool flag_output = false;
@ -203,6 +266,11 @@ struct RenamePass : public Pass {
got_mode = true;
continue;
}
if (arg == "-witness" && !got_mode) {
flag_witness = true;
got_mode = true;
continue;
}
if (arg == "-hide" && !got_mode) {
flag_hide = true;
got_mode = true;
@ -309,6 +377,19 @@ struct RenamePass : public Pass {
}
}
else
if (flag_witness)
{
extra_args(args, argidx, design, false);
RTLIL::Module *module = design->top_module();
if (module == nullptr)
log_cmd_error("No top module found!\n");
dict<RTLIL::Module *, int> cache;
rename_witness(design, cache, module);
}
else
if (flag_hide)
{
extra_args(args, argidx, design);

24
passes/cmds/setundef.cc
View File

@ -20,6 +20,7 @@
#include "kernel/register.h"
#include "kernel/celltypes.h"
#include "kernel/sigtools.h"
#include "kernel/mem.h"
#include "kernel/rtlil.h"
#include "kernel/log.h"
@ -478,6 +479,29 @@ struct SetundefPass : public Pass {
log_assert(ffbits.empty());
}
if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
{
// Do not add anyseq / anyconst to unused memory port clocks
std::vector<Mem> memories = Mem::get_selected_memories(module);
for (auto &mem : memories) {
bool changed = false;
for (auto &rd_port : mem.rd_ports) {
if (!rd_port.clk_enable && rd_port.clk.is_fully_undef()) {
changed = true;
rd_port.clk = State::S0;
}
}
for (auto &wr_port : mem.rd_ports) {
if (!wr_port.clk_enable && wr_port.clk.is_fully_undef()) {
changed = true;
wr_port.clk = State::S0;
}
}
if (changed)
mem.emit();
}
}
module->rewrite_sigspecs(worker);
if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)

1
passes/cmds/show.cc
View File

@ -574,6 +574,7 @@ struct ShowWorker
{
ct.setup_internals();
ct.setup_internals_mem();
ct.setup_internals_anyinit();
ct.setup_stdcells();
ct.setup_stdcells_mem();
ct.setup_design(design);

1
passes/fsm/fsm_detect.cc
View File

@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass {
CellTypes ct;
ct.setup_internals();
ct.setup_internals_anyinit();
ct.setup_internals_mem();
ct.setup_stdcells();
ct.setup_stdcells_mem();

1
passes/hierarchy/submod.cc
View File

@ -260,6 +260,7 @@ struct SubmodWorker
}
ct.setup_internals();
ct.setup_internals_anyinit();
ct.setup_internals_mem();
ct.setup_stdcells();
ct.setup_stdcells_mem();

84
passes/memory/memory_map.cc
View File

@ -32,6 +32,7 @@ struct MemoryMapWorker
bool attr_icase = false;
bool rom_only = false;
bool keepdc = false;
bool formal = false;
dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
RTLIL::Design *design;
@ -151,6 +152,8 @@ struct MemoryMapWorker
// all write ports must share the same clock
RTLIL::SigSpec refclock;
bool refclock_pol = false;
bool async_wr = false;
bool static_only = true;
for (int i = 0; i < GetSize(mem.wr_ports); i++) {
auto &port = mem.wr_ports[i];
if (port.en.is_fully_const() && !port.en.as_bool()) {
@ -164,10 +167,20 @@ struct MemoryMapWorker
static_ports.insert(i);
continue;
}
log("Not mapping memory %s in module %s (write port %d has no clock).\n",
mem.memid.c_str(), module->name.c_str(), i);
return;
static_only = false;
if (GetSize(refclock) != 0)
log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n",
mem.memid.c_str(), module->name.c_str());
if (!formal)
log("Not mapping memory %s in module %s (write port %d has no clock).\n",
mem.memid.c_str(), module->name.c_str(), i);
async_wr = true;
continue;
}
static_only = false;
if (async_wr)
log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n",
mem.memid.c_str(), module->name.c_str());
if (refclock.size() == 0) {
refclock = port.clk;
refclock_pol = port.clk_polarity;
@ -185,6 +198,8 @@ struct MemoryMapWorker
std::vector<RTLIL::SigSpec> data_reg_in(1 << abits);
std::vector<RTLIL::SigSpec> data_reg_out(1 << abits);
std::vector<RTLIL::SigSpec> &data_read = async_wr ? data_reg_in : data_reg_out;
int count_static = 0;
for (int i = 0; i < mem.size; i++)
@ -194,24 +209,36 @@ struct MemoryMapWorker
SigSpec w_init = init_data.extract(i*mem.width, mem.width);
if (static_cells_map.count(addr) > 0)
{
data_reg_out[idx] = static_cells_map[addr];
data_read[idx] = static_cells_map[addr];
count_static++;
}
else if (mem.wr_ports.empty() && (!keepdc || w_init.is_fully_def()))
else if (static_only && (!keepdc || w_init.is_fully_def()))
{
data_reg_out[idx] = w_init;
data_read[idx] = w_init;
}
else
{
RTLIL::Cell *c = module->addCell(genid(mem.memid, "", addr), ID($dff));
c->parameters[ID::WIDTH] = mem.width;
if (GetSize(refclock) != 0) {
RTLIL::Cell *c;
auto ff_id = genid(mem.memid, "", addr);
if (static_only) {
// non-static part is a ROM, we only reach this with keepdc
if (formal) {
c = module->addCell(ff_id, ID($ff));
} else {
c = module->addCell(ff_id, ID($dff));
c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1);
c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0));
}
} else if (async_wr) {
log_assert(formal); // General async write not implemented yet, checked against above
c = module->addCell(ff_id, ID($ff));
} else {
c = module->addCell(ff_id, ID($dff));
c->parameters[ID::CLK_POLARITY] = RTLIL::Const(refclock_pol);
c->setPort(ID::CLK, refclock);
} else {
c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1);
c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0));
}
c->parameters[ID::WIDTH] = mem.width;
RTLIL::Wire *w_in = module->addWire(genid(mem.memid, "", addr, "$d"), mem.width);
data_reg_in[idx] = w_in;
@ -223,18 +250,27 @@ struct MemoryMapWorker
RTLIL::Wire *w_out = module->addWire(w_out_name, mem.width);
if (formal && mem.packed && mem.cell->name.c_str()[0] == '\\') {
auto hdlname = mem.cell->get_hdlname_attribute();
if (hdlname.empty())
hdlname.push_back(mem.cell->name.c_str() + 1);
hdlname.push_back(stringf("[%d]", addr));
w_out->set_hdlname_attribute(hdlname);
}
if (!w_init.is_fully_undef())
w_out->attributes[ID::init] = w_init.as_const();
data_reg_out[idx] = w_out;
c->setPort(ID::Q, w_out);
if (mem.wr_ports.empty())
if (static_only)
module->connect(RTLIL::SigSig(w_in, w_out));
}
}
log(" created %d $dff cells and %d static cells of width %d.\n", mem.size-count_static, count_static, mem.width);
log(" created %d %s cells and %d static cells of width %d.\n",
mem.size-count_static, formal && (static_only || async_wr) ? "$ff" : "$dff", count_static, mem.width);
int count_dff = 0, count_mux = 0, count_wrmux = 0;
@ -272,13 +308,13 @@ struct MemoryMapWorker
}
for (int j = 0; j < (1 << abits); j++)
if (data_reg_out[j] != SigSpec())
module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_reg_out[j]));
if (data_read[j] != SigSpec())
module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_read[j]));
}
log(" read interface: %d $dff and %d $mux cells.\n", count_dff, count_mux);
if (!mem.wr_ports.empty())
if (!static_only)
{
for (int i = 0; i < mem.size; i++)
{
@ -387,12 +423,19 @@ struct MemoryMapPass : public Pass {
log(" -keepdc\n");
log(" when mapping ROMs, keep x-bits shared across read ports.\n");
log("\n");
log(" -formal\n");
log(" map memories for a global clock based formal verification flow.\n");
log(" This implies -keepdc, uses $ff cells for ROMs and sets hdlname\n");
log(" attributes. It also has limited support for async write ports\n");
log(" as generated by clk2fflogic.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool attr_icase = false;
bool rom_only = false;
bool keepdc = false;
bool formal = false;
dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n");
@ -439,6 +482,12 @@ struct MemoryMapPass : public Pass {
keepdc = true;
continue;
}
if (args[argidx] == "-formal")
{
formal = true;
keepdc = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -449,6 +498,7 @@ struct MemoryMapPass : public Pass {
worker.attributes = attributes;
worker.rom_only = rom_only;
worker.keepdc = keepdc;
worker.formal = formal;
worker.run();
}
}

2
passes/opt/opt_clean.cc
View File

@ -633,6 +633,7 @@ struct OptCleanPass : public Pass {
keep_cache.reset(design);
ct_reg.setup_internals_mem();
ct_reg.setup_internals_anyinit();
ct_reg.setup_stdcells_mem();
ct_all.setup(design);
@ -694,6 +695,7 @@ struct CleanPass : public Pass {
keep_cache.reset(design);
ct_reg.setup_internals_mem();
ct_reg.setup_internals_anyinit();
ct_reg.setup_stdcells_mem();
ct_all.setup(design);

8
passes/opt/wreduce.cc
View File

@ -166,8 +166,8 @@ struct WreduceWorker
for (int i = GetSize(sig_q)-1; i >= 0; i--)
{
if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || initval[i] == State::Sx) &&
(!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || rst_value[i] == State::Sx)) {
if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || (!config->keepdc && initval[i] == State::Sx)) &&
(!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || (!config->keepdc && rst_value[i] == State::Sx))) {
module->connect(sig_q[i], State::S0);
initvals.remove_init(sig_q[i]);
sig_d.remove(i);
@ -175,8 +175,8 @@ struct WreduceWorker
continue;
}
if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] &&
(!has_reset || i >= GetSize(rst_value) || rst_value[i] == rst_value[i-1])) {
if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] && (!config->keepdc || initval[i] != State::Sx) &&
(!has_reset || i >= GetSize(rst_value) || (rst_value[i] == rst_value[i-1] && (!config->keepdc || rst_value[i] != State::Sx)))) {
module->connect(sig_q[i], sig_q[i-1]);
initvals.remove_init(sig_q[i]);
sig_d.remove(i);

1
passes/sat/Makefile.inc
View File

@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o
OBJS += passes/sat/assertpmux.o
OBJS += passes/sat/clk2fflogic.o
OBJS += passes/sat/async2sync.o
OBJS += passes/sat/formalff.o
OBJS += passes/sat/supercover.o
OBJS += passes/sat/fmcombine.o
OBJS += passes/sat/mutate.o

5
passes/sat/clk2fflogic.cc
View File

@ -233,7 +233,10 @@ struct Clk2fflogicPass : public Pass {
qval = past_q;
}
if (ff.has_aload) {
// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
// generating a lot of extra logic.
if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) {
SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID);
if (!ff.is_fine)

549
passes/sat/formalff.cc Normal file
View File

@ -0,0 +1,549 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*/
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
#include "kernel/ffinit.h"
#include "kernel/ff.h"
#include "kernel/modtools.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
// Finds signal values with known constant or known unused values in the initial state
struct InitValWorker
{
Module *module;
ModWalker modwalker;
SigMap &sigmap;
FfInitVals initvals;
dict<RTLIL::SigBit, RTLIL::State> initconst_bits;
dict<RTLIL::SigBit, bool> used_bits;
InitValWorker(Module *module) : module(module), modwalker(module->design), sigmap(modwalker.sigmap)
{
modwalker.setup(module);
initvals.set(&modwalker.sigmap, module);
for (auto wire : module->wires())
if (wire->name.isPublic() || wire->get_bool_attribute(ID::keep))
for (auto bit : SigSpec(wire))
used_bits[sigmap(bit)] = true;
}
// Sign/Zero-extended indexing of individual port bits
static SigBit bit_in_port(RTLIL::Cell *cell, RTLIL::IdString port, RTLIL::IdString sign, int index)
{
auto sig_port = cell->getPort(port);
if (index < GetSize(sig_port))
return sig_port[index];
else if (cell->getParam(sign).as_bool())
return GetSize(sig_port) > 0 ? sig_port[GetSize(sig_port) - 1] : State::Sx;
else
return State::S0;
}
// Has the signal a known constant value in the initial state?
//
// For sync-only FFs outputs, this is their initval. For logic loops,
// multiple drivers or unknown cells this is Sx. For a small number of
// handled cells we recurse through their inputs. All results are cached.
RTLIL::State initconst(SigBit bit)
{
sigmap.apply(bit);
if (!bit.is_wire())
return bit.data;
auto it = initconst_bits.find(bit);
if (it != initconst_bits.end())
return it->second;
// Setting this temporarily to x takes care of any logic loops
initconst_bits[bit] = State::Sx;
pool<ModWalker::PortBit> portbits;
modwalker.get_drivers(portbits, {bit});
if (portbits.size() != 1)
return State::Sx;
ModWalker::PortBit portbit = *portbits.begin();
RTLIL::Cell *cell = portbit.cell;
if (RTLIL::builtin_ff_cell_types().count(cell->type))
{
FfData ff(&initvals, cell);
if (ff.has_aload || ff.has_sr || ff.has_arst || (!ff.has_clk && !ff.has_gclk)) {
for (auto bit_q : ff.sig_q) {
initconst_bits[sigmap(bit_q)] = State::Sx;
}
return State::Sx;
}
for (int i = 0; i < ff.width; i++) {
initconst_bits[sigmap(ff.sig_q[i])] = ff.val_init[i];
}
return ff.val_init[portbit.offset];
}
if (cell->type.in(ID($mux), ID($and), ID($or), ID($eq), ID($eqx), ID($initstate)))
{
if (cell->type == ID($mux))
{
SigBit sig_s = sigmap(cell->getPort(ID::S));
State init_s = initconst(sig_s);
State init_y;
if (init_s == State::S0) {
init_y = initconst(cell->getPort(ID::A)[portbit.offset]);
} else if (init_s == State::S1) {
init_y = initconst(cell->getPort(ID::B)[portbit.offset]);
} else {
State init_a = initconst(cell->getPort(ID::A)[portbit.offset]);
State init_b = initconst(cell->getPort(ID::B)[portbit.offset]);
init_y = init_a == init_b ? init_a : State::Sx;
}
initconst_bits[bit] = init_y;
return init_y;
}
if (cell->type.in(ID($and), ID($or)))
{
State init_a = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, portbit.offset));
State init_b = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, portbit.offset));
State init_y;
if (init_a == init_b)
init_y = init_a;
else if (cell->type == ID($and) && (init_a == State::S0 || init_b == State::S0))
init_y = State::S0;
else if (cell->type == ID($or) && (init_a == State::S1 || init_b == State::S1))
init_y = State::S1;
else
init_y = State::Sx;
initconst_bits[bit] = init_y;
return init_y;
}
if (cell->type.in(ID($eq), ID($eqx))) // Treats $eqx as $eq
{
if (portbit.offset > 0) {
initconst_bits[bit] = State::S0;
return State::S0;
}
SigSpec sig_a = cell->getPort(ID::A);
SigSpec sig_b = cell->getPort(ID::B);
State init_y = State::S1;
for (int i = 0; init_y != State::S0 && i < GetSize(sig_a); i++) {
State init_ai = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, i));
if (init_ai == State::Sx) {
init_y = State::Sx;
continue;
}
State init_bi = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, i));
if (init_bi == State::Sx)
init_y = State::Sx;
else if (init_ai != init_bi)
init_y = State::S0;
}
initconst_bits[bit] = init_y;
return init_y;
}
if (cell->type == ID($initstate))
{
initconst_bits[bit] = State::S1;
return State::S1;
}
log_assert(false);
}
return State::Sx;
}
RTLIL::Const initconst(SigSpec sig)
{
std::vector<RTLIL::State> bits;
for (auto bit : sig)
bits.push_back(initconst(bit));
return bits;
}
// Is the initial value of this signal used?
//
// An initial value of a signal is considered as used if it a) aliases a
// wire with a public name, an output wire or with a keep attribute b)
// combinationally drives such a wire or c) drive an input to an unknown
// cell.
//
// This recurses into driven cells for a small number of known handled
// celltypes. Results are cached and initconst is used to detect unused
// inputs for the handled celltypes.
bool is_initval_used(SigBit bit)
{
if (!bit.is_wire())
return false;
auto it = used_bits.find(bit);
if (it != used_bits.end())
return it->second;
used_bits[bit] = true; // Temporarily set to guard against logic loops
pool<ModWalker::PortBit> portbits;
modwalker.get_consumers(portbits, {bit});
for (auto portbit : portbits) {
RTLIL::Cell *cell = portbit.cell;
if (!cell->type.in(ID($mux), ID($and), ID($or), ID($mem_v2)) && !RTLIL::builtin_ff_cell_types().count(cell->type)) {
return true;
}
}
for (auto portbit : portbits)
{
RTLIL::Cell *cell = portbit.cell;
if (RTLIL::builtin_ff_cell_types().count(cell->type))
{
FfData ff(&initvals, cell);
if (ff.has_aload || ff.has_sr || ff.has_arst || ff.has_gclk || !ff.has_clk)
return true;
if (ff.has_ce && initconst(ff.sig_ce.as_bit()) == (ff.pol_ce ? State::S0 : State::S1))
continue;
if (ff.has_srst && initconst(ff.sig_ce.as_bit()) == (ff.pol_srst ? State::S1 : State::S0))
continue;
return true;
}
else if (cell->type == ID($mux))
{
State init_s = initconst(cell->getPort(ID::S).as_bit());
if (init_s == State::S0 && portbit.port == ID::B)
continue;
if (init_s == State::S1 && portbit.port == ID::A)
continue;
auto sig_y = cell->getPort(ID::Y);
if (is_initval_used(sig_y[portbit.offset]))
return true;
}
else if (cell->type.in(ID($and), ID($or)))
{
auto sig_a = cell->getPort(ID::A);
auto sig_b = cell->getPort(ID::B);
auto sig_y = cell->getPort(ID::Y);
if (GetSize(sig_y) != GetSize(sig_a) || GetSize(sig_y) != GetSize(sig_b))
return true; // TODO handle more of this
State absorbing = cell->type == ID($and) ? State::S0 : State::S1;
if (portbit.port == ID::A && initconst(sig_b[portbit.offset]) == absorbing)
continue;
if (portbit.port == ID::B && initconst(sig_a[portbit.offset]) == absorbing)
continue;
if (is_initval_used(sig_y[portbit.offset]))
return true;
}
else if (cell->type == ID($mem_v2))
{
// TODO Use mem.h instead to uniformily cover all cases, most
// likely requires processing all memories when initializing
// the worker
if (!portbit.port.in(ID::WR_DATA, ID::WR_ADDR, ID::RD_ADDR))
return true;
if (portbit.port == ID::WR_DATA)
{
if (initconst(cell->getPort(ID::WR_EN)[portbit.offset]) == State::S0)
continue;
}
else if (portbit.port == ID::WR_ADDR)
{
int port = portbit.offset / cell->getParam(ID::ABITS).as_int();
auto sig_en = cell->getPort(ID::WR_EN);
int width = cell->getParam(ID::WIDTH).as_int();
for (int i = port * width; i < (port + 1) * width; i++)
if (initconst(sig_en[i]) != State::S0)
return true;
continue;
}
else if (portbit.port == ID::RD_ADDR)
{
int port = portbit.offset / cell->getParam(ID::ABITS).as_int();
auto sig_en = cell->getPort(ID::RD_EN);
if (initconst(sig_en[port]) != State::S0)
return true;
continue;
}
else
return true;
}
else
log_assert(false);
}
used_bits[bit] = false;
return false;
}
};
struct FormalFfPass : public Pass {
FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" formalff [options] [selection]\n");
log("\n");
log("This pass transforms clocked flip-flops to prepare a design for formal\n");
log("verification. If a design contains latches and/or multiple different clocks run\n");
log("the async2sync or clk2fflogic passes before using this pass.\n");
log("\n");
log(" -clk2ff\n");
log(" Replace all clocked flip-flops with $ff cells that use the implicit\n");
log(" global clock. This assumes, without checking, that the design uses a\n");
log(" single global clock. If that is not the case, the clk2fflogic pass\n");
log(" should be used instead.\n");
log("\n");
log(" -ff2anyinit\n");
log(" Replace uninitialized bits of $ff cells with $anyinit cells. An\n");
log(" $anyinit cell behaves exactly like an $ff cell with an undefined\n");
log(" initialization value. The difference is that $anyinit inhibits\n");
log(" don't-care optimizations and is used to track solver-provided values\n");
log(" in witness traces.\n");
log("\n");
log(" If combined with -clk2ff this also affects newly created $ff cells.\n");
log("\n");
log(" -anyinit2ff\n");
log(" Replaces $anyinit cells with uninitialized $ff cells. This performs the\n");
log(" reverse of -ff2anyinit and can be used, before running a backend pass\n");
log(" (or similar) that is not yet aware of $anyinit cells.\n");
log("\n");
log(" Note that after running -anyinit2ff, in general, performing don't-care\n");
log(" optimizations is not sound in a formal verification setting.\n");
log("\n");
log(" -fine\n");
log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n");
log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n");
log("\n");
log(" -setundef\n");
log(" Find FFs with undefined initialization values for which changing the\n");
log(" initialization does not change the observable behavior and initialize\n");
log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
log(" cells that drive wires with private names.\n");
log("\n");
// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool flag_clk2ff = false;
bool flag_ff2anyinit = false;
bool flag_anyinit2ff = false;
bool flag_fine = false;
bool flag_setundef = false;
log_header(design, "Executing FORMALFF pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
if (args[argidx] == "-clk2ff") {
flag_clk2ff = true;
continue;
}
if (args[argidx] == "-ff2anyinit") {
flag_ff2anyinit = true;
continue;
}
if (args[argidx] == "-anyinit2ff") {
flag_anyinit2ff = true;
continue;
}
if (args[argidx] == "-fine") {
flag_fine = true;
continue;
}
if (args[argidx] == "-setundef") {
flag_setundef = true;
continue;
}
break;
}
extra_args(args, argidx, design);
if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
if (flag_ff2anyinit && flag_anyinit2ff)
log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
if (flag_fine && !flag_anyinit2ff)
log_cmd_error("The option -fine requries the -anyinit2ff option.\n");
if (flag_fine && flag_clk2ff)
log_cmd_error("The options -fine and -clk2ff are exclusive.\n");
for (auto module : design->selected_modules())
{
if (flag_setundef)
{
InitValWorker worker(module);
for (auto cell : module->selected_cells())
{
if (RTLIL::builtin_ff_cell_types().count(cell->type))
{
FfData ff(&worker.initvals, cell);
if (ff.has_aload || ff.has_sr || ff.has_arst || ff.val_init.is_fully_def())
continue;
if (ff.has_ce && // CE can make the initval stick around
worker.initconst(ff.sig_ce.as_bit()) != (ff.pol_ce ? State::S1 : State::S0) && // unless it's known active
(!ff.has_srst || ff.ce_over_srst ||
worker.initconst(ff.sig_srst.as_bit()) != (ff.pol_srst ? State::S1 : State::S0))) // or a srst with priority is known active
continue;
auto before = ff.val_init;
for (int i = 0; i < ff.width; i++)
if (ff.val_init[i] == State::Sx && !worker.is_initval_used(ff.sig_q[i]))
ff.val_init[i] = State::S0;
if (ff.val_init != before) {
log("Setting unused undefined initial value of %s.%s (%s) from %s to %s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_const(before), log_const(ff.val_init));
worker.initvals.set_init(ff.sig_q, ff.val_init);
}
}
}
}
SigMap sigmap(module);
FfInitVals initvals(&sigmap, module);
for (auto cell : module->selected_cells())
{
if (flag_anyinit2ff && cell->type == ID($anyinit))
{
FfData ff(&initvals, cell);
ff.remove();
ff.is_anyinit = false;
ff.is_fine = flag_fine;
if (flag_fine)
for (int i = 0; i < ff.width; i++)
ff.slice({i}).emit();
else
ff.emit();
continue;
}
if (!RTLIL::builtin_ff_cell_types().count(cell->type))
continue;
FfData ff(&initvals, cell);
bool emit = false;
if (flag_clk2ff && ff.has_clk) {
if (ff.sig_clk.is_fully_const())
log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n",
log_id(cell), log_id(cell->type), log_id(module));
auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr;
if (clk_wire == nullptr) {
clk_wire = module->addWire(NEW_ID);
module->connect(RTLIL::SigBit(clk_wire), ff.sig_clk);
}
auto clk_polarity = ff.pol_clk ? State::S1 : State::S0;
std::string attribute = clk_wire->get_string_attribute(ID::replaced_by_gclk);
auto &attr = clk_wire->attributes[ID::replaced_by_gclk];
if (!attr.empty() && attr != clk_polarity)
log_error("CLK %s on %s (%s) from module %s also used with opposite polarity, run clk2fflogic instead.\n",
log_id(clk_wire), log_id(cell), log_id(cell->type), log_id(module));
attr = clk_polarity;
clk_wire->set_bool_attribute(ID::keep);
// TODO propagate the replaced_by_gclk attribute upwards throughout the hierarchy
ff.unmap_ce_srst();
ff.has_clk = false;
ff.has_gclk = true;
emit = true;
}
if (!ff.has_gclk) {
continue;
}
if (flag_ff2anyinit && !ff.val_init.is_fully_def())
{
ff.remove();
emit = false;
int cursor = 0;
while (cursor < ff.val_init.size())
{
bool is_anyinit = ff.val_init[cursor] == State::Sx;
std::vector<int> bits;
bits.push_back(cursor++);
while (cursor < ff.val_init.size() && (ff.val_init[cursor] == State::Sx) == is_anyinit)
bits.push_back(cursor++);
if ((int)bits.size() == ff.val_init.size()) {
// This check is only to make the private names more helpful for debugging
ff.is_anyinit = true;
emit = true;
break;
}
auto slice = ff.slice(bits);
slice.is_anyinit = is_anyinit;
slice.emit();
}
}
if (emit)
ff.emit();
}
}
}
} FormalFfPass;
PRIVATE_NAMESPACE_END

52
passes/sat/sim.cc
View File

@ -81,6 +81,7 @@ struct SimShared
bool hide_internal = true;
bool writeback = false;
bool zinit = false;
bool hdlname = false;
int rstlen = 1;
FstData *fst = nullptr;
double start_time = 0;
@ -231,7 +232,7 @@ struct SimInstance
}
}
if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
FfData ff_data(nullptr, cell);
ff_state_t ff;
ff.past_d = Const(State::Sx, ff_data.width);
@ -738,9 +739,17 @@ struct SimInstance
child.second->register_signals(id);
}
void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int, bool)> register_signal)
void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, Wire*, int, bool)> register_signal)
{
enter_scope(name());
int exit_scopes = 1;
if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) {
auto hdlname = instance->get_hdlname_attribute();
log_assert(!hdlname.empty());
for (auto name : hdlname)
enter_scope("\\" + name);
exit_scopes = hdlname.size();
} else
enter_scope(name());
dict<Wire*,bool> registers;
for (auto cell : module->cells())
@ -756,13 +765,25 @@ struct SimInstance
for (auto signal : signal_database)
{
register_signal(signal.first, signal.second.first, registers.count(signal.first)!=0);
if (shared->hdlname && signal.first->name.isPublic() && signal.first->has_attribute(ID::hdlname)) {
auto hdlname = signal.first->get_hdlname_attribute();
log_assert(!hdlname.empty());
auto signal_name = std::move(hdlname.back());
hdlname.pop_back();
for (auto name : hdlname)
enter_scope("\\" + name);
register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0);
for (auto name : hdlname)
exit_scope();
} else
register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0);
}
for (auto child : children)
child.second->write_output_header(enter_scope, exit_scope, register_signal);
exit_scope();
for (int i = 0; i < exit_scopes; i++)
exit_scope();
}
void register_output_step_values(std::map<int,Const> *data)
@ -1712,7 +1733,11 @@ struct VCDWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
[this]() { vcdfile << stringf("$upscope $end\n");},
[this,use_signal](Wire *wire, int id, bool is_reg) { if (use_signal.at(id)) vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); }
[this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
if (use_signal.at(id)) {
vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name);
}
}
);
vcdfile << stringf("$enddefinitions $end\n");
@ -1770,11 +1795,10 @@ struct FSTWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
[this]() { fstWriterSetUpscope(fstfile); },
[this,use_signal](Wire *wire, int id, bool is_reg) {
[this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
if (!use_signal.at(id)) return;
fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0);
name, 0);
mapping.emplace(id, fst_id);
}
);
@ -1856,7 +1880,7 @@ struct AIWWriter : public OutputWriter
worker->top->write_output_header(
[](IdString) {},
[]() {},
[this](Wire *wire, int id, bool) { mapping[wire] = id; }
[this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; }
);
std::map<int, Yosys::RTLIL::Const> current;
@ -1945,6 +1969,10 @@ struct SimPass : public Pass {
log(" write the simulation results to an AIGER witness file\n");
log(" (requires a *.aim file via -map)\n");
log("\n");
log(" -hdlname\n");
log(" use the hdlname attribute when writing simulation results\n");
log(" (preserves hierarchy in a flattened design)\n");
log("\n");
log(" -x\n");
log(" ignore constant x outputs in simulation file.\n");
log("\n");
@ -2057,6 +2085,10 @@ struct SimPass : public Pass {
worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(new AIWWriter(&worker, aiw_filename.c_str())));
continue;
}
if (args[argidx] == "-hdlname") {
worker.hdlname = true;
continue;
}
if (args[argidx] == "-n" && argidx+1 < args.size()) {
numcycles = atoi(args[++argidx].c_str());
worker.cycles_set = true;

17
techlibs/common/simlib.v
View File

@ -1696,6 +1696,23 @@ assign Y = 'bx;
endmodule
// --------------------------------------------------------
`ifdef SIMLIB_FF
module \$anyinit (D, Q);
parameter WIDTH = 0;
input [WIDTH-1:0] D;
output reg [WIDTH-1:0] Q;
initial Q <= 'bx;
always @($global_clk) begin
Q <= D;
end
endmodule
`endif
// --------------------------------------------------------
module \$allconst (Y);

8
tests/various/smtlib2_module-expected.smt2
View File

@ -4,11 +4,14 @@
(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
; yosys-smt2-input a 8
; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8}
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
; yosys-smt2-input b 8
; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8}
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
; yosys-smt2-output add 8
; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8}
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@ -16,6 +19,7 @@
(bvadd a b)
))
; yosys-smt2-output eq 1
; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1}
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@ -23,6 +27,7 @@
(= a b)
))
; yosys-smt2-output sub 8
; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8}
(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
@ -38,13 +43,16 @@
(declare-sort |uut_s| 0)
(declare-fun |uut_is| (|uut_s|) Bool)
; yosys-smt2-cell smtlib2 s
; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"}
(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8}
(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8}
(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9