1231
1284
(walist vl-wirealist-p)
1232
1285
(warnings vl-warninglist-p))
1233
1286
:returns (mv (warnings vl-warninglist-p)
1234
(db us-db-p :hyp :fguard))
1235
1288
(b* (((when (atom x))
1289
(mv (ok) (us-db-fix db)))
1237
1290
((mv warnings db)
1238
1291
(us-mark-false-inouts-for-portdecl (car x) db walist warnings)))
1239
1292
(us-mark-false-inouts (cdr x) db walist warnings))))
1243
1295
; We make a US-NOTE for every module instance connection:
1245
(defaggregate us-note
1246
(submod ; the submodule being instanced
1247
formals ; the particular wires (port bits from submod) that this note pertains to
1248
actuals ; the actual wires that are connected
1298
((submod stringp) ; the submodule being instanced
1299
(formals vl-emodwirelist) ; the particular wires (port bits from submod) that this note pertains to
1300
(actuals vl-emodwirelist) ; the actual wires that are connected
1252
:require ((stringp-of-us-note->submod
1254
:rule-classes :type-prescription)
1255
(vl-emodwirelist-p-of-us-note->formals
1256
(vl-emodwirelist-p formals))
1257
(vl-emodwirelist-p-of-us-note->actuals
1258
(vl-emodwirelist-p actuals))))
1260
(deflist us-notelist-p (x)
1305
(fty::deflist us-notelist :elt-type us-note
1263
1306
:elementp-of-nil nil)
1265
(defalist us-notealist-p (x)
1267
:val (us-notelist-p x)
1308
(fty::defalist us-notealist :key-type string :val-type us-notelist
1268
1309
:keyp-of-nil nil
1269
1310
:valp-of-nil t)
1273
(defsection us-mark-wires-for-modinst-lvalue-arg
1275
; Handler for module instance arguments whose expressions look like lvalues,
1276
; and hence whose bits can be lined up with the port expression.
1278
(defund us-mark-wires-for-modinst-lvalue-arg
1279
(actual-bits ; bits for the argument
1280
formal-bits ; bits for the submodule's port; matches len of actual-bits
1281
sub-db ; db for the submodule
1282
db ; db for the superior module (may be extended)
1283
warnings ; warnings accumulator for the superior module (may be extended)
1284
inst ; context for warnings and notes
1285
notes ; accumulator for notes (may be extended)
1287
"Returns (MV WARNINGS DB NOTES)"
1288
(declare (xargs :guard (and (vl-emodwirelist-p actual-bits)
1289
(vl-emodwirelist-p formal-bits)
1290
(same-lengthp actual-bits formal-bits)
1293
(vl-warninglist-p warnings)
1295
(us-notelist-p notes))
1296
:verify-guards nil))
1298
;; We recursively process each actual-bit/formal-bit pair.
1299
(b* (((when (atom actual-bits))
1300
(mv warnings db notes))
1302
((mv warnings db notes)
1303
(us-mark-wires-for-modinst-lvalue-arg (cdr actual-bits) (cdr formal-bits)
1304
sub-db db warnings inst notes))
1306
(actual1 (car actual-bits))
1307
(formal1 (car formal-bits))
1308
(formal1-look (hons-get formal1 sub-db))
1309
((unless formal1-look)
1310
(b* ((w (make-vl-warning
1311
:type :use-set-fudging
1312
:msg "~a0: expected a binding for formal bit ~s1; not ~
1314
(define us-mark-wires-for-modinst-lvalue-arg ((actual-bits vl-emodwirelist-p)
1315
(formal-bits vl-emodwirelist-p)
1318
(warnings vl-warninglist-p)
1320
(notes us-notelist-p))
1321
:guard (same-lengthp actual-bits formal-bits)
1323
:returns (mv (warnings1 vl-warninglist-p)
1325
(notes1 us-notelist-p))
1326
;; We recursively process each actual-bit/formal-bit pair.
1327
(b* ((warnings (vl-warninglist-fix warnings))
1329
(sub-db (us-db-fix sub-db))
1330
(notes (us-notelist-fix notes))
1331
(inst (vl-modinst-fix inst))
1332
((when (atom actual-bits))
1333
(mv warnings db notes))
1335
((mv warnings db notes)
1336
(us-mark-wires-for-modinst-lvalue-arg (cdr actual-bits) (cdr formal-bits)
1337
sub-db db warnings inst notes))
1339
(actual1 (vl-emodwire-fix (car actual-bits)))
1340
(formal1 (vl-emodwire-fix (car formal-bits)))
1341
(formal1-look (hons-get formal1 sub-db))
1342
((unless formal1-look)
1343
(b* ((w (make-vl-warning
1344
:type :use-set-fudging
1345
:msg "~a0: expected a binding for formal bit ~s1; not ~
1313
1346
inferring any use/set information for ~s2."
1314
:args (list inst formal1 actual1)
1315
:fn 'us-mark-wires-for-modinst-lvalue-arg)))
1316
(mv (cons w warnings) db notes)))
1318
;; We just merge in the mask from formal1. If the formal is
1319
;; truly/falsely used, then this marks the actual as being
1320
;; truly/falsely used. If the formal is truly/falsely set, this marks
1321
;; the actual as being truly/falsely set.
1322
(formal1-mask (cdr formal1-look))
1323
;; Strip out any used above/below info
1324
(formal1-mask (acl2::bitset-difference formal1-mask *us-above-mask*))
1326
(us-mark-wire formal1-mask actual1 db warnings inst))
1327
(note (make-us-note :submod (vl-modinst->modname inst)
1328
:formals (list formal1)
1329
:actuals (list actual1))))
1330
(mv warnings db (cons note notes))))
1332
(defthm us-mark-wires-for-modinst-lvalue-arg-basics
1333
(implies (and (force (vl-emodwirelist-p actual-bits))
1334
(force (vl-emodwirelist-p formal-bits))
1335
(force (same-lengthp actual-bits formal-bits))
1336
(force (us-db-p sub-db))
1337
(force (us-db-p db))
1338
(force (vl-warninglist-p warnings))
1339
(force (vl-modinst-p inst))
1340
(force (us-notelist-p notes)))
1341
(let ((ret (us-mark-wires-for-modinst-lvalue-arg actual-bits formal-bits
1342
sub-db db warnings inst
1344
(and (vl-warninglist-p (mv-nth 0 ret))
1345
(us-db-p (mv-nth 1 ret))
1346
(us-notelist-p (mv-nth 2 ret)))))
1347
:hints(("Goal" :in-theory (enable us-mark-wires-for-modinst-lvalue-arg))))
1347
:args (list inst formal1 actual1)
1348
:fn 'us-mark-wires-for-modinst-lvalue-arg)))
1349
(mv (cons w warnings) db notes)))
1351
;; We just merge in the mask from formal1. If the formal is
1352
;; truly/falsely used, then this marks the actual as being
1353
;; truly/falsely used. If the formal is truly/falsely set, this marks
1354
;; the actual as being truly/falsely set.
1355
(formal1-mask (cdr formal1-look))
1356
;; Strip out any used above/below info
1357
(formal1-mask (acl2::bitset-difference formal1-mask *us-above-mask*))
1359
(us-mark-wire formal1-mask actual1 db warnings inst))
1360
(note (make-us-note :submod (vl-modinst->modname inst)
1361
:formals (list formal1)
1362
:actuals (list actual1))))
1363
(mv warnings db (cons note notes)))
1349
1365
(verify-guards us-mark-wires-for-modinst-lvalue-arg))
1354
(defsection us-mark-wires-for-modinst-rvalue-arg
1370
(define us-rvalue-mask
1356
1372
; Handler for module instance arguments whose expressions do NOT look like
1488
1498
:actuals expr-wires)))
1489
1499
(mv warnings db (cons note notes))))
1491
(defthm us-mark-wires-for-modinst-rvalue-arg-basics
1492
(implies (and (force (vl-expr-p expr))
1493
(force (vl-emodwirelist-p formal-bits))
1494
(force (us-db-p sub-db))
1495
(force (us-db-p db))
1496
(force (vl-wirealist-p walist))
1497
(force (vl-warninglist-p warnings))
1498
(force (vl-modinst-p inst))
1499
(force (us-notelist-p notes)))
1500
(let ((ret (us-mark-wires-for-modinst-rvalue-arg expr formal-bits
1502
warnings inst notes)))
1503
(and (vl-warninglist-p (mv-nth 0 ret))
1504
(us-db-p (mv-nth 1 ret))
1505
(us-notelist-p (mv-nth 2 ret)))))
1506
:hints(("Goal" :in-theory (enable us-mark-wires-for-modinst-rvalue-arg)))))
1510
(defsection us-mark-wires-for-modinst-arg
1512
(defund us-mark-wires-for-modinst-arg
1513
(arg ; the plainarg being connected to the port
1514
formal-bits ; the bits of the formal, in msb-first order
1515
sub-db ; db for the submodule
1516
db ; db for the superior module (may be extended)
1517
walist ; wire alist for the superior module
1518
warnings ; warnings accumulator for the superior module (may be extended)
1519
inst ; context for warnings and notes
1520
notes ; accumulator for notes (may be extended)
1522
"Returns (MV WARNINGS DB NOTES)"
1523
(declare (xargs :guard (and (vl-plainarg-p arg)
1524
(vl-emodwirelist-p formal-bits)
1527
(vl-wirealist-p walist)
1528
(vl-warninglist-p warnings)
1530
(us-notelist-p notes))))
1531
(b* ((expr (vl-plainarg->expr arg))
1533
;; Okay, nothing to do.
1534
(mv warnings db notes))
1535
((unless (vl-expr-lvaluep expr))
1536
(us-mark-wires-for-modinst-rvalue-arg expr formal-bits
1538
warnings inst notes))
1539
((mv successp warnings expr-bits)
1540
(vl-msb-expr-bitlist expr walist warnings))
1541
(len-okp (same-lengthp expr-bits formal-bits))
1543
(cond ((not successp)
1544
(cons (make-vl-warning
1545
:type :use-set-fudging
1546
:msg "~a0: failed to generate wires for ~a1; not ~
1502
(define us-mark-wires-for-modinst-arg
1503
((arg vl-plainarg-p) ; the plainarg being connected to the port
1504
(formal-bits vl-emodwirelist-p) ; the bits of the formal, in msb-first order
1505
(sub-db us-db-p) ; db for the submodule
1506
(db us-db-p) ; db for the superior module (may be extended)
1507
(walist vl-wirealist-p) ; wire alist for the superior module
1508
(warnings vl-warninglist-p) ; warnings accumulator for the superior module (may be extended)
1509
(inst vl-modinst-p) ; context for warnings and notes
1510
(notes us-notelist-p) ; accumulator for notes (may be extended)
1512
:returns (mv (warnings vl-warninglist-p)
1514
(notes us-notelist-p))
1515
(b* ((arg (vl-plainarg-fix arg)) ; the plainarg being connected to the port
1516
(formal-bits (vl-emodwirelist-fix formal-bits)) ; the bits of the formal, in msb-first order
1517
(sub-db (us-db-fix sub-db)) ; db for the submodule
1518
(db (us-db-fix db)) ; db for the superior module (may be extended)
1519
(walist (vl-wirealist-fix walist)) ; wire alist for the superior module
1520
(warnings (vl-warninglist-fix warnings)) ; warnings accumulator for the superior module (may be extended)
1521
(inst (vl-modinst-fix inst)) ; context for warnings and notes
1522
(notes (us-notelist-fix notes)) ; accumulator for notes (may be extended)
1523
(expr (vl-plainarg->expr arg))
1525
;; Okay, nothing to do.
1526
(mv warnings db notes))
1527
((unless (vl-expr-lvaluep expr))
1528
(us-mark-wires-for-modinst-rvalue-arg expr formal-bits
1530
warnings inst notes))
1531
((mv successp warnings expr-bits)
1532
(vl-msb-expr-bitlist expr walist warnings))
1533
(len-okp (same-lengthp expr-bits formal-bits))
1535
(cond ((not successp)
1536
(cons (make-vl-warning
1537
:type :use-set-fudging
1538
:msg "~a0: failed to generate wires for ~a1; not ~
1547
1539
inferring any use/set information from this ~
1549
:args (list inst expr)
1550
:fn 'us-mark-wires-for-modinst-arg)
1553
(cons (make-vl-warning
1554
:type :use-set-fudging
1555
:msg "~a0: width mismatch in port connection: expected ~x1 ~
1541
:args (list inst expr)
1542
:fn 'us-mark-wires-for-modinst-arg)
1545
(cons (make-vl-warning
1546
:type :use-set-fudging
1547
:msg "~a0: width mismatch in port connection: expected ~x1 ~
1556
1548
bits (~s2) but found ~x3 bits in ~a4. Not inferring ~
1557
1549
any use/set information from this port."
1560
(vl-verilogify-emodwirelist formal-bits)
1563
:fn 'us-mark-wires-for-modinst-arg)
1566
;; Okay, everything is fine.
1568
((unless (and successp len-okp))
1569
(mv warnings db notes)))
1570
(us-mark-wires-for-modinst-lvalue-arg expr-bits formal-bits
1571
sub-db db warnings inst notes)))
1573
(defthm us-mark-wires-for-modinst-arg-basics
1574
(implies (and (force (vl-plainarg-p arg))
1575
(force (vl-emodwirelist-p formal-bits))
1576
(force (us-db-p sub-db))
1577
(force (us-db-p db))
1578
(force (vl-wirealist-p walist))
1579
(force (vl-warninglist-p warnings))
1580
(force (vl-modinst-p inst))
1581
(force (us-notelist-p notes)))
1582
(let ((ret (us-mark-wires-for-modinst-arg arg formal-bits
1583
sub-db db walist warnings
1585
(and (vl-warninglist-p (mv-nth 0 ret))
1586
(us-db-p (mv-nth 1 ret))
1587
(us-notelist-p (mv-nth 2 ret)))))
1588
:hints(("Goal" :in-theory (enable us-mark-wires-for-modinst-arg)))))
1592
(defsection us-mark-wires-for-modinst-args
1594
(defund us-mark-wires-for-modinst-args
1595
(actuals ; plainarglist of the actual exprs being passed to the modinst
1596
portpat ; the port pattern for the submodule
1597
sub-db ; db for the submodule being instanced
1598
db ; db for the superior module (may be extended)
1599
walist ; wire alist for the superior module
1600
warnings ; warnings accumulator for the superior module (may be extended)
1601
inst ; the instance itself (context for any warnings and notes)
1602
notes ; accumulator for notes (may be extended)
1604
"Returns (MV WARNINGS DB NOTES)"
1605
(declare (xargs :guard (and (vl-plainarglist-p actuals)
1606
(vl-emodwirelistlist-p portpat)
1607
(same-lengthp actuals portpat)
1610
(vl-wirealist-p walist)
1611
(vl-warninglist-p warnings)
1613
(us-notelist-p notes))))
1614
(b* (((when (atom actuals))
1615
(mv warnings db notes))
1616
((mv warnings db notes)
1617
(us-mark-wires-for-modinst-arg (car actuals) (car portpat) sub-db db walist warnings inst notes))
1618
((mv warnings db notes)
1619
(us-mark-wires-for-modinst-args (cdr actuals) (cdr portpat) sub-db db walist warnings inst notes)))
1620
(mv warnings db notes)))
1622
(defthm us-mark-wires-for-modinst-args-basics
1623
(implies (and (force (vl-plainarglist-p actuals))
1624
(force (vl-emodwirelistlist-p portpat))
1625
(force (same-lengthp actuals portpat))
1626
(force (us-db-p sub-db))
1627
(force (us-db-p db))
1628
(force (vl-wirealist-p walist))
1629
(force (vl-warninglist-p warnings))
1630
(force (vl-modinst-p inst))
1631
(force (us-notelist-p notes)))
1632
(let ((ret (us-mark-wires-for-modinst-args actuals portpat
1633
sub-db db walist warnings
1635
(and (vl-warninglist-p (mv-nth 0 ret))
1636
(us-db-p (mv-nth 1 ret))
1637
(us-notelist-p (mv-nth 2 ret)))))
1638
:hints(("Goal" :in-theory (enable us-mark-wires-for-modinst-args)))))
1642
(defsection us-mark-wires-for-modinst
1644
(defund us-mark-wires-for-modinst
1645
(x ; the modinst to process
1646
walist ; walist for the current module
1647
db ; db for the current module (may be extended)
1649
modalist ; modalist for all modules
1650
dbalist ; dbalist-p that should bind every submodule (due to dependency order traversal)
1651
all-walists ; precomputed walists for all mods
1652
warnings ; warnings accumulator (may be extended)
1653
notes ; notes accumulator (may be extended)
1655
"Returns (MV WARNINGS DB NOTES)"
1656
(declare (xargs :guard (and (vl-modinst-p x)
1657
(vl-wirealist-p walist)
1659
(vl-modulelist-p mods)
1660
(equal modalist (vl-modalist mods))
1661
(us-dbalist-p dbalist)
1662
(equal all-walists (vl-nowarn-all-wirealists mods))
1663
(vl-warninglist-p warnings)
1664
(us-notelist-p notes))))
1665
(b* (((vl-modinst x) x)
1667
((unless (and (not x.range)
1668
(atom (vl-arguments->args x.paramargs))
1669
(eq (vl-arguments-kind x.portargs) :plain)))
1670
(b* ((w (make-vl-warning
1671
:type :use-set-fudging
1672
:msg "~a0: skipping this module instance because it has a ~
1552
(vl-verilogify-emodwirelist formal-bits)
1555
:fn 'us-mark-wires-for-modinst-arg)
1558
;; Okay, everything is fine.
1560
((unless (and successp len-okp))
1561
(mv warnings db notes)))
1562
(us-mark-wires-for-modinst-lvalue-arg expr-bits formal-bits
1563
sub-db db warnings inst notes)))
1566
(define us-mark-wires-for-modinst-args
1567
((actuals vl-plainarglist-p) ; plainarglist of the actual exprs being passed to the modinst
1568
(portpat vl-emodwirelistlist-p) ; the port pattern for the submodule
1569
(sub-db us-db-p) ; db for the submodule being instanced
1570
(db us-db-p) ; db for the superior module (may be extended)
1571
(walist vl-wirealist-p) ; wire alist for the superior module
1572
(warnings vl-warninglist-p) ; warnings accumulator for the superior module (may be extended)
1573
(inst vl-modinst-p) ; the instance itself (context for any warnings and notes)
1574
(notes us-notelist-p) ; accumulator for notes (may be extended)
1576
:measure (len (vl-plainarglist-fix actuals))
1577
:guard (same-lengthp actuals portpat)
1578
:returns (mv (warnings vl-warninglist-p)
1580
(notes us-notelist-p))
1581
(b* ((actuals (vl-plainarglist-fix actuals)) ; plainarglist of the actual exprs being passed to the modinst
1582
(portpat (vl-emodwirelistlist-fix portpat)) ; the port pattern for the submodule
1583
(sub-db (us-db-fix sub-db)) ; db for the submodule being instanced
1584
(db (us-db-fix db)) ; db for the superior module (may be extended)
1585
(walist (vl-wirealist-fix walist)) ; wire alist for the superior module
1586
(warnings (vl-warninglist-fix warnings)) ; warnings accumulator for the superior module (may be extended)
1587
(inst (vl-modinst-fix inst)) ; the instance itself (context for any warnings and notes)
1588
(notes (us-notelist-fix notes))
1589
((when (atom actuals))
1590
(mv warnings db notes))
1591
((mv warnings db notes)
1592
(us-mark-wires-for-modinst-arg (car actuals) (car portpat) sub-db db walist warnings inst notes))
1593
((mv warnings db notes)
1594
(us-mark-wires-for-modinst-args (cdr actuals) (cdr portpat) sub-db db walist warnings inst notes)))
1595
(mv warnings db notes)))
1598
(define us-mark-wires-for-modinst
1599
((x vl-modinst-p) ; the modinst to process
1600
(walist vl-wirealist-p) ; walist for the current module
1601
(db us-db-p) ; db for the current module (may be extended)
1602
(mods vl-modulelist-p)
1603
(ss vl-scopestack-p)
1604
(dbalist us-dbalist-p) ; dbalist-p that should bind every submodule (due to dependency order traversal)
1605
(all-walists (equal all-walists (vl-nowarn-all-wirealists mods))) ; precomputed walists for all mods
1606
(warnings vl-warninglist-p) ; warnings accumulator (may be extended)
1607
(notes us-notelist-p) ; notes accumulator (may be extended)
1609
(declare (ignorable mods))
1610
:returns (mv (warnings vl-warninglist-p)
1612
(notes us-notelist-p))
1613
(b* ((x (vl-modinst-fix x))
1614
(walist (vl-wirealist-fix walist))
1616
(dbalist (us-dbalist-fix dbalist))
1617
(warnings (vl-warninglist-fix warnings))
1618
(notes (us-notelist-fix notes))
1621
((unless (and (not x.range)
1622
(vl-paramargs-empty-p x.paramargs)
1623
(eq (vl-arguments-kind x.portargs) :vl-arguments-plain)))
1624
(b* ((w (make-vl-warning
1625
:type :use-set-fudging
1626
:msg "~a0: skipping this module instance because it has a ~
1673
1627
range, parameters, or unresolved arguments."
1674
:args (list x x.modname)
1675
:fn 'us-mark-wires-for-modinst)))
1676
(mv (cons w warnings) db notes)))
1678
(actuals (vl-arguments-plain->args x.portargs))
1680
(submod (vl-fast-find-module x.modname mods modalist))
1682
(b* ((w (make-vl-warning
1683
:type :use-set-fudging
1684
:msg "~a0: skipping this module instance because module ~m1 ~
1628
:args (list x x.modname)
1629
:fn 'us-mark-wires-for-modinst)))
1630
(mv (cons w warnings) db notes)))
1632
(actuals (vl-arguments-plain->args x.portargs))
1634
(submod (vl-scopestack-find-definition x.modname ss))
1635
((unless (and submod (eq (tag submod) :vl-module)))
1636
(b* ((w (make-vl-warning
1637
:type :use-set-fudging
1638
:msg "~a0: skipping this module instance because module ~m1 ~
1685
1639
was not found."
1686
:args (list x x.modname)
1687
:fn 'us-mark-wires-for-modinst)))
1688
(mv (cons w warnings) db notes)))
1640
:args (list x x.modname)
1641
:fn 'us-mark-wires-for-modinst)))
1642
(mv (cons w warnings) db notes)))
1690
(sub-db-look (hons-get x.modname dbalist))
1691
(sub-db (cdr sub-db-look))
1692
((unless sub-db-look)
1693
(b* ((w (make-vl-warning
1694
:type :use-set-fudging
1695
:msg "~a0: skipping this module instance because the use-set ~
1644
(sub-db-look (hons-get x.modname dbalist))
1645
(sub-db (cdr sub-db-look))
1646
((unless sub-db-look)
1647
(b* ((w (make-vl-warning
1648
:type :use-set-fudging
1649
:msg "~a0: skipping this module instance because the use-set ~
1696
1650
database for ~m1 was not found."
1697
:args (list x x.modname)
1698
:fn 'us-mark-wires-for-modinst)))
1699
(mv (cons w warnings) db notes)))
1651
:args (list x x.modname)
1652
:fn 'us-mark-wires-for-modinst)))
1653
(mv (cons w warnings) db notes)))
1701
(sub-walist-look (hons-get x.modname all-walists))
1702
(sub-walist (cdr sub-walist-look))
1703
((unless sub-walist-look)
1704
(b* ((w (make-vl-warning
1705
:type :use-set-fudging
1706
:msg "~a0: skipping this module instance because the wire ~
1655
(sub-walist-look (hons-get x.modname all-walists))
1656
(sub-walist (cdr sub-walist-look))
1657
((unless sub-walist-look)
1658
(b* ((w (make-vl-warning
1659
:type :use-set-fudging
1660
:msg "~a0: skipping this module instance because the wire ~
1707
1661
alist for ~m1 was not found."
1708
:args (list x x.modname)
1709
:fn 'us-mark-wires-for-modinst)))
1710
(mv (cons w warnings) db notes)))
1662
:args (list x x.modname)
1663
:fn 'us-mark-wires-for-modinst)))
1664
(mv (cons w warnings) db notes)))
1712
((mv successp warnings1 portpat)
1713
(vl-portlist-msb-bit-pattern (vl-module->ports submod) sub-walist))
1714
(warnings (append-without-guard warnings1 warnings))
1716
(b* ((w (make-vl-warning
1717
:type :use-set-fudging
1718
:msg "~a0: skipping this module instance because the port pattern ~
1666
((mv successp warnings1 portpat)
1667
(vl-portlist-msb-bit-pattern (vl-module->ports submod) sub-walist))
1668
(warnings (append-without-guard warnings1 warnings))
1670
(b* ((w (make-vl-warning
1671
:type :use-set-fudging
1672
:msg "~a0: skipping this module instance because the port pattern ~
1719
1673
for ~m1 was not successfully generated."
1720
:args (list x x.modname)
1721
:fn 'us-mark-wires-for-modinst)))
1722
(mv (cons w warnings) db notes)))
1674
:args (list x x.modname)
1675
:fn 'us-mark-wires-for-modinst)))
1676
(mv (cons w warnings) db notes)))
1724
((unless (same-lengthp portpat actuals))
1725
(b* ((w (make-vl-warning
1726
:type :use-set-fudging
1727
:msg "~a0: skipping this module instance because it has ~x1 arguments ~
1678
((unless (same-lengthp portpat actuals))
1679
(b* ((w (make-vl-warning
1680
:type :use-set-fudging
1681
:msg "~a0: skipping this module instance because it has ~x1 arguments ~
1728
1682
but we expected ~x2 arguments."
1729
:args (list x (len actuals) (len portpat))
1730
:fn 'us-mark-wires-for-modinst)))
1731
(mv (cons w warnings) db notes))))
1733
(us-mark-wires-for-modinst-args actuals portpat
1737
(defthm us-mark-wires-for-modinst-basics
1738
(implies (and (force (vl-modinst-p x))
1739
(force (vl-wirealist-p walist))
1740
(force (us-db-p db))
1741
(force (vl-modulelist-p mods))
1742
(force (equal modalist (vl-modalist mods)))
1743
(force (us-dbalist-p dbalist))
1744
(force (equal all-walists (vl-nowarn-all-wirealists mods)))
1745
(force (vl-warninglist-p warnings))
1746
(force (us-notelist-p notes)))
1747
(let ((ret (us-mark-wires-for-modinst x walist db mods modalist dbalist all-walists warnings notes)))
1748
(and (vl-warninglist-p (mv-nth 0 ret))
1749
(us-db-p (mv-nth 1 ret))
1750
(us-notelist-p (mv-nth 2 ret)))))
1751
:hints(("Goal" :in-theory (enable us-mark-wires-for-modinst)))))
1756
(defsection us-mark-wires-for-modinstlist
1758
(defund us-mark-wires-for-modinstlist
1759
(x ; the modinstlist to process
1760
walist ; walist for the current module
1761
db ; db for the current module (may be extended)
1763
modalist ; modalist for all modules
1764
dbalist ; dbalist-p that should bind every submodule (due to dependency order traversal)
1765
all-walists ; precomputed walists for all mods
1766
warnings ; warnings accumulator (may be extended)
1767
notes ; notes accumulator (may be extended)
1769
"Returns (MV WARNINGS DB NOTES)"
1770
(declare (xargs :guard (and (vl-modinstlist-p x)
1771
(vl-wirealist-p walist)
1773
(vl-modulelist-p mods)
1774
(equal modalist (vl-modalist mods))
1775
(us-dbalist-p dbalist)
1776
(equal all-walists (vl-nowarn-all-wirealists mods))
1777
(vl-warninglist-p warnings)
1778
(us-notelist-p notes))))
1779
(b* (((when (atom x))
1780
(mv warnings db notes))
1781
((mv warnings db notes)
1782
(us-mark-wires-for-modinst (car x) walist db mods modalist
1783
dbalist all-walists warnings notes))
1784
((mv warnings db notes)
1785
(us-mark-wires-for-modinstlist (cdr x) walist db mods modalist
1786
dbalist all-walists warnings notes)))
1787
(mv warnings db notes)))
1789
(defthm us-mark-wires-for-modinstlist-basics
1790
(implies (and (force (vl-modinstlist-p x))
1791
(force (vl-wirealist-p walist))
1792
(force (us-db-p db))
1793
(force (vl-modulelist-p mods))
1794
(force (equal modalist (vl-modalist mods)))
1795
(force (us-dbalist-p dbalist))
1796
(force (equal all-walists (vl-nowarn-all-wirealists mods)))
1797
(force (vl-warninglist-p warnings))
1798
(force (us-notelist-p notes)))
1799
(let ((ret (us-mark-wires-for-modinstlist x walist db mods modalist dbalist all-walists
1801
(and (vl-warninglist-p (mv-nth 0 ret))
1802
(us-db-p (mv-nth 1 ret))
1803
(us-notelist-p (mv-nth 2 ret)))))
1804
:hints(("Goal" :in-theory (enable us-mark-wires-for-modinstlist)))))
1810
(defsection us-union-masks
1812
(defund us-union-masks (super wires db warnings)
1813
"Returns (MV WARNINGS MASK)"
1814
(declare (xargs :guard (and (stringp super)
1815
(vl-emodwirelist-p wires)
1817
(vl-warninglist-p warnings))))
1818
(b* (((when (atom wires))
1820
((mv warnings cdr-mask)
1821
(us-union-masks super (cdr wires) db warnings))
1822
(entry1 (hons-get (car wires) db))
1824
(b* ((w (make-vl-warning
1825
:type :use-set-fudging
1826
:msg "In ~m0, expected use-set database entry for ~s1. ~
1683
:args (list x (len actuals) (len portpat))
1684
:fn 'us-mark-wires-for-modinst)))
1685
(mv (cons w warnings) db notes))))
1687
(us-mark-wires-for-modinst-args actuals portpat
1692
(define us-mark-wires-for-modinstlist
1693
((x vl-modinstlist-p) ; the modinstlist to process
1694
(walist vl-wirealist-p) ; walist for the current module
1695
(db us-db-p) ; db for the current module (may be extended)
1696
(mods vl-modulelist-p) ; all modules
1697
(ss vl-scopestack-p)
1698
(dbalist us-dbalist-p) ; dbalist-p that should bind every submodule (due to dependency order traversal)
1699
(all-walists (equal all-walists (vl-nowarn-all-wirealists mods))) ; precomputed walists for all mods
1700
(warnings vl-warninglist-p) ; warnings accumulator (may be extended)
1701
(notes us-notelist-p) ; notes accumulator (may be extended)
1703
:returns (mv (warnings vl-warninglist-p)
1705
(notes us-notelist-p))
1706
:measure (len (vl-modinstlist-fix x))
1707
(b* ((x (vl-modinstlist-fix x))
1708
(walist (vl-wirealist-fix walist))
1710
(mods (vl-modulelist-fix mods))
1711
(dbalist (us-dbalist-fix dbalist))
1712
(warnings (vl-warninglist-fix warnings))
1713
(notes (us-notelist-fix notes))
1715
(mv warnings db notes))
1716
((mv warnings db notes)
1717
(us-mark-wires-for-modinst (car x) walist db mods ss
1718
dbalist all-walists warnings notes))
1719
((mv warnings db notes)
1720
(us-mark-wires-for-modinstlist (cdr x) walist db mods ss
1721
dbalist all-walists warnings notes)))
1722
(mv warnings db notes)))
1728
(define us-union-masks ((super stringp)
1729
(wires vl-emodwirelist-p)
1731
(warnings vl-warninglist-p))
1732
:returns (mv (warnings vl-warninglist-p)
1734
:measure (len (vl-emodwirelist-fix wires))
1735
(b* ((super (string-fix super))
1736
(wires (vl-emodwirelist-fix wires))
1738
(warnings (vl-warninglist-fix warnings))
1739
((when (atom wires))
1741
((mv warnings cdr-mask)
1742
(us-union-masks super (cdr wires) db warnings))
1743
(entry1 (hons-get (car wires) db))
1745
(b* ((w (make-vl-warning
1746
:type :use-set-fudging
1747
:msg "In ~m0, expected use-set database entry for ~s1. ~
1827
1748
Assuming unused/unset. The used/set from above info ~
1828
1749
for ports may be incorrect."
1829
:args (list super (car wires))
1832
(mv (cons w warnings) cdr-mask)))
1833
(mask (acl2::bitset-insert (cdr entry1) cdr-mask)))
1834
(mv warnings mask)))
1836
(defthm us-union-masks-basics
1837
(implies (and (force (stringp super))
1838
(force (vl-emodwirelist-p wires))
1839
(force (us-db-p db))
1840
(force (vl-warninglist-p warnings)))
1841
(let ((ret (us-union-masks super wires db warnings)))
1842
(and (vl-warninglist-p (mv-nth 0 ret))
1843
(natp (mv-nth 1 ret)))))
1844
:hints(("Goal" :in-theory (enable us-union-masks)))))
1847
(defsection us-mark-wires-for-notes
1849
(defund us-mark-wires-for-notes (submod mask wires db reportcard)
1850
"Returns (MV REPORTCARD DB)"
1851
(declare (xargs :guard (and (stringp submod)
1853
(vl-emodwirelist-p wires)
1855
(vl-reportcard-p reportcard))))
1856
(b* (((when (atom wires))
1859
(us-mark-wires-for-notes submod mask (cdr wires) db reportcard))
1860
(wire1-look (hons-get (car wires) db))
1861
((unless wire1-look)
1862
(b* ((w (make-vl-warning
1863
:type :use-set-fudging
1864
:msg "Expected use-set database entry for ~s0. Ignoring this wire."
1865
:args (list (car wires))
1866
:fn 'us-mark-wires-for-notes
1868
(mv (vl-extend-reportcard submod w reportcard) db)))
1869
(curr-mask (cdr wire1-look))
1870
(new-mask (acl2::bitset-union curr-mask mask))
1871
((when (= curr-mask new-mask))
1874
(db (hons-acons (car wires) new-mask db)))
1875
(mv reportcard db)))
1877
(defthm us-mark-wires-for-notes-basics
1878
(implies (and (force (stringp submod))
1880
(force (vl-emodwirelist-p wires))
1881
(force (us-db-p db))
1882
(force (vl-reportcard-p reportcard)))
1883
(let ((ret (us-mark-wires-for-notes submod mask wires db reportcard)))
1884
(and (vl-reportcard-p (mv-nth 0 ret))
1885
(us-db-p (mv-nth 1 ret)))))
1886
:hints(("Goal" :in-theory (enable us-mark-wires-for-notes)))))
1889
(defsection us-apply-notes
1891
(defund us-apply-notes (super notes db dbalist reportcard)
1892
"Returns (MV REPORTCARD' DBALIST')"
1893
(declare (xargs :guard (and (stringp super)
1894
(us-notelist-p notes)
1895
(us-db-p db) ; DB for the current module
1896
(us-dbalist-p dbalist) ; DBS for the submodules
1897
(vl-reportcard-p reportcard))
1898
:verify-guards nil))
1899
(b* (((when (atom notes))
1900
(mv reportcard dbalist))
1902
((mv reportcard dbalist)
1903
(us-apply-notes super (cdr notes) db dbalist reportcard))
1905
((us-note note1) (car notes))
1907
(sub-db-look (hons-get note1.submod dbalist))
1908
(sub-db (cdr sub-db-look))
1909
((unless sub-db-look)
1910
(b* ((w (make-vl-warning
1911
:type :use-set-fudging
1912
:msg "Expected an entry for ~m0 in the dbalist. Failing to record ~
1750
:args (list super (car wires))
1753
(mv (cons w warnings) cdr-mask)))
1754
(mask (acl2::bitset-insert (cdr entry1) cdr-mask)))
1755
(mv warnings mask)))
1758
(define us-mark-wires-for-notes ((submod stringp)
1760
(wires vl-emodwirelist-p)
1762
(reportcard vl-reportcard-p))
1763
:returns (mv (reportcard vl-reportcard-p)
1765
:measure (len (vl-emodwirelist-fix wires))
1766
(b* ((submod (string-fix submod))
1768
(wires (vl-emodwirelist-fix wires))
1770
(reportcard (vl-reportcard-fix reportcard))
1771
((when (atom wires))
1774
(us-mark-wires-for-notes submod mask (cdr wires) db reportcard))
1775
(wire1-look (hons-get (car wires) db))
1776
((unless wire1-look)
1777
(b* ((w (make-vl-warning
1778
:type :use-set-fudging
1779
:msg "Expected use-set database entry for ~s0. Ignoring this wire."
1780
:args (list (car wires))
1781
:fn 'us-mark-wires-for-notes
1783
(mv (vl-extend-reportcard submod w reportcard) db)))
1784
(curr-mask (cdr wire1-look))
1785
(new-mask (acl2::bitset-union curr-mask mask))
1786
((when (= curr-mask new-mask))
1789
(db (hons-acons (car wires) new-mask db)))
1790
(mv reportcard db)))
1793
(define us-apply-notes ((super stringp)
1794
(notes us-notelist-p)
1795
(db us-db-p) ; DB for the current module
1796
(dbalist us-dbalist-p) ; DBS for the submodules
1797
(reportcard vl-reportcard-p))
1798
:returns (mv (reportcard vl-reportcard-p)
1799
(dbalist us-dbalist-p))
1801
:measure (len (us-notelist-fix notes))
1802
:hooks ((:fix :hints (("goal" :expand ((:free (super db dbalist reportcard)
1803
(us-apply-notes super notes db dbalist reportcard))
1804
(us-apply-notes super (us-notelist-fix notes)
1805
db dbalist reportcard))
1806
:do-not-induct t))))
1807
(b* ((super (string-fix super))
1808
(notes (us-notelist-fix notes))
1810
(dbalist (us-dbalist-fix dbalist))
1811
(reportcard (vl-reportcard-fix reportcard))
1812
((when (atom notes))
1813
(mv reportcard dbalist))
1815
((mv reportcard dbalist)
1816
(us-apply-notes super (cdr notes) db dbalist reportcard))
1818
((us-note note1) (car notes))
1820
(sub-db-look (hons-get note1.submod dbalist))
1821
(sub-db (cdr sub-db-look))
1822
((unless sub-db-look)
1823
(b* ((w (make-vl-warning
1824
:type :use-set-fudging
1825
:msg "Expected an entry for ~m0 in the dbalist. Failing to record ~
1913
1826
superior uses/sets of ~&1."
1914
:args (list note1.submod note1.formals)
1916
:fn 'us-apply-notes)))
1917
(mv (vl-extend-reportcard note1.submod w reportcard)
1920
((mv warnings actuals-mask)
1921
(us-union-masks super note1.actuals db nil))
1923
(reportcard (if (consp warnings)
1924
(vl-extend-reportcard-list note1.submod warnings reportcard)
1928
;; a wire is used above the submodule if used in the current module or
1929
;; used above the current module.
1930
(above-mask (if (or (acl2::bitset-memberp *us-truly-setp* actuals-mask)
1931
(acl2::bitset-memberp *us-truly-set-abovep* actuals-mask))
1932
(acl2::bitset-insert *us-truly-set-abovep* above-mask)
1934
(above-mask (if (or (acl2::bitset-memberp *us-truly-usedp* actuals-mask)
1935
(acl2::bitset-memberp *us-truly-used-abovep* actuals-mask))
1936
(acl2::bitset-insert *us-truly-used-abovep* above-mask)
1939
((mv reportcard new-sub-db) (us-mark-wires-for-notes note1.submod above-mask note1.formals sub-db reportcard))
1940
(dbalist (hons-acons note1.submod new-sub-db dbalist))
1943
(mv reportcard dbalist)))
1945
(defthm us-apply-notes-basics
1946
(implies (and (force (stringp super))
1947
(force (us-notelist-p notes))
1948
(force (us-db-p db))
1949
(force (us-dbalist-p dbalist))
1950
(force (vl-reportcard-p reportcard)))
1951
(let ((ret (us-apply-notes super notes db dbalist reportcard)))
1952
(and (vl-reportcard-p (mv-nth 0 ret))
1953
(us-dbalist-p (mv-nth 1 ret))
1956
:do-not '(generalize fertilize eliminate-destructors)
1957
:in-theory (enable us-apply-notes))))
1827
:args (list note1.submod note1.formals)
1829
:fn 'us-apply-notes)))
1830
(mv (vl-extend-reportcard note1.submod w reportcard)
1833
((mv warnings actuals-mask)
1834
(us-union-masks super note1.actuals db nil))
1836
(reportcard (if (consp warnings)
1837
(vl-extend-reportcard-list note1.submod warnings reportcard)
1841
;; a wire is used above the submodule if used in the current module or
1842
;; used above the current module.
1843
(above-mask (if (or (acl2::bitset-memberp *us-truly-setp* actuals-mask)
1844
(acl2::bitset-memberp *us-truly-set-abovep* actuals-mask))
1845
(acl2::bitset-insert *us-truly-set-abovep* above-mask)
1847
(above-mask (if (or (acl2::bitset-memberp *us-truly-usedp* actuals-mask)
1848
(acl2::bitset-memberp *us-truly-used-abovep* actuals-mask))
1849
(acl2::bitset-insert *us-truly-used-abovep* above-mask)
1852
((mv reportcard new-sub-db) (us-mark-wires-for-notes note1.submod above-mask note1.formals sub-db reportcard))
1853
(dbalist (hons-acons note1.submod new-sub-db dbalist))
1856
(mv reportcard dbalist))
1959
1858
(verify-guards us-apply-notes))
1963
(defsection us-apply-notesalist
1965
(defund us-apply-notesalist (x notealist dbalist reportcard)
1966
"Returns (MV REPORTCARD' DBALIST')"
1967
(declare (xargs :guard (and (vl-modulelist-p x)
1968
(us-notealist-p notealist)
1969
(us-dbalist-p dbalist)
1970
(vl-reportcard-p reportcard))))
1971
(b* (((when (atom x))
1972
(mv reportcard dbalist))
1974
((vl-module x1) (car x))
1975
(db-look (hons-get x1.name dbalist))
1976
(notes-look (hons-get x1.name notealist))
1978
(notes (cdr notes-look))
1980
(if (and db-look notes-look)
1982
(b* ((w (make-vl-warning
1983
:type :use-set-fudging
1984
:msg "Expected use-set database and notes for ~
1861
(define us-apply-notesalist ((x vl-modulelist-p)
1862
(notealist us-notealist-p)
1863
(dbalist us-dbalist-p)
1864
(reportcard vl-reportcard-p))
1865
:returns (mv (reportcard vl-reportcard-p)
1866
(dbalist us-dbalist-p))
1867
:measure (len (vl-modulelist-fix x))
1868
(b* ((x (vl-modulelist-fix x))
1869
(notealist (us-notealist-fix notealist))
1870
(dbalist (us-dbalist-fix dbalist))
1871
(reportcard (vl-reportcard-fix reportcard))
1873
(mv reportcard dbalist))
1875
((vl-module x1) (car x))
1876
(db-look (hons-get x1.name dbalist))
1877
(notes-look (hons-get x1.name notealist))
1879
(notes (cdr notes-look))
1881
(if (and db-look notes-look)
1883
(b* ((w (make-vl-warning
1884
:type :use-set-fudging
1885
:msg "Expected use-set database and notes for ~
1985
1886
module ~m0. Not propagating used/set from ~
1986
1887
above information."
1987
:args (list x1.name)
1989
:fn 'us-apply-notesalist)))
1990
(vl-extend-reportcard x1.name w reportcard))))
1991
((mv reportcard dbalist)
1992
(us-apply-notes x1.name notes db dbalist reportcard))
1993
((mv reportcard dbalist)
1994
(us-apply-notesalist (cdr x) notealist dbalist reportcard)))
1995
(mv reportcard dbalist)))
1997
(defthm us-apply-notesalist-basics
1998
(implies (and (force (vl-modulelist-p x))
1999
(force (us-notealist-p notealist))
2000
(force (us-dbalist-p dbalist))
2001
(force (vl-reportcard-p reportcard)))
2002
(let ((ret (us-apply-notesalist x notealist dbalist reportcard)))
2003
(and (vl-reportcard-p (mv-nth 0 ret))
2004
(us-dbalist-p (mv-nth 1 ret)))))
2005
:hints(("Goal" :in-theory (enable us-apply-notesalist)))))
2009
(defalist us-results-p (x)
2011
:val (vl-emodwirelist-p x)
1888
:args (list x1.name)
1890
:fn 'us-apply-notesalist)))
1891
(vl-extend-reportcard x1.name w reportcard))))
1892
((mv reportcard dbalist)
1893
(us-apply-notes x1.name notes db dbalist reportcard))
1894
((mv reportcard dbalist)
1895
(us-apply-notesalist (cdr x) notealist dbalist reportcard)))
1896
(mv reportcard dbalist)))
1899
(fty::defalist us-results
1901
:val-type vl-emodwirelist-p
2012
1902
:keyp-of-nil nil
2013
1903
:valp-of-nil t)
2016
(defsection us-organize-results
1906
(define us-organize-results-aux
2018
1908
; Invert the database so that each bit-set is associated with the list of wires
2019
1909
; that have it. This way you can extract the wires that have any particular
2023
1913
; ASSUMES THE DATABSE HAS ALREADY BEEN SHRUNK.
2025
(defund us-organize-results-aux (db buckets)
2026
;; DB binds names to masks. Buckets binds masks to names.
2027
(declare (xargs :guard (us-db-p db)))
2028
(b* (((when (atom db))
2032
(val1-wires (cdr (hons-get val1 buckets)))
2033
(buckets (hons-acons val1 (cons name1 val1-wires) buckets)))
2034
(us-organize-results-aux (cdr db) buckets)))
2036
(defthm us-results-p-of-us-organize-results-aux
2037
(implies (and (force (us-db-p db))
2038
(force (us-results-p buckets)))
2039
(us-results-p (us-organize-results-aux db buckets)))
2041
:do-not '(generalize fertilize)
2042
:in-theory (e/d (us-organize-results-aux)
2045
(defund us-organize-results (db)
2046
(declare (xargs :guard (us-db-p db)))
1916
(buckets us-results-p))
1917
:returns (buckets us-results-p)
1918
:measure (len (us-db-fix db))
1919
;; DB binds names to masks. Buckets binds masks to names.
1920
(b* ((db (us-db-fix db))
1921
(buckets (us-results-fix buckets))
1926
(val1-wires (cdr (hons-get val1 buckets)))
1927
(buckets (hons-acons val1 (cons name1 val1-wires) buckets)))
1928
(us-organize-results-aux (cdr db) buckets)))
1931
(define us-organize-results ((db us-db-p))
1932
:returns (buckets us-results-p)
2047
1933
(b* ((temp (us-organize-results-aux db nil))
2048
1934
(ret (hons-shrink-alist temp nil))
2049
1935
(- (fast-alist-free temp))
2050
1936
(- (fast-alist-free ret)))
2053
(defthm us-results-p-of-us-organize-results
2054
(implies (force (us-db-p db))
2055
(us-results-p (us-organize-results db)))
2056
:hints(("Goal" :in-theory (enable us-organize-results)))))
2059
(defsection us-filter-db-by-names
1940
(define us-filter-db-by-names1
2061
1942
;; Get entries that have particular names
2063
1944
; ASSUMES THE DATABSE HAS ALREADY BEEN SHRUNK
2065
(defund us-filter-db-by-names1 (names names-fal db yes no)
2066
"Returns (MV YES NO), slow alists."
2067
(declare (xargs :guard (and (equal names-fal (make-lookup-alist names))
2069
(b* (((when (atom db))
2072
(if (fast-memberp (caar db) names names-fal)
2073
(mv (cons (car db) yes) no)
2074
(mv yes (cons (car db) no)))))
2075
(us-filter-db-by-names1 names names-fal (cdr db) yes no)))
2077
(defund us-filter-db-by-names (names db)
2078
"Returns (MV YES NO), slow alists."
2079
(declare (xargs :guard (us-db-p db)))
2080
(b* ((fal (make-lookup-alist names))
2081
((mv yes no) (us-filter-db-by-names1 names fal db nil nil))
2082
(- (fast-alist-free fal)))
2085
(defthm us-filter-db-by-names1-basics
2086
(implies (and (force (equal names-fal (make-lookup-alist names)))
2087
(force (us-db-p db))
2088
(force (us-db-p yes))
2089
(force (us-db-p no)))
2090
(let ((ret (us-filter-db-by-names1 names names-fal db yes no)))
2091
(and (us-db-p (mv-nth 0 ret))
2092
(us-db-p (mv-nth 1 ret)))))
2093
:hints(("Goal" :in-theory (enable us-filter-db-by-names1))))
2095
(defthm us-filter-db-by-names-basics
2096
(implies (force (us-db-p db))
2097
(let ((ret (us-filter-db-by-names names db)))
2098
(and (us-db-p (mv-nth 0 ret))
2099
(us-db-p (mv-nth 1 ret)))))
2100
:hints(("Goal" :in-theory (enable us-filter-db-by-names)))))
2103
(defsection us-filter-db-by-bit
1946
(names names-fal (db us-db-p) (yes us-db-p) (no us-db-p))
1947
:returns (mv (yes us-db-p)
1949
:guard (equal names-fal (make-lookup-alist names))
1950
:measure (len (us-db-fix db))
1951
(b* ((db (us-db-fix db))
1952
(yes (us-db-fix yes))
1957
(if (fast-memberp (caar db) names names-fal)
1958
(mv (cons (car db) yes) no)
1959
(mv yes (cons (car db) no)))))
1960
(us-filter-db-by-names1 names names-fal (cdr db) yes no)))
1962
(define us-filter-db-by-names (names (db us-db-p))
1963
:returns (mv (yes us-db-p) ;; slow alists
1965
(b* ((fal (make-lookup-alist names))
1966
((mv yes no) (us-filter-db-by-names1 names fal db nil nil))
1967
(- (fast-alist-free fal)))
1971
(define us-filter-db-by-bit1
2105
1973
;; Get entries that have a particular bit set
2107
1975
; ASSUMES THE DATABSE HAS ALREADY BEEN SHRUNK
2109
(defund us-filter-db-by-bit1 (bit db yes no)
2110
"Returns (MV YES NO), slow alists."
2111
(declare (xargs :guard (and (natp bit)
2113
(b* (((when (atom db))
2116
(if (acl2::bitset-memberp bit (cdar db))
2117
(mv (cons (car db) yes) no)
2118
(mv yes (cons (car db) no)))))
2119
(us-filter-db-by-bit1 bit (cdr db) yes no)))
2121
(defund us-filter-db-by-bit (bit db)
2122
"Returns (MV YES NO), slow alists."
2123
(declare (xargs :guard (and (natp bit)
2125
(us-filter-db-by-bit1 bit db nil nil))
2127
(defthm us-filter-db-by-bit1-basics
2128
(implies (and (force (natp bit))
2129
(force (us-db-p db))
2130
(force (us-db-p yes))
2131
(force (us-db-p no)))
2132
(let ((ret (us-filter-db-by-bit1 bit db yes no)))
2133
(and (us-db-p (mv-nth 0 ret))
2134
(us-db-p (mv-nth 1 ret)))))
2135
:hints(("Goal" :in-theory (enable us-filter-db-by-bit1))))
2137
(defthm us-filter-db-by-bit-basics
2138
(implies (and (force (natp bit))
2139
(force (us-db-p db)))
2140
(let ((ret (us-filter-db-by-bit bit db)))
2141
(and (us-db-p (mv-nth 0 ret))
2142
(us-db-p (mv-nth 1 ret)))))
2143
:hints(("Goal" :in-theory (enable us-filter-db-by-bit)))))
2146
(defsection us-filter-db-by-mask
1981
:returns (mv (yes us-db-p) ;; slow alists
1983
:measure (len (us-db-fix db))
1984
(b* ((db (us-db-fix db))
1985
(yes (us-db-fix yes))
1991
(if (acl2::bitset-memberp bit (cdar db))
1992
(mv (cons (car db) yes) no)
1993
(mv yes (cons (car db) no)))))
1994
(us-filter-db-by-bit1 bit (cdr db) yes no)))
1996
(define us-filter-db-by-bit ((bit natp) (db us-db-p))
1997
:returns (mv (yes us-db-p) ;; slow alists
1999
(us-filter-db-by-bit1 bit db nil nil))
2001
(define us-filter-db-by-mask1
2148
2003
;; Get entries that have exactly some mask
2150
2005
; ASSUMES THE DATABSE HAS ALREADY BEEN SHRUNK
2152
(defund us-filter-db-by-mask1 (mask db yes no)
2153
"Returns (MV YES NO), slow alists."
2154
(declare (xargs :guard (and (natp mask)
2156
(b* (((when (atom db))
2159
(if (equal mask (cdar db))
2160
(mv (cons (car db) yes) no)
2161
(mv yes (cons (car db) no)))))
2162
(us-filter-db-by-mask1 mask (cdr db) yes no)))
2164
(defund us-filter-db-by-mask (mask db)
2165
"Returns (MV YES NO), slow alists."
2166
(declare (xargs :guard (and (natp mask)
2168
(us-filter-db-by-mask1 mask db nil nil))
2170
(defthm us-filter-db-by-mask1-basics
2171
(implies (and (force (natp mask))
2172
(force (us-db-p db))
2173
(force (us-db-p yes))
2174
(force (us-db-p no)))
2175
(let ((ret (us-filter-db-by-mask1 mask db yes no)))
2176
(and (us-db-p (mv-nth 0 ret))
2177
(us-db-p (mv-nth 1 ret)))))
2178
:hints(("Goal" :in-theory (enable us-filter-db-by-mask1))))
2180
(defthm us-filter-db-by-mask-basics
2181
(implies (and (force (natp mask))
2182
(force (us-db-p db)))
2183
(let ((ret (us-filter-db-by-mask mask db)))
2184
(and (us-db-p (mv-nth 0 ret))
2185
(us-db-p (mv-nth 1 ret)))))
2186
:hints(("Goal" :in-theory (enable us-filter-db-by-mask)))))
2189
(defsection us-warn-nonport-results
2191
(defund us-warn-nonport-results (modname x)
2192
(declare (xargs :guard (and (stringp modname)
2194
(b* (((when (atom x))
2198
((when (atom wires))
2199
(us-warn-nonport-results modname (cdr x)))
2201
(- (or (not (or (acl2::bitset-memberp *us-truly-used-abovep* mask)
2202
(acl2::bitset-memberp *us-truly-set-abovep* mask)))
2203
(cw "Errr... non-ports marked used/set above??? something is wrong.~%")))
2206
(usedp (acl2::bitset-memberp *us-truly-usedp* mask))
2207
(setp (acl2::bitset-memberp *us-truly-setp* mask))
2208
((when (and usedp setp))
2209
;; It's fine, no reason to warn about it. We've already warned
2210
;; about trainwrecks earlier.
2211
(us-warn-nonport-results modname (cdr x)))
2213
;; falsely used/set but not truly used/set?
2214
(fusedp (and (not usedp) (acl2::bitset-memberp *us-falsely-usedp* mask)))
2215
(fsetp (and (not setp) (acl2::bitset-memberp *us-falsely-setp* mask)))
2217
(pluralp (vl-plural-p wires))
2218
(|wire(s)| (if pluralp "wires" "wire"))
2219
(|are| (if pluralp "are" "is"))
2222
;; New summary line for Terry
2223
(cat (natstr (len wires))
2224
(cond (usedp " unset bit")
2225
(setp " unused bit")
2226
(t " spurious bit"))
2227
(if pluralp "s. " ". ")))
2231
:type (cond (usedp (if fsetp
2232
:use-set-warn-1-unset-tricky
2233
:use-set-warn-1-unset))
2235
:use-set-warn-2-unused-tricky
2236
:use-set-warn-2-unused))
2237
(t (if (or fusedp fsetp)
2238
:use-set-warn-3-spurious-tricky
2239
:use-set-warn-3-spurious)))
2240
:msg (cat summary-line
2241
(cond (usedp "These ~s0 ~s1 never set: ~&2.")
2242
(setp "These ~s0 ~s1 never used: ~&2.")
2243
(t "These ~s0 ~s1 never used or set: ~&2.")))
2244
:args (list |wire(s)|
2246
(cwtime (vl-verilogify-emodwirelist wires)
2249
:fn 'us-warn-nonport-results)))
2252
(us-warn-nonport-results modname (cdr x)))))
2254
(defthm vl-warninglist-p-of-us-warn-nonport-results
2255
(vl-warninglist-p (us-warn-nonport-results modname x))
2256
:hints(("Goal" :in-theory (enable us-warn-nonport-results)))))
2258
(define vl-netdecls-for-flattened-hids ((x vl-netdecllist-p))
2259
:returns (flattened-decls vl-netdecllist-p :hyp :fguard)
2007
((mask natp) (db us-db-p) (yes us-db-p) (no us-db-p))
2008
:returns (mv (yes us-db-p) ;; slow alists
2010
:measure (len (us-db-fix db))
2011
(b* ((db (us-db-fix db))
2012
(yes (us-db-fix yes))
2018
(if (equal mask (cdar db))
2019
(mv (cons (car db) yes) no)
2020
(mv yes (cons (car db) no)))))
2021
(us-filter-db-by-mask1 mask (cdr db) yes no)))
2023
(define us-filter-db-by-mask ((mask natp)
2025
:returns (mv (yes us-db-p) ;; slow alists
2027
(declare (xargs :guard (and (natp mask)
2029
(us-filter-db-by-mask1 mask db nil nil))
2033
(define us-warn-nonport-results ((modname stringp)
2035
:returns (warnings vl-warninglist-p)
2036
:measure (len (us-results-fix x))
2037
(b* ((modname (string-fix modname))
2038
(x (us-results-fix x))
2043
((when (atom wires))
2044
(us-warn-nonport-results modname (cdr x)))
2046
(- (or (not (or (acl2::bitset-memberp *us-truly-used-abovep* mask)
2047
(acl2::bitset-memberp *us-truly-set-abovep* mask)))
2048
(cw "Errr... non-ports marked used/set above??? something is wrong.~%")))
2051
(usedp (acl2::bitset-memberp *us-truly-usedp* mask))
2052
(setp (acl2::bitset-memberp *us-truly-setp* mask))
2053
((when (and usedp setp))
2054
;; It's fine, no reason to warn about it. We've already warned
2055
;; about trainwrecks earlier.
2056
(us-warn-nonport-results modname (cdr x)))
2058
;; falsely used/set but not truly used/set?
2059
(fusedp (and (not usedp) (acl2::bitset-memberp *us-falsely-usedp* mask)))
2060
(fsetp (and (not setp) (acl2::bitset-memberp *us-falsely-setp* mask)))
2062
(pluralp (vl-plural-p wires))
2063
(|wire(s)| (if pluralp "wires" "wire"))
2064
(|are| (if pluralp "are" "is"))
2067
;; New summary line for Terry
2068
(cat (natstr (len wires))
2069
(cond (usedp " unset bit")
2070
(setp " unused bit")
2071
(t " spurious bit"))
2072
(if pluralp "s. " ". ")))
2076
:type (cond (usedp (if fsetp
2077
:use-set-warn-1-unset-tricky
2078
:use-set-warn-1-unset))
2080
:use-set-warn-2-unused-tricky
2081
:use-set-warn-2-unused))
2082
(t (if (or fusedp fsetp)
2083
:use-set-warn-3-spurious-tricky
2084
:use-set-warn-3-spurious)))
2085
:msg (cat summary-line
2086
(cond (usedp "These ~s0 ~s1 never set: ~&2.")
2087
(setp "These ~s0 ~s1 never used: ~&2.")
2088
(t "These ~s0 ~s1 never used or set: ~&2.")))
2089
:args (list |wire(s)|
2091
(cwtime (vl-verilogify-emodwirelist wires)
2094
:fn 'us-warn-nonport-results)))
2097
(us-warn-nonport-results modname (cdr x)))))
2100
(define vl-vardecls-for-flattened-hids ((x vl-vardecllist-p))
2101
:returns (flattened-decls vl-vardecllist-p)
2260
2102
(cond ((atom x)
2262
((assoc-equal "VL_HID_RESOLVED_MODULE_NAME" (vl-netdecl->atts (car x)))
2263
(cons (car x) (vl-netdecls-for-flattened-hids (cdr x))))
2104
((assoc-equal "VL_HID_RESOLVED_MODULE_NAME" (vl-vardecl->atts (car x)))
2105
(cons (vl-vardecl-fix (car x)) (vl-vardecls-for-flattened-hids (cdr x))))
2265
(vl-netdecls-for-flattened-hids (cdr x)))))
2107
(vl-vardecls-for-flattened-hids (cdr x)))))
2267
(define vl-netdecllist-wires
2268
((x vl-netdecllist-p)
2109
(define vl-vardecllist-wires
2110
((x vl-vardecllist-p)
2269
2111
(walist vl-wirealist-p)
2270
2112
(warnings vl-warninglist-p))
2271
2113
:returns (mv (successp booleanp :rule-classes :type-prescription)
2272
2114
(warnings vl-warninglist-p)
2273
(wires vl-emodwirelist-p :hyp :fguard))
2115
(wires vl-emodwirelist-p))
2274
2116
(b* (((when (atom x))
2275
2117
(mv t (ok) nil))
2276
(car-look (hons-get (vl-netdecl->name (car x)) walist))
2118
(walist (vl-wirealist-fix walist))
2119
((vl-vardecl x1) (vl-vardecl-fix (car x)))
2120
(car-look (hons-get x1.name walist))
2277
2121
(car-wires (cdr car-look))
2278
2122
(warnings (if car-look
2280
2124
(warn :type :use-set-fudging
2281
:msg "~a0: No wires for this net?"
2282
:args (list (car x)))))
2125
:msg "~a0: No wires for this variable?"
2283
2127
((mv cdr-successp warnings cdr-wires)
2284
(vl-netdecllist-wires (cdr x) walist warnings)))
2128
(vl-vardecllist-wires (cdr x) walist warnings)))
2285
2129
(mv (and car-look cdr-successp)
2287
2131
(append car-wires cdr-wires))))
2289
2133
(define us-report-mod ((x vl-module-p)
2134
(ss vl-scopestack-p)
2290
2135
(dbalist us-dbalist-p)
2291
2136
(walist vl-wirealist-p))
2292
:returns (new-x vl-module-p :hyp :fguard)
2293
(b* (((vl-module x) x)
2137
:returns (new-x vl-module-p)
2138
(b* (((vl-module x) (vl-module-fix x))
2294
2139
(warnings x.warnings)
2140
(dbalist (us-dbalist-fix dbalist))
2141
(walist (vl-wirealist-fix walist))
2296
2142
(entry (hons-get x.name dbalist))
2143
(ss (vl-scopestack-push x ss))
2297
2144
(db (cdr entry))
2298
2145
((unless entry)
2299
2146
(b* ((warnings (warn :type :use-set-fudging
2443
2288
(mv x-prime dbalist reportcard notealist)))
2445
(defthm us-analyze-mod-basics
2446
(implies (and (force (vl-module-p x))
2447
(force (vl-modulelist-p mods))
2448
(force (equal modalist (vl-modalist mods)))
2449
(force (us-dbalist-p dbalist))
2450
(force (equal all-walists (vl-nowarn-all-wirealists mods)))
2451
(force (vl-reportcard-p reportcard))
2452
(force (string-listp toplevel))
2453
(force (us-notealist-p notealist)))
2454
(let ((ret (us-analyze-mod x mods modalist dbalist all-walists reportcard toplevel notealist)))
2455
(and (vl-module-p (mv-nth 0 ret))
2456
(us-dbalist-p (mv-nth 1 ret))
2457
(vl-reportcard-p (mv-nth 2 ret))
2458
(us-notealist-p (mv-nth 3 ret)))))
2459
:hints(("Goal" :in-theory (enable us-analyze-mod)))))
2463
(defsection us-analyze-mods
2465
(defund us-analyze-mods-aux (x mods modalist dbalist all-walists reportcard toplevel notealist)
2466
"Returns (MV X' DBALIST' REPORTCARD')"
2467
(declare (xargs :guard (and (vl-modulelist-p x)
2468
(vl-modulelist-p mods)
2469
(equal modalist (vl-modalist mods))
2470
(us-dbalist-p dbalist)
2471
(equal all-walists (vl-nowarn-all-wirealists mods))
2472
(vl-reportcard-p reportcard)
2473
(string-listp toplevel)
2474
(us-notealist-p notealist))))
2475
(b* (((when (atom x))
2476
(mv nil dbalist reportcard notealist))
2477
((mv car-prime dbalist reportcard notealist)
2478
(us-analyze-mod (car x) mods modalist dbalist
2479
all-walists reportcard toplevel notealist))
2480
((mv cdr-prime dbalist reportcard notealist)
2481
(us-analyze-mods-aux (cdr x) mods modalist dbalist
2482
all-walists reportcard toplevel notealist))
2483
(x-prime (cons car-prime cdr-prime)))
2484
(mv x-prime dbalist reportcard notealist)))
2486
(defthm us-analyze-mods-aux-basics
2487
(implies (and (force (vl-modulelist-p x))
2488
(force (vl-modulelist-p mods))
2489
(force (equal modalist (vl-modalist mods)))
2490
(force (us-dbalist-p dbalist))
2491
(force (equal all-walists (vl-nowarn-all-wirealists mods)))
2492
(force (vl-reportcard-p reportcard))
2493
(force (string-listp toplevel))
2494
(force (us-notealist-p notealist)))
2495
(let ((ret (us-analyze-mods-aux x mods modalist dbalist all-walists reportcard toplevel notealist)))
2496
(and (vl-modulelist-p (mv-nth 0 ret))
2497
(us-dbalist-p (mv-nth 1 ret))
2498
(vl-reportcard-p (mv-nth 2 ret))
2499
(us-notealist-p (mv-nth 3 ret)))))
2500
:hints(("Goal" :in-theory (enable us-analyze-mods-aux))))
2502
(defund us-analyze-mods (x)
2503
"Returns (MV X-PRIME DBALIST)"
2504
(declare (xargs :guard (vl-modulelist-p x)
2506
;; bozo check port bits
2507
(b* ((x (cwtime (vl-deporder-sort x) :mintime 1/2))
2508
(modalist (cwtime (vl-modalist x) :mintime 1/2))
2509
(toplevel (cwtime (vl-modulelist-toplevel x) :mintime 1/2))
2510
((mv warnings-alist all-walists)
2511
(cwtime (vl-modulelist-all-wirealists x)
2514
((mv x-prime dbalist warnings-alist notealist)
2515
;; pass 1: analyze the modules in dependency order, bottom-up,
2516
;; generating their initial dbalists and notes.
2517
(cwtime (us-analyze-mods-aux x x modalist (len x)
2518
all-walists warnings-alist
2521
(- (fast-alist-free modalist))
2523
((mv warnings-alist dbalist)
2524
;; pass2: apply the notes in reverse dependency order, top-down,
2525
;; marking which ports are used/set anywhere above
2526
(cwtime (us-apply-notesalist (rev x-prime) notealist dbalist
2529
(- (fast-alist-free notealist))
2532
(cwtime (vl-modulelist-apply-reportcard x-prime warnings-alist)
2534
(- (fast-alist-free warnings-alist))
2537
(cwtime (us-report-mods x-prime x dbalist all-walists)
2540
(- (fast-alist-free-each-alist-val all-walists))
2541
(- (fast-alist-free all-walists)))
2543
;; bozo probably free other stuff -- walists, etc.
2544
(mv x-prime dbalist)))
2546
(defthm us-analyze-mods-basics
2547
(implies (force (vl-modulelist-p x))
2548
(let ((ret (us-analyze-mods x)))
2549
(and (vl-modulelist-p (mv-nth 0 ret))
2550
(us-dbalist-p (mv-nth 1 ret)))))
2551
:hints(("Goal" :in-theory (enable us-analyze-mods)))))
2291
(define us-analyze-mods-aux ((x vl-modulelist-p)
2292
(mods vl-modulelist-p)
2293
(ss vl-scopestack-p)
2294
(dbalist us-dbalist-p)
2295
(all-walists (equal all-walists (vl-nowarn-all-wirealists mods)))
2296
(reportcard vl-reportcard-p)
2297
(toplevel string-listp)
2298
(notealist us-notealist-p))
2299
"Returns (MV X' DBALIST' REPORTCARD')"
2300
:returns (mv (x-prime vl-modulelist-p)
2301
(dbalist us-dbalist-p)
2302
(rcard vl-reportcard-p)
2303
(nalist us-notealist-p))
2304
(b* (((when (atom x))
2306
(us-dbalist-fix dbalist)
2307
(vl-reportcard-fix reportcard)
2308
(us-notealist-fix notealist)))
2309
((mv car-prime dbalist reportcard notealist)
2310
(us-analyze-mod (car x) mods ss dbalist
2311
all-walists reportcard toplevel notealist))
2312
((mv cdr-prime dbalist reportcard notealist)
2313
(us-analyze-mods-aux (cdr x) mods ss dbalist
2314
all-walists reportcard toplevel notealist))
2315
(x-prime (cons car-prime cdr-prime)))
2316
(mv x-prime dbalist reportcard notealist)))
2318
(define us-analyze-mods ((x vl-modulelist-p) (ss vl-scopestack-p))
2319
"Returns (MV X-PRIME DBALIST)"
2320
:returns (mv (x-prime vl-modulelist-p)
2321
(dbalist us-dbalist-p))
2322
;; bozo check port bits
2323
(b* ((toplevel (cwtime (vl-modulelist-toplevel x) :mintime 1/2))
2324
((mv warnings-alist all-walists)
2325
(cwtime (vl-modulelist-all-wirealists x)
2328
((mv x-prime dbalist warnings-alist notealist)
2329
;; pass 1: analyze the modules in dependency order, bottom-up,
2330
;; generating their initial dbalists and notes.
2331
(cwtime (us-analyze-mods-aux x x ss (len x)
2332
all-walists warnings-alist
2336
((mv warnings-alist dbalist)
2337
;; pass2: apply the notes in reverse dependency order, top-down,
2338
;; marking which ports are used/set anywhere above
2339
(cwtime (us-apply-notesalist (rev x-prime) notealist dbalist
2342
(- (fast-alist-free notealist))
2345
(cwtime (vl-modulelist-apply-reportcard x-prime warnings-alist)
2347
(- (fast-alist-free warnings-alist))
2350
(cwtime (us-report-mods x-prime x ss dbalist all-walists)
2353
(- (fast-alist-free-each-alist-val all-walists))
2354
(- (fast-alist-free all-walists)))
2356
;; bozo probably free other stuff -- walists, etc.
2357
(mv x-prime dbalist)))
2553
2359
(define vl-design-bit-use-set ((x vl-design-p))
2554
2360
:returns (mv (new-x vl-design-p)
2555
2361
(dbalist us-dbalist-p))
2556
(b* ((x (vl-design-fix x))
2362
(b* (((mv okp x) (vl-design-deporder-modules x))
2364
(raise "Somehow failed to deporder sort modules.")
2366
(ss (vl-scopestack-init x))
2557
2367
((vl-design x) x)
2558
((mv new-mods dbalist) (us-analyze-mods x.mods))
2368
((mv new-mods dbalist) (us-analyze-mods x.mods ss))
2559
2369
(new-x (change-vl-design x :mods new-mods)))
2370
(vl-scopestacks-free)
2560
2371
(mv new-x dbalist)))
added
removed
books/centaur/vl/lint/bit-use-set.lisp
