mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

Add smtmap.v describing the smt2 backend's behavior for undef bits

Browse source 
Some builtin cells have an undefined (x) output even when all inputs are
defined. This is not natively supported by the formal backends which
will produce a fully defined value instead. This can lead to issues when
combining different backends in a formal flow. To work around these,
this adds a file containing verilog implementation of cells matching the
fully defined behavior implemented by the smt2 backend.
This commit is contained in:
Jannis Harder 2022-10-20 15:41:17 +02:00
parent be1a12595a
commit 0f96ae5990
2 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
techlibs/common/Makefile.inc
View file

@ -22,6 +22,7 @@ kernel/register.o: techlibs/common/simlib_help.inc techlibs/common/simcells_help
$(eval $(call add_share_file,share,techlibs/common/simlib.v))
$(eval $(call add_share_file,share,techlibs/common/simcells.v))
$(eval $(call add_share_file,share,techlibs/common/techmap.v))
$(eval $(call add_share_file,share,techlibs/common/smtmap.v))
$(eval $(call add_share_file,share,techlibs/common/pmux2mux.v))
$(eval $(call add_share_file,share,techlibs/common/adff2dff.v))
$(eval $(call add_share_file,share,techlibs/common/dff2ff.v))

28
techlibs/common/smtmap.v Normal file
View file

@ -0,0 +1,28 @@
(* techmap_celltype = "$pmux" *)
module smt_pmux (A, B, S, Y);
parameter WIDTH = 1;
parameter S_WIDTH = 1;
(* force_downto *)
input [WIDTH-1:0] A;
(* force_downto *)
input [WIDTH*S_WIDTH-1:0] B;
(* force_downto *)
input [S_WIDTH-1:0] S;
(* force_downto *)
output [WIDTH-1:0] Y;
(* force_downto *)
wire [WIDTH-1:0] Y_B;
genvar i, j;
generate
(* force_downto *)
wire [WIDTH*(S_WIDTH+1)-1:0] C;
assign C[WIDTH-1:0] = A;
for (i = 0; i < S_WIDTH; i = i + 1)
assign C[WIDTH*(i+2)-1:WIDTH*(i+1)] = S[i] ? B[WIDTH*(i+1)-1:WIDTH*i] : C[WIDTH*(i+1)-1:WIDTH*i];
assign Y = C[WIDTH*(S_WIDTH+1)-1:WIDTH*S_WIDTH];
endgenerate
endmodule