<html><head>
<title>YosysJS Example Application #02</title>
<script type="text/javascript" src="yosysjs.js"></script>
<script src="http://wavedrom.com/skins/default.js" type="text/javascript"></script>
<script src="http://wavedrom.com/WaveDrom.js" type="text/javascript"></script>
<style type="text/css">
.noedit { color: #666; }
</style>
<script id="golden_verilog" type="text/plain">
module ref(input clk, reset, input [7:0] A, output reg [7:0] Y);
	always @(posedge clk) begin
		if (reset)
			Y <= 0;
		else
			Y <= ((Y << 5) + Y) ^ A;
	end
endmodule
</script>
</head><body>
	<div id="popup" style="position: fixed; left: 0; top: 0; width:100%; height:100%; text-align:center; z-index: 1000;
		background-color: rgba(100, 100, 100, 0.5);"><div style="width:300px; margin: 200px auto; background-color: #88f;
		border:3px dashed #000; padding:15px; text-align:center;"><span id="popupmsg">Loading...</span></div>
	</div>
	<h1>YosysJS Example Application #03</h1>
	<b>Your mission:</b> Create a behavioral Verilog model for the following circuit:
	<p/>
	<div id="main" style="visibility: hidden">
		<svg id="schem" width="800"></svg>
		<p/>
		<pre id="code" style="width: 800px; border:2px solid #000; padding: 0.5em;"><span class="noedit">module top(input clk, reset, input [7:0] A, output reg [7:0] Y);
  always @(posedge clock) begin</span><span class="edit" contenteditable="true">
    Y &lt;= A | {4{reset}};
  </span><span class="noedit">end
endmodule</span></pre><p/>
		<input type="button" value="Check Model" onclick="check_model()"> <span id="checkmessage"></span>
		<p/>
		<p id="wave">&nbsp;</p>
	</div>
	<script type="text/javascript">
		function on_ys_ready() {
			ys.write_file('golden.v', document.getElementById('golden_verilog').textContent);
			ys.run('echo on; read_verilog golden.v; proc;;');
			ys.run('show -notitle -width -stretch');
			YosysJS.dot_into_svg(ys.read_file('show.dot'), 'schem');
			document.getElementById('popup').style.visibility = 'hidden';
			document.getElementById('popupmsg').textContent = 'Please wait..';
			document.getElementById('main').style.visibility = 'visible';
		}
		function check_model() {
			function work() {
				ys.remove_file('wave.json');
				ys.write_file('code.v', document.getElementById('code').textContent);
				ys.errmsg = '';
				ys.run('design -reset; read_verilog code.v; hierarchy -top top; proc; opt; flatten; hierarchy; ' +
					'read_verilog golden.v; proc; miter -equiv -ignore_gold_x -make_outputs -flatten ref top miter; ' +
					'hierarchy -top miter; clean -purge; sat -set-init-undef -seq 8 -dump_json wave.json -show-ports ' +
					'-max_undef -prove trigger 0 miter');
				w = document.getElementById('wave')
				if (ys.errmsg) {
					w.innerHTML = '<b><pre>ERROR: ' + ys.errmsg.replace('&', '&amp;').replace('<', '&lt;').replace('>', '&gt;') + '</pre></b>';
				} else {
					wdata = ys.read_file('wave.json');
					if (wdata) {
						wdata = JSON.parse(wdata);
						function wsignal(signame, newname) {
							for (i = 0; i < wdata["signal"].length; i++)
								if (wdata["signal"][i].name == signame) {
									if (newname)
										wdata["signal"][i].name = newname;
									return wdata["signal"][i];
								}
							return {};
						}
						wdata2 = {
							"signal" : [
								{ name: 'clk', wave: 'P........' },
								wsignal("trigger"),
								{},
								[ "Inputs", wsignal("in_reset", "reset"), wsignal("in_A", "A") ],
								{},
								[ "Y Output", wsignal("gold_Y", "Ref"), wsignal("gate_Y", "UUT") ],
							],
							"config" : wdata["config"]
						};
						wdata2 = JSON.stringify(wdata2)
						w.innerHTML = '<b>The model did not pass verification:</b><p/>' +
								'<script type="WaveDrom">' + wdata2 + '<\/script>';
						WaveDrom.ProcessAll();
					} else {
						w.innerHTML = '<b>Congratulations! The model did pass verification.</b><p/>';
					}
				}
				document.getElementById('popup').style.visibility = 'hidden';
			}
			document.getElementById('popup').style.visibility = 'visible';
			window.setTimeout(work, 100);
		}

		YosysJS.load_viz();
		var ys = YosysJS.create('', on_ys_ready);
		ys.logprint = true;
	</script>
</body></html>