[Libre-soc-bugs] [Bug 835] add support for smtlib2 floating-point to yosys and nmigen

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=835

--- Comment #34 from Jacob Lifshay <programmerjake at gmail.com> ---
I switched nmigen and yosys to the new rtlil API:
https://github.com/YosysHQ/yosys/pull/3319#issuecomment-1145606912
> I switched the implementation to use attributes on the outputs
> and an attribute on the module.
> 
> example:
> yosys/tests/various/smtlib2_module.v
> 
> Lines 1 to 10 in cd57c5a
> 
>  (* smtlib2_module *) 
>  module smtlib2(a, b, add, sub, eq); 
>  	input [7:0] a, b; 
>  	(* smtlib2_comb_expr = "(bvadd a b)" *) 
>  	output [7:0] add; 
>  	(* smtlib2_comb_expr = "(bvadd a (bvneg b))" *) 
>  	output [7:0] sub; 
>  	(* smtlib2_comb_expr = "(= a b)" *) 
>  	output eq; 
>  endmodule 
> I also added a test that compares the generated smt2 to the
> expected output, avoiding the need to run a smtlib2 solver (which
> iirc yosys doesn't want a dependency on)

I haven't yet backported the new yosys modifications to the yosys 0.13 branch,
I'll do that after I get it working upstream.

I still need to make some modifications to sby:
* removing -simcheck:
https://github.com/YosysHQ/sby/issues/168
* adding support for cvc5 (both cvc4 and z3 fail on one of nmigen's new tests
now):
https://github.com/YosysHQ/sby/issues/167

-- 
You are receiving this mail because:
You are on the CC list for the bug.