Support SMV resize and type-conversion operators by augustomafra · Pull Request #475 · stanford-centaur/pono

augustomafra · 2025-09-28T21:26:49Z

SMV files generated from Yosys use several bit-vector resize and type conversion operations that are not currently supported by pono.

Also adding test cases for soundness bug on RTS that got exposed when testing Yosys-generated SMV files (see soundness fix PR at #474 ).

…raint

…th constraint" This reverts commit 1369e9a.

CyanoKobalamyne

Hi! Thank you for contributing to Pono and sorry for taking so long to review your PR. I have left a couple of comments. :)

CyanoKobalamyne · 2026-01-23T01:44:20Z

frontends/smv_node.cpp

+  s << " resize (";
  ex1->generate_ostream(name, prefix, module_list, new_prefix, s);
  s << " , ";
  ex2->generate_ostream(name, prefix, module_list, new_prefix, s);
+  s << " ) ";


What is the purpose of this change?

The SMV parser actually does two passes: the first one generating an AST with SMVnodes whose only purpose is to be dumped as text with all modules flattened in SMVEncoder::preprocess(). Then the second pass reads the flattened stream and does the actual encoding to smt-switch terms.

The first pass is run with enc.module_flat = false, and the second one with enc.module_flat = true, hence the branching on this condition almost everywhere in smvparser.y.

This flow is executed from SMVEncoder's constructor:

pono/frontends/smv_encoder.h

Lines 31 to 38 in 309e07a

module_flat = false;

file = filename;

parse(filename);

preprocess();

module_flat = true;

loc.end.line = 0;

std::string output = preprocess().str();

processCase();

Having that in mind, the issue here is that the flattened text had a syntax error: it would dump resize a, 32 instead of resize(a, 32)

CyanoKobalamyne · 2026-01-28T18:31:43Z

frontends/smvparser.y

 %right OP_IMPLY
 %left OP_BI
-%left IF_ELSE
+%right IF_ELSE


I can't find the associativity of the ternary conditional described anywhere in the NuSMV manual; why did you make this change?

It seems NuSMV/NuXmv manuals do not specify that, indeed. I figured out this rule by running the test tests/encoders/inputs/smv/ternary.smv with NuXmv directly, and it would accept it as right-associative whereas pono would raise a syntax error.

I hit this condition because some SMV files generated from Yosys contained right-associative ternaries, e.g. result := a ? 0.0 : b ? 1.0 : c ? 2.0 : d ? 3.0 : 4.0;

CyanoKobalamyne · 2026-01-29T01:20:09Z

frontends/smvparser.y

              if((bvs_a == SMVnode::Real && bvs_b == SMVnode::Integer) || (bvs_a == SMVnode::Integer && bvs_b == SMVnode::Real) ){
-                e = enc.solver_->make_term(smt::Equal, a->getTerm(), b->getTerm());
+                smt::Term a_term = a->getTerm();
+                smt::Term b_term = b->getTerm();
+                if (bvs_a == SMVnode::Real || bvs_b == SMVnode::Real){
+                  if (bvs_a != SMVnode::Real)
+                    a_term = enc.solver_->make_term(smt::To_Real, a_term);
+                  if (bvs_b != SMVnode::Real)
+                    b_term = enc.solver_->make_term(smt::To_Real, b_term);
+                }
+                e = enc.solver_->make_term(smt::Equal, a_term, b_term);


As per the NuSMV manual, mixed-type equality check are not actually allowed.

Maybe there's a conceptual definition that I should double check regarding Pono's language frontend.
I see you mention NuSMV's manual (https://nusmv.fbk.eu/userman/v26/nusmv.pdf), however, I was actually following NuXmv's manual (https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf).

I assumed NuXmv was the reference used because real arithmetic was introduced only in it. Also, it introduced the signatures integer * real → boolean and real * integer → boolean for = and !=.

I don't know if Pono should stick strictly to SMV, as indeed there were no SMV tests with real types before my change. Let me know what is your decision here.
In any case, I would need to continue with the NuXmv style on my fork for the purpose of my work, so I could figure out later how to merge the related changes in SMV here.

CyanoKobalamyne · 2026-01-29T01:21:48Z

frontends/smvparser.y

+              if(enc.module_flat){
+                SMVnode *boolean = $3;
+                if(boolean->getType() != SMVnode::Boolean){
+                  throw PonoException("Word1 word type is uncompatible");


Suggested change

throw PonoException("Word1 word type is uncompatible");

throw PonoException("word1 can only be applied to booleans");

CyanoKobalamyne · 2026-01-29T01:23:09Z

frontends/smvparser.y

+                                                       boolean->getTerm(), 
+                                                       enc.solver_->make_term(1, bv1sort), 
+                                                       enc.solver_->make_term(0, bv1sort));
+                assert(res); //check res non-null


I don't think this is necessary. When would res be null? In any case, assertions get compiled out of non-debug builds.

CyanoKobalamyne · 2026-01-29T01:37:25Z

frontends/smvparser.y

               throw PonoException("No array");
            }
-            | basic_expr IF_ELSE basic_expr ":" basic_expr  {
+            | basic_expr IF_ELSE basic_expr ":" basic_expr %prec IF_ELSE {


What does this affect and why is it needed?

This complements the change making ternaries right-associative. The %prec directive tells Bison that the associativity of the entire rule follows the associative of the given token (IF_ELSE). The first change is not effective without this extra directive.

CyanoKobalamyne · 2026-01-29T01:40:51Z

frontends/smvparser.y

+              if(enc.module_flat){
+                SMVnode *expr = $4;
+                SMVnode::Type expr_type = expr->getType();
+
+                if(expr_type != SMVnode::Integer){
+                  throw PonoException("Signed word conversion type is uncompatible");
+                }
+                assert(expr);
+                smt::Term res = enc.solver_->make_term(smt::Op(smt::Int_To_BV, $2), expr->getTerm());
+                assert(res);
+                $$ = new SMVnode(res, SMVnode::Signed);
+              }else{
+                SMVnode *integer = new constant(std::to_string($2));
+                $$ = new resize_expr($4,integer);
+              }


Where is this conversion coming from? As far as I can tell, the current NuSMV manual language description says that "signed" is used for unsigned-to-signed bit vector conversion. There is a separate swconst operator for converting an integer to a signed bit-vector constant.

This was another difference introduced in nuXmv. Again, it is fine if Pono would stick to SMV, then I could keep those changes limited to my fork.

CyanoKobalamyne · 2026-01-29T01:43:43Z

tests/encoders/test_encoder_inputs.h

      { "simple_counter_integer_uf.smv", pono::ProverResult::FALSE },
      { "combined-false.smv", pono::ProverResult::FALSE },
      { "combined-true.smv", pono::ProverResult::TRUE },
+      { "counter_yosys.smv", pono::ProverResult::FALSE },


Is there any particular reason for this ordering?

None at all, I only appended the new tests at the bottom. Please let me know if any other grouping is preferred (e.g. grouping by TRUE/FALSE results or alphabetical order)

CyanoKobalamyne · 2026-01-29T01:46:28Z

tests/encoders/inputs/smv/real_arithmetic.smv

+    _$auto$rtlil#cc#2837#Not$9 := !resize(_$eq$arithmetic#sv#8$6_Y, 1);
+    _$auto$rtlil#cc#2884#And$11 := resize(_$auto$rtlil#cc#2837#Not$9, 1) & resize(0ub1_1, 1);


What are these two variables?

For some reason (maybe a bug) Yosys always dumps those dangling variables at the end of the SMV definitions. They don't have any purpose, but I left them in the test only for ensuring that Yosys' output won't be rejected in the future.

CyanoKobalamyne · 2026-01-29T01:54:39Z

tests/encoders/inputs/smv/real_arithmetic_floor.smv

+    _delta := 1.00000000000000000 / 8.00000000000000000;
+    _$div$maurice2024_adc#sv#46$14_Y := _VIN / _delta;
+    _$floor$maurice2024_adc#sv#46$15_Y := signed word[3](floor(_$div$maurice2024_adc#sv#46$14_Y));
+  INVARSPEC bool(word1(_$floor$maurice2024_adc#sv#46$15_Y = 0sb3_000));


Shouldn't this hold? At least if we assume that the type conversion is mod 8.

This test is actually pretty underconstrained because _VIN is a free input. So any real value could propagate into the floor operation.
Maybe a more meaningful test case should have an actual true invariant to check for. My goal at first was just to ensure that the syntax and typing checks would pass.

augustomafra · 2026-01-29T14:14:11Z

Hi, @CyanoKobalamyne ,

Thanks for the review! No problem with the time at all: actually, I'm pretty much focused on finishing my thesis right now, so I will probably take a while until I'm able to address the changes here. It's great to hear feedback, I will work on the improvements to carry on with the merge request when it's possible.

I'm leaving some notes regarding the reasoning behind some of the changes, so feel free to continue commenting if you have something else in mind.

augustomafra mentioned this pull request Sep 28, 2025

Fix Relational Transition Systems soundness bugs #474

Merged

augustomafra force-pushed the smv_frontend_v4 branch from 38564d2 to ffebb82 Compare October 10, 2025 01:34

augustomafra marked this pull request as ready for review October 10, 2025 02:47

augustomafra force-pushed the smv_frontend_v4 branch from 6abba63 to 611a94c Compare October 18, 2025 18:28

augustomafra added 13 commits January 17, 2026 17:05

Prevent trivial unsat in BMC-SP engine due to false simple path const…

c2c3b39

…raint

Support SMV resize operator

8495eb4

Handle SMV resize for new size smaller than word size

334d71a

Support SMV word1 conversion operator

fdf7057

Support SMV bool conversion operator

d4b05d9

Fix width bug in SMV resize operator

7372052

Fix missing parenthesis on SMV dump for resize operator

8fc513b

Add tests for SMV bitvector resize operations

9d61442

Fix associativity of ternary "?" operator

3b66188

Support "signed word [N](int)" conversion operator on SMV frontend

2a378ea

Support integer/real conversion on SMV frontend

cf9916c

Revert "Prevent trivial unsat in BMC-SP engine due to false simple pa…

bab587c

…th constraint" This reverts commit 1369e9a.

Add SMV tests for ternary, toint and floor

4a6641e

augustomafra force-pushed the smv_frontend_v4 branch from 611a94c to 4a6641e Compare January 17, 2026 20:08

CyanoKobalamyne requested changes Jan 29, 2026

View reviewed changes

	module_flat = false;
	file = filename;
	parse(filename);
	preprocess();
	module_flat = true;
	loc.end.line = 0;
	std::string output = preprocess().str();
	processCase();

	throw PonoException("Word1 word type is uncompatible");
	throw PonoException("word1 can only be applied to booleans");

		_$auto$rtlil#cc#2837#Not$9 := !resize(_$eq$arithmetic#sv#8$6_Y, 1);
		_$auto$rtlil#cc#2884#And$11 := resize(_$auto$rtlil#cc#2837#Not$9, 1) & resize(0ub1_1, 1);

Conversation

augustomafra commented Sep 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

CyanoKobalamyne left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

augustomafra commented Jan 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

augustomafra commented Sep 28, 2025 •

edited

Loading