Produce the E-language, MSB-ordered list of bits for an expression.
(vl-msb-expr-bitlist x walist warnings) → (mv successp warnings bits)
When we translate module and gate instances into E, the arguments of the instance are Verilog expressions, and we need to convert them into E-language patterns. By the end of our simplification process, we think that each such expression should contain only:
This routine is intended to convert arbitrary expressions that include only the above forms into a list of MSB order bits.
Theorem:
(defthm return-type-of-vl-msb-expr-bitlist.successp (b* (((mv ?successp ?warnings ?bits) (vl-msb-expr-bitlist x walist warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-msb-expr-bitlist.warnings (b* (((mv ?successp ?warnings ?bits) (vl-msb-expr-bitlist x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-msb-expr-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-expr-bitlist x walist warnings))) (vl-emodwirelist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-msb-exprlist-bitlist.successp (b* (((mv ?successp ?warnings ?bits) (vl-msb-exprlist-bitlist x walist warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-msb-exprlist-bitlist.warnings (b* (((mv ?successp ?warnings ?bits) (vl-msb-exprlist-bitlist x walist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-msb-exprlist-bitlist.bits (b* (((mv ?successp ?warnings ?bits) (vl-msb-exprlist-bitlist x walist warnings))) (vl-emodwirelist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-expr-bitlist-2 (true-listp (mv-nth 2 (vl-msb-expr-bitlist x walist warnings))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-vl-msb-exprlist-bitlist-2 (true-listp (mv-nth 2 (vl-msb-exprlist-bitlist x walist warnings))) :rule-classes :type-prescription)