23
23
#include <trans-netlist/instantiate_netlist.h>
24
24
#include <trans-netlist/trans_trace_netlist.h>
25
25
#include <trans-netlist/unwind_netlist.h>
26
- #include <verilog/sva_expr.h>
27
26
28
27
#include "netlist.h"
29
28
@@ -66,7 +65,7 @@ class bdd_enginet
66
65
const namespacet ns;
67
66
netlistt netlist;
68
67
69
- static bool property_supported(const exprt &);
68
+ static std::optional<exprt> property_supported(const exprt &);
70
69
71
70
// the Manager must appear before any BDDs
72
71
// to do the cleanup in the right order
@@ -199,9 +198,20 @@ property_checker_resultt bdd_enginet::operator()()
199
198
<< ", nodes: " << netlist.number_of_nodes()
200
199
<< messaget::eom;
201
200
202
- for(const auto &property : properties.properties)
203
- if(property_supported(property.normalized_expr))
204
- get_atomic_propositions(property.normalized_expr);
201
+ for(auto &property : properties.properties)
202
+ {
203
+ if(!property.is_disabled())
204
+ {
205
+ auto converted_opt = property_supported(property.normalized_expr);
206
+ if(converted_opt.has_value())
207
+ {
208
+ property.normalized_expr = *converted_opt;
209
+ get_atomic_propositions(*converted_opt);
210
+ }
211
+ else
212
+ property.failure("property not supported by BDD engine");
213
+ }
214
+ }
205
215
206
216
message.status() << "Building BDD for netlist" << messaget::eom;
207
217
@@ -449,40 +459,29 @@ Function: bdd_enginet::property_supported
449
459
450
460
\*******************************************************************/
451
461
452
- bool bdd_enginet::property_supported(const exprt &expr)
462
+ std::optional<exprt> bdd_enginet::property_supported(const exprt &expr)
453
463
{
454
464
// Our engine knows all of CTL.
455
465
if(is_CTL(expr))
456
- return true ;
466
+ return expr ;
457
467
458
468
if(is_LTL(expr))
459
469
{
460
470
// We can map selected path properties to CTL.
461
- return LTL_to_CTL(expr).has_value() ;
471
+ return LTL_to_CTL(expr);
462
472
}
463
473
464
474
if(is_SVA(expr))
465
475
{
466
- if(
467
- expr.id() == ID_sva_always &&
468
- !has_temporal_operator(to_sva_always_expr(expr).op()))
469
- {
470
- // always p
471
- return true;
472
- }
473
-
474
- if(
475
- expr.id() == ID_sva_always &&
476
- to_sva_always_expr(expr).op().id() == ID_sva_s_eventually &&
477
- !has_temporal_operator(
478
- to_sva_s_eventually_expr(to_sva_always_expr(expr).op()).op()))
479
- {
480
- // always s_eventually p
481
- return true;
482
- }
476
+ // We can map some SVA to LTL. In turn, some of that can be mapped to CTL.
477
+ auto ltl_opt = SVA_to_LTL(expr);
478
+ if(ltl_opt.has_value())
479
+ return property_supported(ltl_opt.value());
480
+ else
481
+ return {};
483
482
}
484
483
485
- return false ;
484
+ return {} ;
486
485
}
487
486
488
487
/*******************************************************************\
@@ -505,51 +504,12 @@ void bdd_enginet::check_property(propertyt &property)
505
504
if(property.is_assumed())
506
505
return;
507
506
508
- if(!property_supported(property.normalized_expr))
509
- {
510
- property.failure("property not supported by BDD engine");
507
+ if(property.is_failure())
511
508
return;
512
- }
513
509
514
510
message.status() << "Checking " << property.name << messaget::eom;
515
511
property.status=propertyt::statust::UNKNOWN;
516
512
517
- if(
518
- property.normalized_expr.id() == ID_sva_always &&
519
- to_sva_always_expr(property.normalized_expr).op().id() ==
520
- ID_sva_s_eventually &&
521
- !has_temporal_operator(to_sva_s_eventually_expr(
522
- to_sva_always_expr(property.normalized_expr).op())
523
- .op()))
524
- {
525
- // always s_eventually p --> AG AF p
526
- auto p = to_sva_s_eventually_expr(
527
- to_sva_always_expr(property.normalized_expr).op())
528
- .op();
529
- property.normalized_expr = AG_exprt{AF_exprt{p}};
530
- }
531
-
532
- if(
533
- property.normalized_expr.id() == ID_sva_always &&
534
- !has_temporal_operator(to_sva_always_expr(property.normalized_expr).op()))
535
- {
536
- // always p --> AG p
537
- auto p = to_sva_always_expr(property.normalized_expr).op();
538
- property.normalized_expr = AG_exprt{p};
539
- }
540
-
541
- // Our engine knows CTL only.
542
- // We map selected path properties to CTL.
543
- if(
544
- has_temporal_operator(property.normalized_expr) &&
545
- is_LTL(property.normalized_expr))
546
- {
547
- auto CTL_opt = LTL_to_CTL(property.normalized_expr);
548
- CHECK_RETURN(CTL_opt.has_value());
549
- property.normalized_expr = CTL_opt.value();
550
- CHECK_RETURN(is_CTL(property.normalized_expr));
551
- }
552
-
553
513
if(is_AGp(property.normalized_expr))
554
514
{
555
515
check_AGp(property);
0 commit comments