OPERATORS library in rtl netlist produced by Mentor's precis

  • Thread starter Vlad Ciubotariu
  • Start date
V

Vlad Ciubotariu

Guest
Hi all,

I'm working on a formal verification tool that starts with the rtl netlist
produced by precision. The netlist contains some operators that are left a
blackboxes, some of them are shown below:

or_10u_10u(a(9:0) : INPUT, d : OUTPUT)
or_5u_5u(a(4:0) : INPUT, d : OUTPUT)
add_16u_16u_16u_0(cin : INPUT, a(15:0) : INPUT, b(15:0) : INPUT, d(15:0) : OUTPUT, cout : OUTPUT)
eq_8u_8u(a(7:0) : INPUT, b(7:0) : INPUT, d : OUTPUT)
eq_24u_24u(a(23:0) : INPUT, b(23:0) : INPUT, d : OUTPUT)
or_13u_13u(a(12:0) : INPUT, d : OUTPUT)
eq_9u_9u(a(8:0) : INPUT, b(8:0) : INPUT, d : OUTPUT)
or_9u_9u(a(8:0) : INPUT, d : OUTPUT)
eq_28u_28u(a(27:0) : INPUT, b(27:0) : INPUT, d : OUTPUT)
mult_32u_32u_32u(a(31:0) : INPUT, b(31:0) : INPUT, d(31:0) : OUTPUT)
eq_3u_3u(a(2:0) : INPUT, b(2:0) : INPUT, d : OUTPUT)
xor_3u_3u(a(2:0) : INPUT, d : OUTPUT)
eq_10u_10u(a(9:0) : INPUT, b(9:0) : INPUT, d : OUTPUT)
eq_23u_23u(a(22:0) : INPUT, b(22:0) : INPUT, d : OUTPUT)
eq_29u_29u(a(28:0) : INPUT, b(28:0) : INPUT, d : OUTPUT)
eq_26u_26u(a(25:0) : INPUT, b(25:0) : INPUT, d : OUTPUT)
eq_30u_30u(a(29:0) : INPUT, b(29:0) : INPUT, d : OUTPUT)
case_6_15_1_15(ctrl(5:0) : INPUT, data(14:0) : INPUT, default_data(0:0) : INPUT, out(0:0) : OUTPUT)
case_6_20_1_2(ctrl(5:0) : INPUT, data(19:0) : INPUT, default_data(0:0) :
INPUT, out(0:0) : OUTPUT)

The precision manual specifies how these mnemonics are derived but it does
not give functional descriptions. I'm particularly asymmetric operators
such as 'case' above.

For a 'case' operator the netlist would have this information:

(cell case_6_15_1_1 (cellType GENERIC)
(property (rename EX_GENERIC "$GENERIC") (string "modgen_case_op"))
(property (rename EX_minterms "$minterms") (string "( 100001 100010 100011 100100 100101 100110 100111 000000 000001 000011 000100 110101 110110 110111 000110 )"))
(property (rename EX_cell_index "$cell_index") (string "1"))
(property (rename EX_size "$size") (string "1"))
(property (rename EX_select_size "$select_size") (string "6"))
(property (rename EX_num_minterms "$num_minterms") (string "15"))
(property (rename EX_full_case "$full_case") (string "false"))
(property (rename EX_default_dc "$default_dc") (string "false"))
(property (rename EX_onehot "$onehot") (string "false"))
(view INTERFACE (viewType NETLIST)
(interface
(port (array (rename ctrl "ctrl(5:0)") 6 )(direction INPUT))
(port (array (rename data "data(14:0)") 15 )(direction INPUT))
(port (array (rename default_data "default_data(0:0)") 1 )(direction INPUT))
(port (array (rename out "out(0:0)") 1 )(direction OUTPUT)))))

The midterms have length 6, which is the number of control inputs, and
there are 15 of them, exactly the number of data inputs.

Does anybody have any know-how about the library OPERATORS that precision
uses? Or what would work best to find out what the blackboxes do?

thanks,
vlad
 
On Feb 3, 12:06 pm, Vlad Ciubotariu <vcciu...@uwaterloo.ca> wrote:
Hi all,

I'm working on a formal verification tool that starts with the rtl netlist
produced by precision. The netlist contains some operators that are left a
blackboxes, some of them are shown below:

or_10u_10u(a(9:0) : INPUT, d : OUTPUT)
or_5u_5u(a(4:0) : INPUT, d : OUTPUT)
add_16u_16u_16u_0(cin : INPUT, a(15:0) : INPUT, b(15:0) : INPUT, d(15:0) : OUTPUT, cout : OUTPUT)
eq_8u_8u(a(7:0) : INPUT, b(7:0) : INPUT, d : OUTPUT)
eq_24u_24u(a(23:0) : INPUT, b(23:0) : INPUT, d : OUTPUT)
or_13u_13u(a(12:0) : INPUT, d : OUTPUT)
eq_9u_9u(a(8:0) : INPUT, b(8:0) : INPUT, d : OUTPUT)
or_9u_9u(a(8:0) : INPUT, d : OUTPUT)
eq_28u_28u(a(27:0) : INPUT, b(27:0) : INPUT, d : OUTPUT)
mult_32u_32u_32u(a(31:0) : INPUT, b(31:0) : INPUT, d(31:0) : OUTPUT)
eq_3u_3u(a(2:0) : INPUT, b(2:0) : INPUT, d : OUTPUT)
xor_3u_3u(a(2:0) : INPUT, d : OUTPUT)
eq_10u_10u(a(9:0) : INPUT, b(9:0) : INPUT, d : OUTPUT)
eq_23u_23u(a(22:0) : INPUT, b(22:0) : INPUT, d : OUTPUT)
eq_29u_29u(a(28:0) : INPUT, b(28:0) : INPUT, d : OUTPUT)
eq_26u_26u(a(25:0) : INPUT, b(25:0) : INPUT, d : OUTPUT)
eq_30u_30u(a(29:0) : INPUT, b(29:0) : INPUT, d : OUTPUT)
case_6_15_1_15(ctrl(5:0) : INPUT, data(14:0) : INPUT, default_data(0:0) : INPUT, out(0:0) : OUTPUT)
case_6_20_1_2(ctrl(5:0) : INPUT, data(19:0) : INPUT, default_data(0:0) :
INPUT, out(0:0) : OUTPUT)

The precision manual specifies how these mnemonics are derived but it does
not give functional descriptions. I'm particularly asymmetric operators
such as 'case' above.

For a 'case' operator the netlist would have this information:

(cell case_6_15_1_1 (cellType GENERIC)
(property (rename EX_GENERIC "$GENERIC") (string "modgen_case_op"))
(property (rename EX_minterms "$minterms") (string "( 100001 100010 100011 100100 100101 100110 100111 000000 000001 000011 000100 110101 110110 110111 000110 )"))
(property (rename EX_cell_index "$cell_index") (string "1"))
(property (rename EX_size "$size") (string "1"))
(property (rename EX_select_size "$select_size") (string "6"))
(property (rename EX_num_minterms "$num_minterms") (string "15"))
(property (rename EX_full_case "$full_case") (string "false"))
(property (rename EX_default_dc "$default_dc") (string "false"))
(property (rename EX_onehot "$onehot") (string "false"))
(view INTERFACE (viewType NETLIST)
(interface
(port (array (rename ctrl "ctrl(5:0)") 6 )(direction INPUT))
(port (array (rename data "data(14:0)") 15 )(direction INPUT))
(port (array (rename default_data "default_data(0:0)") 1 )(direction INPUT))
(port (array (rename out "out(0:0)") 1 )(direction OUTPUT)))))

The midterms have length 6, which is the number of control inputs, and
there are 15 of them, exactly the number of data inputs.

Does anybody have any know-how about the library OPERATORS that precision
uses? Or what would work best to find out what the blackboxes do?

thanks,
vlad
Click to expand...
Vlad,

Sometimes there is no good public reference for the primitives into
which a synthesizer targets a design. If you know what target device
you're after though, you can sometimes find a relevant functional
model in your simulator, just by rooting through the file system.
Reading the code (assuming there's a non-encrypted source model) can
give you clues.

- Kenn
 
On Sun, 03 Feb 2008 12:06:55 -0500, Vlad Ciubotariu <vcciubot@uwaterloo.ca>
wrote:

Hi all,

I'm working on a formal verification tool that starts with the rtl netlist
produced by precision.

For a 'case' operator the netlist would have this information:

(cell case_6_15_1_1 (cellType GENERIC)
(property (rename EX_GENERIC "$GENERIC") (string "modgen_case_op"))
Click to expand...
This may be the clue. Mentor uses a tool (tool set?) called "modgen" to generate
black boxes. I can't find out much about it offhand, but a brief summary appears
in
http://web.cecs.pdx.edu/~mperkows/CLASS_VHDL/=EDITH_LEONARDO/leo_sort.htm

"Module Generation
High-level design allows the use of operators such as add, subtract, multiply,
compare and increment. These functions may be inefficient to synthesize as
random logic, and an ideal implementation for the technology is generally
already known. Leonardo's Module Generation (MODGEN) automatically detects many
common arithmetic relational and other data flow operations and uses a
technology-specific implementation. This reduces synthesis time and improves
results. Module generators are optimized for different architectures and include
area and delay trade-offs. "

So taking a relatively abstract specification (expressed in the EDIF), Modgen
will create special-case logic using primitives provided by a specific FPGA
family (e.g. using wide multiplexers, or fast carry chains, if they are
available).

I suspect you need to contact Mentor support, explain what you are doing, and
ask for any documentation or help they can give you on Modgen.

(property (rename EX_minterms "$minterms") (string "( 100001 100010 100011 100100 100101 100110 100111 000000 000001 000011 000100 110101 110110 110111 000110 )"))
Click to expand...
This Case operator appears to be a 15:1 mux, 1 bit wide, with some decoding from
the 6-bit input word to the multiplexer.
But these minterms are not in either sequential or Gray order. If they
correspond directly to the cases in your original design, the internals may be
simple; if not, it is likely that re-ordering has been done to simplify
decoding, optimise delays, or reduce gate count.

- Brian
 
Thanks for drawing my attention to the modgen library. It turns out
precision implements those components for simulation purpose and it's
easy enough to figure out what the inputs represent. I couldn't find the
case_n_m blocks though. Hopefully I'll figure them out on a per need basis
through simulation.

vlad

On Mon, 04 Feb 2008 12:22:49 +0000, Brian Drummond wrote:

On Sun, 03 Feb 2008 12:06:55 -0500, Vlad Ciubotariu <vcciubot@uwaterloo.ca
wrote:

Hi all,

I'm working on a formal verification tool that starts with the rtl netlist
produced by precision.

For a 'case' operator the netlist would have this information:

(cell case_6_15_1_1 (cellType GENERIC)
(property (rename EX_GENERIC "$GENERIC") (string "modgen_case_op"))

This may be the clue. Mentor uses a tool (tool set?) called "modgen" to generate
black boxes. I can't find out much about it offhand, but a brief summary appears
in
http://web.cecs.pdx.edu/~mperkows/CLASS_VHDL/=EDITH_LEONARDO/leo_sort.htm

"Module Generation
High-level design allows the use of operators such as add, subtract, multiply,
compare and increment. These functions may be inefficient to synthesize as
random logic, and an ideal implementation for the technology is generally
already known. Leonardo's Module Generation (MODGEN) automatically detects many
common arithmetic relational and other data flow operations and uses a
technology-specific implementation. This reduces synthesis time and improves
results. Module generators are optimized for different architectures and include
area and delay trade-offs. "

So taking a relatively abstract specification (expressed in the EDIF), Modgen
will create special-case logic using primitives provided by a specific FPGA
family (e.g. using wide multiplexers, or fast carry chains, if they are
available).

I suspect you need to contact Mentor support, explain what you are doing, and
ask for any documentation or help they can give you on Modgen.

(property (rename EX_minterms "$minterms") (string "( 100001 100010 100011 100100 100101 100110 100111 000000 000001 000011 000100 110101 110110 110111 000110 )"))

This Case operator appears to be a 15:1 mux, 1 bit wide, with some decoding from
the 6-bit input word to the multiplexer.
But these minterms are not in either sequential or Gray order. If they
correspond directly to the cases in your original design, the internals may be
simple; if not, it is likely that re-ordering has been done to simplify
decoding, optimise delays, or reduce gate count.

- Brian
Click to expand...
 
Vlad,

Sometimes there is no good public reference for the primitives into
which a synthesizer targets a design. If you know what target device
you're after though, you can sometimes find a relevant functional
model in your simulator, just by rooting through the file system.
Reading the code (assuming there's a non-encrypted source model) can
give you clues.

- Kenn
Click to expand...
Hey Kenn,

Good to hear from you! There's a bunch of encrypted vhd files that
matched my search for modgen, I assume they are modgen implementation for
those target devices. I'm out of luck, hopefully I can trigger enough
inputs through simulation.

vlad
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top