Line 22... |
Line 22... |
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// for more details.
|
// for more details.
|
//
|
//
|
// You should have received a copy of the GNU General Public License along
|
// You should have received a copy of the GNU General Public License along
|
// with this program. (It's in the $(ROOT)/doc directory, run make with no
|
// with this program. (It's in the $(ROOT)/doc directory. Run make with no
|
// target there if the PDF file isn't present.) If not, see
|
// target there if the PDF file isn't present.) If not, see
|
// <http://www.gnu.org/licenses/> for a copy.
|
// <http://www.gnu.org/licenses/> for a copy.
|
//
|
//
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// http://www.gnu.org/licenses/gpl.html
|
// http://www.gnu.org/licenses/gpl.html
|
Line 96... |
Line 96... |
fprintf(fp, "%s", cpyleft);
|
fprintf(fp, "%s", cpyleft);
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
fprintf(fp, "//\n//\n`default_nettype\tnone\n//\n");
|
fprintf(fp,
|
fprintf(fp,
|
"module %s(i_clk, %s, i_ce, i_in, o_out, o_sync);\n"
|
"module %s(i_clk, %s, i_ce, i_in, o_out, o_sync);\n"
|
"\tparameter\t\t\tLGSIZE=%d, WIDTH=24;\n"
|
"\tparameter\t\t\tLGSIZE=%d, WIDTH=24;\n"
|
"\tinput\t\t\t\ti_clk, %s, i_ce;\n"
|
"\tinput\twire\t\t\ti_clk, %s, i_ce;\n"
|
"\tinput\t\t[(2*WIDTH-1):0]\ti_in;\n"
|
"\tinput\twire\t[(2*WIDTH-1):0]\ti_in;\n"
|
"\toutput\twire\t[(2*WIDTH-1):0]\to_out;\n"
|
"\toutput\treg\t[(2*WIDTH-1):0]\to_out;\n"
|
"\toutput\treg\t\t\to_sync;\n", modulename, resetw.c_str(),
|
"\toutput\treg\t\t\to_sync;\n", modulename, resetw.c_str(),
|
TST_DBLREVERSE_LGSIZE,
|
TST_DBLREVERSE_LGSIZE,
|
resetw.c_str());
|
resetw.c_str());
|
|
|
fprintf(fp,
|
fprintf(fp,
|
Line 111... |
Line 111... |
"\n"
|
"\n"
|
" reg [(2*WIDTH-1):0] brmem [0:((1<<(LGSIZE+1))-1)];\n"
|
" reg [(2*WIDTH-1):0] brmem [0:((1<<(LGSIZE+1))-1)];\n"
|
"\n"
|
"\n"
|
" genvar k;\n"
|
" genvar k;\n"
|
" generate for(k=0; k<LGSIZE; k=k+1)\n"
|
" generate for(k=0; k<LGSIZE; k=k+1)\n"
|
|
" begin : DBL\n"
|
" assign rdaddr[k] = wraddr[LGSIZE-1-k];\n"
|
" assign rdaddr[k] = wraddr[LGSIZE-1-k];\n"
|
" endgenerate\n"
|
" end endgenerate\n"
|
" assign rdaddr[LGSIZE] = !wraddr[LGSIZE];\n"
|
" assign rdaddr[LGSIZE] = !wraddr[LGSIZE];\n"
|
"\n"
|
"\n"
|
" reg in_reset;\n"
|
" reg in_reset;\n"
|
"\n"
|
"\n"
|
" initial in_reset = 1'b1;\n");
|
" initial in_reset = 1'b1;\n");
|
Line 162... |
Line 163... |
|
|
|
|
if (formal_property_flag) {
|
if (formal_property_flag) {
|
fprintf(fp,
|
fprintf(fp,
|
"`ifdef\tFORMAL\n"
|
"`ifdef\tFORMAL\n"
|
|
"`define\tASSERT assert\n"
|
"`ifdef BITREVERSE\n"
|
"`ifdef BITREVERSE\n"
|
"`define\tASSUME assume\n"
|
"`define\tASSUME assume\n");
|
"`define\tASSERT assert\n");
|
|
if (async_reset)
|
if (async_reset)
|
fprintf(fp,
|
fprintf(fp,
|
"\n\talways @($global_clock)\n"
|
"\n\talways @($global_clock)\n"
|
"\t\tassume(i_clk != $past(i_clk));\n\n");
|
"\t\tassume(i_clk != $past(i_clk));\n\n");
|
|
|
fprintf(fp,
|
fprintf(fp,
|
"`else\n"
|
"`else\n"
|
"`define\tASSUME assert\n"
|
"`define\tASSUME assert\n"
|
"`define\tASSERT assume\n"
|
|
"`endif\n"
|
"`endif\n"
|
"\n"
|
"\n"
|
"\treg f_past_valid;\n"
|
"\treg f_past_valid;\n"
|
"\tinitial f_past_valid = 1'b0;\n"
|
"\tinitial f_past_valid = 1'b0;\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|
Line 391... |
Line 391... |
"//\n");
|
"//\n");
|
fprintf(fp,
|
fprintf(fp,
|
"module %s(i_clk, %s, i_ce, i_in_0, i_in_1,\n"
|
"module %s(i_clk, %s, i_ce, i_in_0, i_in_1,\n"
|
"\t\to_out_0, o_out_1, o_sync);\n"
|
"\t\to_out_0, o_out_1, o_sync);\n"
|
"\tparameter\t\t\tLGSIZE=%d, WIDTH=24;\n"
|
"\tparameter\t\t\tLGSIZE=%d, WIDTH=24;\n"
|
"\tinput\t\t\t\ti_clk, %s, i_ce;\n"
|
"\tinput\twire\t\t\ti_clk, %s, i_ce;\n"
|
"\tinput\t\t[(2*WIDTH-1):0]\ti_in_0, i_in_1;\n"
|
"\tinput\twire\t[(2*WIDTH-1):0]\ti_in_0, i_in_1;\n"
|
"\toutput\twire\t[(2*WIDTH-1):0]\to_out_0, o_out_1;\n"
|
"\toutput\twire\t[(2*WIDTH-1):0]\to_out_0, o_out_1;\n"
|
"\toutput\treg\t\t\to_sync;\n", modulename,
|
"\toutput\treg\t\t\to_sync;\n", modulename,
|
resetw.c_str(), TST_DBLREVERSE_LGSIZE, resetw.c_str());
|
resetw.c_str(), TST_DBLREVERSE_LGSIZE, resetw.c_str());
|
|
|
fprintf(fp,
|
fprintf(fp,
|
Line 464... |
Line 464... |
"\n");
|
"\n");
|
|
|
if (formal_property_flag) {
|
if (formal_property_flag) {
|
fprintf(fp,
|
fprintf(fp,
|
"`ifdef\tFORMAL\n"
|
"`ifdef\tFORMAL\n"
|
|
"`define\tASSERT assert\n"
|
"`ifdef BITREVERSE\n"
|
"`ifdef BITREVERSE\n"
|
"`define\tASSUME assume\n"
|
"`define\tASSUME assume\n");
|
"`define\tASSERT assert\n");
|
|
if (async_reset)
|
if (async_reset)
|
fprintf(fp,
|
fprintf(fp,
|
"\n\talways @($global_clock)\n"
|
"\n\talways @($global_clock)\n"
|
"\t\tassume(i_clk != $past(i_clk));\n\n");
|
"\t\tassume(i_clk != $past(i_clk));\n\n");
|
|
|
fprintf(fp,
|
fprintf(fp,
|
"`else\n"
|
"`else\n"
|
"`define\tASSUME assert\n"
|
"`define\tASSUME assert\n"
|
"`define\tASSERT assume\n"
|
|
"`endif\n"
|
"`endif\n"
|
"\n"
|
"\n"
|
"\treg f_past_valid;\n"
|
"\treg f_past_valid;\n"
|
"\tinitial f_past_valid = 1'b0;\n"
|
"\tinitial f_past_valid = 1'b0;\n"
|
"\talways @(posedge i_clk)\n"
|
"\talways @(posedge i_clk)\n"
|