frontends/verific/verificsva.cc

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20
  21 // SVA Properties Simplified Syntax:
  22 //
  23 // prop:
  24 //   not prop
  25 //   prop or prop
  26 //   prop and prop
  27 //   seq |-> prop
  28 //   seq |=> prop
  29 //   if (expr) prop [else prop]
  30 //   prop until prop
  31 //   prop implies prop
  32 //   prop iff prop
  33 //   accept_on (expr) prop
  34 //   reject_on (expr) prop
  35 //
  36 // seq:
  37 //   expr
  38 //   expr ##N seq
  39 //   expr ##[N:M] seq
  40 //   seq or seq
  41 //   seq and seq
  42 //   seq intersect seq
  43 //   first_match (seq)
  44 //   expr throughout seq
  45 //   seq within seq
  46 //   seq [*N]
  47 //   seq [*N:M]
  48 //   expr [=N]
  49 //   expr [=N:M]
  50 //   expr [->N]
  51 //   expr [->N:M]
  52
  53
  54 #include "kernel/yosys.h"
  55 #include "frontends/verific/verific.h"
  56
  57 USING_YOSYS_NAMESPACE
  58
  59 #ifdef VERIFIC_NAMESPACE
  60 using namespace Verific;
  61 #endif
  62
  63 YOSYS_NAMESPACE_BEGIN
  64
  65 pool<int> verific_sva_prims = {
  66         // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
  67         PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
  68         PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
  69         PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
  70         PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
  71         PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
  72         PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
  73         PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
  74         PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
  75         PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
  76         PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
  77         PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
  78         PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
  79         PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
  80         PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
  81         PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
  82         PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
  83         PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
  84         PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
  85         PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
  86 };
  87
  88 struct VerificSvaImporter
  89 {
  90         VerificImporter *importer = nullptr;
  91         Module *module = nullptr;
  92
  93         Netlist *netlist = nullptr;
  94         Instance *root = nullptr;
  95
  96         SigBit clock = State::Sx;
  97         bool clock_posedge = false;
  98
  99         SigBit disable_iff = State::S0;
 100
 101         bool mode_assert = false;
 102         bool mode_assume = false;
 103         bool mode_cover = false;
 104         bool eventually = false;
 105         bool did_something = false;
 106
 107         Instance *net_to_ast_driver(Net *n)
 108         {
 109                 if (n == nullptr)
 110                         return nullptr;
 111
 112                 if (n->IsMultipleDriven())
 113                         return nullptr;
 114
 115                 Instance *inst = n->Driver();
 116
 117                 if (inst == nullptr)
 118                         return nullptr;
 119
 120                 if (!verific_sva_prims.count(inst->Type()))
 121                         return nullptr;
 122
 123                 if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
 124                                 inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
 125                         return nullptr;
 126
 127                 return inst;
 128         }
 129
 130         Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
 131         Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
 132         Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
 133         Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
 134         Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
 135
 136         // ----------------------------------------------------------
 137         // SVA AST Types
 138
 139         struct svatype_t
 140         {
 141                 bool flag_linear = true;
 142         };
 143
 144         std::map<Instance*, svatype_t> svatype_cache;
 145
 146         void svatype_visit_child(svatype_t &entry, Instance *inst)
 147         {
 148                 if (inst == nullptr)
 149                         return;
 150
 151                 const svatype_t &child_entry = svatype(inst);
 152                 entry.flag_linear &= child_entry.flag_linear;
 153         }
 154
 155         const svatype_t &svatype(Instance *inst)
 156         {
 157                 if (svatype_cache.count(inst) != 0)
 158                         return svatype_cache.at(inst);
 159
 160                 svatype_t &entry = svatype_cache[inst];
 161
 162                 if (inst == nullptr)
 163                         return entry;
 164
 165                 if (inst->Type() == PRIM_SVA_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
 166                 {
 167                         const char *sva_low_s = inst->GetAttValue("sva:low");
 168                         const char *sva_high_s = inst->GetAttValue("sva:high");
 169
 170                         int sva_low = atoi(sva_low_s);
 171                         int sva_high = atoi(sva_high_s);
 172                         bool sva_inf = !strcmp(sva_high_s, "$");
 173
 174                         if (sva_inf || sva_low != sva_high)
 175                                 entry.flag_linear = false;
 176                 }
 177
 178                 svatype_visit_child(entry, get_ast_input(inst));
 179                 svatype_visit_child(entry, get_ast_input1(inst));
 180                 svatype_visit_child(entry, get_ast_input2(inst));
 181                 svatype_visit_child(entry, get_ast_input3(inst));
 182                 svatype_visit_child(entry, get_ast_control(inst));
 183
 184                 return entry;
 185         }
 186
 187         // ----------------------------------------------------------
 188         // SVA Preprocessor
 189
 190         Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
 191         Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
 192         Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
 193         Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
 194         Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
 195
 196         Net *rewrite(Instance *inst, Net *default_net = nullptr)
 197         {
 198                 if (inst == nullptr)
 199                         return default_net;
 200
 201                 if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
 202                                 inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
 203                         Net *new_net = rewrite(get_ast_input(inst));
 204                         if (new_net) {
 205                                 inst->Disconnect(inst->View()->GetInput());
 206                                 inst->Connect(inst->View()->GetInput(), new_net);
 207                         }
 208                         return default_net;
 209                 }
 210
 211                 if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
 212                         Net *new_net = rewrite(get_ast_input2(inst));
 213                         if (new_net) {
 214                                 inst->Disconnect(inst->View()->GetInput2());
 215                                 inst->Connect(inst->View()->GetInput2(), new_net);
 216                         }
 217                         return default_net;
 218                 }
 219
 220                 if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
 221                 {
 222                         if (mode_cover) {
 223                                 did_something = true;
 224                                 Net *new_in1 = rewrite_input1(inst);
 225                                 Net *new_in2 = rewrite_input2(inst);
 226                                 return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
 227                         }
 228                         return default_net;
 229                 }
 230
 231                 if (inst->Type() == PRIM_SVA_NOT)
 232                 {
 233                         if (mode_assert || mode_assume) {
 234                                 did_something = true;
 235                                 Net *new_in = rewrite_input(inst);
 236                                 Net *net_zero = netlist->Gnd(inst->Linefile());
 237                                 return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
 238                         }
 239                         return default_net;
 240                 }
 241
 242                 return default_net;
 243         }
 244
 245         void rewrite()
 246         {
 247                 netlist = root->Owner();
 248                 do {
 249                         did_something = false;
 250                         rewrite(root);
 251                 } while (did_something);
 252         }
 253
 254         // ----------------------------------------------------------
 255         // SVA Importer
 256
 257         vector<SigBit> sva_until_list_inclusive;
 258         vector<SigBit> sva_until_list_exclusive;
 259         vector<vector<SigBit>*> sva_sequence_alive_list;
 260
 261         struct sequence_t {
 262                 int length = 0;
 263                 SigBit sig_a = State::S1;
 264                 SigBit sig_en = State::S1;
 265         };
 266
 267         void sequence_cond(sequence_t &seq, SigBit cond)
 268         {
 269                 seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
 270         }
 271
 272         void sequence_ff(sequence_t &seq)
 273         {
 274                 if (disable_iff != State::S0)
 275                         seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
 276
 277                 for (auto &expr : sva_until_list_exclusive)
 278                         seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
 279
 280                 Wire *sig_a_q = module->addWire(NEW_ID);
 281                 sig_a_q->attributes["\\init"] = Const(0, 1);
 282
 283                 Wire *sig_en_q = module->addWire(NEW_ID);
 284                 sig_en_q->attributes["\\init"] = Const(0, 1);
 285
 286                 for (auto list : sva_sequence_alive_list)
 287                         list->push_back(module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en));
 288
 289                 module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
 290                 module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
 291
 292                 if (seq.length >= 0)
 293                         seq.length++;
 294
 295                 seq.sig_a = sig_a_q;
 296                 seq.sig_en = sig_en_q;
 297
 298                 for (auto &expr : sva_until_list_inclusive)
 299                         seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
 300         }
 301
 302         void combine_seq(sequence_t &seq, const sequence_t &other_seq)
 303         {
 304                 if (seq.length != other_seq.length)
 305                         seq.length = -1;
 306
 307                 SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en);
 308                 SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_seq.sig_a, other_seq.sig_en);
 309
 310                 seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a);
 311                 seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_seq.sig_en);
 312         }
 313
 314         void combine_seq(sequence_t &seq, SigBit other_a, SigBit other_en)
 315         {
 316                 SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en);
 317                 SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_a, other_en);
 318
 319                 seq.length = -1;
 320                 seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a);
 321                 seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_en);
 322         }
 323
 324         SigBit make_temporal_one_hot(SigBit enable = State::S1, SigBit *latched = nullptr)
 325         {
 326                 Wire *state = module->addWire(NEW_ID);
 327                 state->attributes["\\init"] = State::S0;
 328
 329                 SigBit any = module->Anyseq(NEW_ID);
 330                 if (enable != State::S1)
 331                         any = module->LogicAnd(NEW_ID, any, enable);
 332
 333                 SigBit next_state = module->LogicOr(NEW_ID, state, any);
 334                 module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
 335
 336                 if (latched != nullptr)
 337                         *latched = state;
 338
 339                 SigBit not_state = module->LogicNot(NEW_ID, state);
 340                 return module->LogicAnd(NEW_ID, next_state, not_state);
 341         }
 342
 343         SigBit make_permanent_latch(SigBit enable, bool async = false)
 344         {
 345                 Wire *state = module->addWire(NEW_ID);
 346                 state->attributes["\\init"] = State::S0;
 347
 348                 SigBit next_state = module->LogicOr(NEW_ID, state, enable);
 349                 module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
 350
 351                 return async ? next_state : state;
 352         }
 353
 354         void parse_sequence(sequence_t &seq, Net *n)
 355         {
 356                 Instance *inst = net_to_ast_driver(n);
 357
 358                 // Regular expression
 359
 360                 if (inst == nullptr) {
 361                         sequence_cond(seq, importer->net_map_at(n));
 362                         return;
 363                 }
 364
 365                 // SVA Primitives
 366
 367                 if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
 368                                 inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
 369                 {
 370                         Instance *consequent = get_ast_input2(inst);
 371                         bool linear_consequent = svatype(consequent).flag_linear;
 372
 373                         parse_sequence(seq, inst->GetInput1());
 374                         seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
 375
 376                         if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
 377                                 sequence_ff(seq);
 378
 379                         if (!linear_consequent && mode_assume)
 380                                 log_error("Non-linear consequent is currently not supported in SVA assumptions.\n");
 381
 382                         if (linear_consequent)
 383                         {
 384                                 parse_sequence(seq, inst->GetInput2());
 385                         }
 386                         else
 387                         {
 388                                 SigBit activated;
 389                                 seq.sig_en = make_temporal_one_hot(seq.sig_en, &activated);
 390
 391                                 SigBit pass_latch_en = module->addWire(NEW_ID);
 392                                 SigBit pass_latch = make_permanent_latch(pass_latch_en, true);
 393
 394                                 vector<SigBit> alive_list;
 395                                 sva_sequence_alive_list.push_back(&alive_list);
 396                                 parse_sequence(seq, inst->GetInput2());
 397                                 sva_sequence_alive_list.pop_back();
 398
 399                                 module->addLogicAnd(NEW_ID, seq.sig_a, seq.sig_en, pass_latch_en);
 400                                 alive_list.push_back(pass_latch);
 401
 402                                 seq.length = -1;
 403                                 seq.sig_a = module->ReduceOr(NEW_ID, SigSpec(alive_list));
 404                                 seq.sig_en = module->ReduceOr(NEW_ID, activated);
 405                         }
 406
 407                         return;
 408                 }
 409
 410                 if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
 411                 {
 412                         const char *sva_low_s = inst->GetAttValue("sva:low");
 413                         const char *sva_high_s = inst->GetAttValue("sva:high");
 414
 415                         int sva_low = atoi(sva_low_s);
 416                         int sva_high = atoi(sva_high_s);
 417                         bool sva_inf = !strcmp(sva_high_s, "$");
 418
 419                         parse_sequence(seq, inst->GetInput1());
 420
 421                         for (int i = 0; i < sva_low; i++)
 422                                 sequence_ff(seq);
 423
 424                         if (sva_inf)
 425                         {
 426                                 SigBit latched_a = module->addWire(NEW_ID);
 427                                 SigBit latched_en = module->addWire(NEW_ID);
 428                                 combine_seq(seq, latched_a, latched_en);
 429
 430                                 sequence_t seq_latched = seq;
 431                                 sequence_ff(seq_latched);
 432                                 module->connect(latched_a, seq_latched.sig_a);
 433                                 module->connect(latched_en, seq_latched.sig_en);
 434                         }
 435                         else
 436                         {
 437                                 for (int i = sva_low; i < sva_high; i++)
 438                                 {
 439                                         sequence_t last_seq = seq;
 440                                         sequence_ff(seq);
 441                                         combine_seq(seq, last_seq);
 442                                 }
 443                         }
 444
 445                         parse_sequence(seq, inst->GetInput2());
 446                         return;
 447                 }
 448
 449                 if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
 450                 {
 451                         const char *sva_low_s = inst->GetAttValue("sva:low");
 452                         const char *sva_high_s = inst->GetAttValue("sva:high");
 453
 454                         int sva_low = atoi(sva_low_s);
 455                         int sva_high = atoi(sva_high_s);
 456                         bool sva_inf = !strcmp(sva_high_s, "$");
 457
 458                         parse_sequence(seq, inst->GetInput());
 459
 460                         for (int i = 1; i < sva_low; i++) {
 461                                 sequence_ff(seq);
 462                                 parse_sequence(seq, inst->GetInput());
 463                         }
 464
 465                         if (sva_inf)
 466                         {
 467                                 SigBit latched_a = module->addWire(NEW_ID);
 468                                 SigBit latched_en = module->addWire(NEW_ID);
 469                                 combine_seq(seq, latched_a, latched_en);
 470
 471                                 sequence_t seq_latched = seq;
 472                                 sequence_ff(seq_latched);
 473                                 parse_sequence(seq_latched, inst->GetInput());
 474                                 module->connect(latched_a, seq_latched.sig_a);
 475                                 module->connect(latched_en, seq_latched.sig_en);
 476                         }
 477                         else
 478                         {
 479                                 for (int i = sva_low; i < sva_high; i++)
 480                                 {
 481                                         sequence_t last_seq = seq;
 482                                         sequence_ff(seq);
 483                                         parse_sequence(seq, inst->GetInput());
 484                                         combine_seq(seq, last_seq);
 485                                 }
 486                         }
 487
 488                         return;
 489                 }
 490
 491                 if (inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
 492                                 inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
 493                 {
 494                         bool flag_with = inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
 495
 496                         if (get_ast_input1(inst) != nullptr)
 497                                 log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n");
 498
 499                         SigBit expr = importer->net_map_at(inst->GetInput1());
 500
 501                         if (flag_with)
 502                         {
 503                                 seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
 504                                 sva_until_list_inclusive.push_back(expr);
 505                                 parse_sequence(seq, inst->GetInput2());
 506                                 sva_until_list_inclusive.pop_back();
 507                         }
 508                         else
 509                         {
 510                                 sva_until_list_exclusive.push_back(expr);
 511                                 parse_sequence(seq, inst->GetInput2());
 512                                 sva_until_list_exclusive.pop_back();
 513                         }
 514
 515                         return;
 516                 }
 517
 518                 // Handle unsupported primitives
 519
 520                 if (!importer->mode_keep)
 521                         log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
 522                 log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
 523         }
 524
 525         void import()
 526         {
 527                 module = importer->module;
 528                 netlist = root->Owner();
 529
 530                 RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
 531
 532                 // parse SVA property clock event
 533
 534                 Instance *at_node = get_ast_input(root);
 535
 536                 // asynchronous immediate assertion/assumption/cover
 537                 if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
 538                                 root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
 539                 {
 540                         SigSpec sig_a = importer->net_map_at(root->GetInput());
 541                         RTLIL::Cell *c = nullptr;
 542
 543                         if (eventually) {
 544                                 if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
 545                                 if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
 546                         } else {
 547                                 if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
 548                                 if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
 549                                 if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
 550                         }
 551
 552                         importer->import_attributes(c->attributes, root);
 553                         return;
 554                 }
 555
 556                 log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
 557
 558                 VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
 559                 clock = clock_edge.clock_sig;
 560                 clock_posedge = clock_edge.posedge;
 561
 562                 // parse disable_iff expression
 563
 564                 Net *sequence_net = at_node->GetInput2();
 565
 566                 while (1)
 567                 {
 568                         Instance *sequence_node = net_to_ast_driver(sequence_net);
 569
 570                         if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
 571                                 eventually = true;
 572                                 sequence_net = sequence_node->GetInput();
 573                                 continue;
 574                         }
 575
 576                         if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
 577                                 disable_iff = importer->net_map_at(sequence_node->GetInput1());
 578                                 sequence_net = sequence_node->GetInput2();
 579                                 continue;
 580                         }
 581
 582                         break;
 583                 }
 584
 585                 // parse SVA sequence into trigger signal
 586
 587                 sequence_t seq;
 588                 parse_sequence(seq, sequence_net);
 589                 sequence_ff(seq);
 590
 591                 // generate assert/assume/cover cell
 592
 593                 RTLIL::Cell *c = nullptr;
 594
 595                 if (eventually) {
 596                         if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
 597                         if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
 598                 } else {
 599                         if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
 600                         if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
 601                         if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
 602                 }
 603
 604                 importer->import_attributes(c->attributes, root);
 605         }
 606 };
 607
 608 void svapp_assert(Instance *inst)
 609 {
 610         VerificSvaImporter worker;
 611         worker.root = inst;
 612         worker.mode_assert = true;
 613         worker.rewrite();
 614 }
 615
 616 void svapp_assume(Instance *inst)
 617 {
 618         VerificSvaImporter worker;
 619         worker.root = inst;
 620         worker.mode_assume = true;
 621         worker.rewrite();
 622 }
 623
 624 void svapp_cover(Instance *inst)
 625 {
 626         VerificSvaImporter worker;
 627         worker.root = inst;
 628         worker.mode_cover = true;
 629         worker.rewrite();
 630 }
 631
 632 void import_sva_assert(VerificImporter *importer, Instance *inst)
 633 {
 634         VerificSvaImporter worker;
 635         worker.importer = importer;
 636         worker.root = inst;
 637         worker.mode_assert = true;
 638         worker.import();
 639 }
 640
 641 void import_sva_assume(VerificImporter *importer, Instance *inst)
 642 {
 643         VerificSvaImporter worker;
 644         worker.importer = importer;
 645         worker.root = inst;
 646         worker.mode_assume = true;
 647         worker.import();
 648 }
 649
 650 void import_sva_cover(VerificImporter *importer, Instance *inst)
 651 {
 652         VerificSvaImporter worker;
 653         worker.importer = importer;
 654         worker.root = inst;
 655         worker.mode_cover = true;
 656         worker.import();
 657 }
 658
 659 YOSYS_NAMESPACE_END